error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/packages/autograder/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/build/lib /home/jireh/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean -Dlinter.unusedVariables=false -DquotPrecheck=false -DwarningAsError=false -Dpp.unicode.fun=true ./././Math2001/09_Sets/02_Set_Operations.lean -R ././. -o ./.lake/build/lib/Math2001/09_Sets/02_Set_Operations.olean -i ./.lake/build/lib/Math2001/09_Sets/02_Set_Operations.ilean -c ./.lake/build/ir/Math2001/09_Sets/02_Set_Operations.c --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Ord-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-LocalContext-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Parser-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-OpenPrivate-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Name-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Format-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Position-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Float-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Json-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Json-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-TryThis-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-Simpa-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Classes-Order-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Control-ForInStep-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Command-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-Unreachable-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Linter-UnreachableTactic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-TagAttribute-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-AttributeExtra-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Linter-UnnecessarySeqFocus-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Linter-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-NoMatch-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Util-TermUnsafe-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-GuardExpr-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-ByCases-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-SeqFocus-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-ShowTerm-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-SimpTrace-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Meta-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-Tactic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-InfoTree-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-CodeAction-Attr-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-CodeAction-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-CodeAction-Deprecated-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-Alias-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Lean-NameMapAttribute-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-Lint-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Array-Init-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Tactic-Lint-Misc-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Logic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Nat-Init-Lemmas-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Classes-Dvd-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Nat-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Nat-Lemmas-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-BinomialHeap-Basic-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-BinomialHeap-Lemmas-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-BinomialHeap-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-IdStrategyHeap-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Misc-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Expr-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-Reduction-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Order-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Clause-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-MessageData-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-LazyList-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-DUnif-UnifProblem-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-OccursCheck-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Fin-Init-Lemmas-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Util-ExtendedBinder-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Classes-SetNotation-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-List-Init-Lemmas-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-List-Init-Attach-1.so --load-dynlib=./.lake/packages/std/.lake/build/lib/libStd-Data-Array-Basic-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-DUnif-Utils-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-DUnif-Bindings-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-DUnif-Oracles-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-DUnif-UnifRules-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Unif-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-MClause-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Match-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-AbstractMVars-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-RuleM-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Selection-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Fingerprint-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-SubsumptionTrie-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-ClauseSubsumptionCheck-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-StrategyHeap-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-DeeplyOccurringVars-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-ProverM-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-ClauseStreamHeap-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Simp-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-ProofReconstruction-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-Clausification-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Preprocessing-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ClauseSubsumption-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ContextualLiteralCutting-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-Demodulation-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-EqualitySubsumption-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-SimplifyReflect-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-BackwardSimplification-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-BetaEtaReduction-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-BoolSimp-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ClausifyPropEq-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ElimDupLit-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ElimResolvedLit-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-EqualityFactoring-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-EqualityResolution-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-FalseElim-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-IdentBoolFalseElim-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-IdentPropFalseElim-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-Superposition-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-SyntacticTautologyDeletion1-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-SyntacticTautologyDeletion2-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-SyntacticTautologyDeletion3-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-DestructiveEqualityResolution-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-IdentBoolHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-BoolHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-EqHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ExistsHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ForallHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-NeHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-ArgumentCongruence-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-FluidSup-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Rules-FluidBoolHoist-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Util-TypeInhabitationReasoning-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Saturate-1.so --load-dynlib=./.lake/packages/Duper/.lake/build/lib/libDuper-Tactic-1.so
error: stdout:
./././Math2001/09_Sets/02_Set_Operations.lean:23:0: warning: declaration uses 'sorry'
./././Math2001/09_Sets/02_Set_Operations.lean:132:51: error: Failed, can't rule out other cases
./././Math2001/09_Sets/02_Set_Operations.lean:135:2: error: Failed, can't rule out other cases
./././Math2001/09_Sets/02_Set_Operations.lean:137:37: error: Failed, can't rule out other cases
./././Math2001/09_Sets/02_Set_Operations.lean:140:2: error: Failed, can't rule out other cases
./././Math2001/09_Sets/02_Set_Operations.lean:142:0: warning: declaration uses 'sorry'
./././Math2001/09_Sets/02_Set_Operations.lean:146:0: warning: declaration uses 'sorry'
./././Math2001/09_Sets/02_Set_Operations.lean:149:0: warning: declaration uses 'sorry'
./././Math2001/09_Sets/02_Set_Operations.lean:157:0: warning: declaration uses 'sorry'
error: external command `/home/jireh/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean` exited with code 1