import DuperXp
-- import Mathlib.LinearAlgebra.Finrank
-- import Mathlib.LinearAlgebra.FreeModule.Finite.Rank
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.Tactic

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring

open QuadraticForm BilinForm ExteriorAlgebra FiniteDimensional

open Function
open BigOperators
open FiniteDimensional

universe uκ uR uM uι

variable {
κ: Type uκ
κ : 
Type uκ: Type (uκ + 1)
Type uκ}
variable {
R: Type uR
R : 
Type uR: Type (uR + 1)
Type uR} [
CommRing: Type uR → Type uR
CommRing 
R: Type uR
R] [
Invertible: {α : Type uR} → [inst : Mul α] → [inst : One α] → α → Type uR
Invertible (
2: R
2 : 
R: Type uR
R)] [
Nontrivial: Type uR → Prop
Nontrivial 
R: Type uR
R]
variable {
M: Type uM
M : 
Type uM: Type (uM + 1)
Type uM} [
AddCommGroup: Type uM → Type uM
AddCommGroup 
M: Type uM
M] [
Module: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst : AddCommMonoid M] → Type (max uR uM)
Module 
R: Type uR
R 
M: Type uM
M]
-- variable {B : BilinForm R M}
variable (
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type uR) →
  (M : Type uM) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Type (max uR uM)
QuadraticForm 
R: Type uR
R 
M: Type uM
M) {
Cl: CliffordAlgebra Q
Cl : 
CliffordAlgebra: {R : Type uR} →
  [inst : CommRing R] →
    {M : Type uM} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max uM uR)
CliffordAlgebra 
Q: QuadraticForm R M
Q} {
Ex: ExteriorAlgebra R M
Ex : 
ExteriorAlgebra: (R : Type uR) → [inst : CommRing R] → (M : Type uM) → [inst_1 : AddCommGroup M] → [inst : Module R M] → Type (max uM uR)
ExteriorAlgebra 
R: Type uR
R 
M: Type uM
M}
variable [
Module.Finite: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Finite 
R: Type uR
R 
M: Type uM
M] [
Module.Free: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Prop
Module.Free 
R: Type uR
R 
M: Type uM
M]

set_option trace.duper.printProof true
set_option trace.duper.proofReconstruction true

theorem 
barber_paradox: ∀ {person : Type} {shaves : person → person → Prop}, (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) → False
barber_paradox {
person: Type
person : 
Type: Type 1
Type} {
shaves: person → person → Prop
shaves : 
person: Type
person → 
person: Type
person → 
Prop: Type
Prop}
  (
h: ∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p
h : ∃ 
b: person
b : 
person: Type
person, ∀ 
p: person
p : 
person: Type
person, (
shaves: person → person → Prop
shaves 
b: person
b 
p: person
p ↔ (¬ 
shaves: person → person → Prop
shaves 
p: person
p 
p: person
p))) : 
False: Prop
False :=
  by
Goals accomplished! 🐙 duper [*] {preprocessing := no_preprocessing, inhabitationReasoning := true}
[duper.printProof] Clause #1 (by assumption []): (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) = True
[duper.printProof] Clause #3 (by clausification [1]): ∀ (a : person),
      (∀ (p : person), shaves (@skS.0 Type 0 (person → person) a) p ↔ ¬shaves p p) = True
[duper.printProof] Clause #4 (by clausification [1]): Nonempty person = True
[duper.printProof] Clause #5 (by clausification [3]): ∀ (a a_1 : person),
      (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) = True
[duper.printProof] Clause #6 (by clausification [5]): ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ (¬shaves a_1 a_1) = False
[duper.printProof] Clause #7 (by clausification [5]): ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ (¬shaves a_1 a_1) = True
[duper.printProof] Clause #8 (by clausification [6]): ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ shaves a_1 a_1 = True
[duper.printProof] Clause #9 (by equality factoring [8]): ∀ (a : person),
      True ≠ True ∨ shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True
[duper.printProof] Clause #10 (by clausification [7]): ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ shaves a_1 a_1 = False
[duper.printProof] Clause #13 (by clausification [9]): ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨
        True = False ∨ True = False
[duper.printProof] Clause #15 (by clausification [13]): ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨ True = False
[duper.printProof] Clause #16 (by clausification [15]): ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True
[duper.printProof] Clause #17 (by superposition [16, 10]): person → True = False ∨ True = False
[duper.printProof] Clause #20 (by removeVanishedVars [17, 4]): True = False ∨ True = False
[duper.printProof] Clause #21 (by clausification [20]): True = False
[duper.printProof] Clause #22 (by clausification [21]): False
[duper.proofReconstruction] Collected clauses: [(∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) = True,
     ∀ (a : person), (∀ (p : person), shaves (@skS.0 Type 0 (person → person) a) p ↔ ¬shaves p p) = True,
     Nonempty person = True,
     ∀ (a a_1 : person), (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) = True,
     ∀ (a a_1 : person), shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ (¬shaves a_1 a_1) = False,
     ∀ (a a_1 : person), shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ (¬shaves a_1 a_1) = True,
     ∀ (a a_1 : person), shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ shaves a_1 a_1 = True,
     ∀ (a : person),
       True ≠ True ∨ shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True,
     ∀ (a a_1 : person), shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ shaves a_1 a_1 = False,
     ∀ (a : person),
       shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨
         True = False ∨ True = False,
     ∀ (a : person),
       shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨ True = False,
     ∀ (a : person), shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True,
     person → True = False ∨ True = False,
     True = False ∨ True = False,
     True = False,
     False]
[duper.proofReconstruction] Request [] ↦ [] for False
[duper.proofReconstruction] Request [] ↦ [] for True = False
[duper.proofReconstruction] Request [] ↦ [] for True = False ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for person → True = False ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨
        True = False ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : person),
      True ≠ True ∨ shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ shaves a_1 a_1 = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ (¬shaves a_1 a_1) = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : person),
      (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : person),
      (∀ (p : person), shaves (@skS.0 Type 0 (person → person) a) p ↔ ¬shaves p p) = True
[duper.proofReconstruction] Request [] ↦ [] for (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ shaves a_1 a_1 = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ (¬shaves a_1 a_1) = True
[duper.proofReconstruction] Request [] ↦ [] for Nonempty person = True
[duper.proofReconstruction] Reconstructing proof for #1 : [] ↦ [] @ (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) =
      True, Rule Name: assumption
[duper.proofReconstruction] #1's newProof: eq_true h
[duper.proofReconstruction] Instantiating parent (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) =
      True ≡≡ person → (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing skolem, _uniq.13518 ≡≡ skol.0 : person →
      person := Duper.Skolem.some fun x => ∀ (p : person), shaves x p ↔ ¬shaves p p
[duper.proofReconstruction] Reconstructing proof for #3 : [] ↦ [] @ ∀ (a : person),
      (∀ (p : person), shaves (skol.0 a) p ↔ ¬shaves p p) = True, Rule Name: clausification
[duper.proofReconstruction] #3's newProof: fun a =>
      (fun h => eq_true (Duper.Skolem.spec ((fun x_0 => x_0) a) (of_eq_true h))) clause.1.0
[duper.proofReconstruction] Instantiating parent (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) =
      True ≡≡ (∃ b, ∀ (p : person), shaves b p ↔ ¬shaves p p) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #4 : [] ↦ [] @ Nonempty person = True, Rule Name: clausification
[duper.proofReconstruction] #4's newProof: (fun h => eq_true (Duper.nonempty_of_exists h)) clause.1.0
[duper.proofReconstruction] Instantiating parent ∀ (a : person),
      (∀ (p : person), shaves (@skS.0 Type 0 (person → person) a) p ↔ ¬shaves p p) =
        True ≡≡ ∀ (x_0 : person),
      person →
        (fun a => (∀ (p : person), shaves (@skS.0 Type 0 (person → person) a) p ↔ ¬shaves p p) = True)
          x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #5 : [] ↦ [] @ ∀ (a a_1 : person),
      (shaves (skol.0 a) a_1 ↔ ¬shaves a_1 a_1) = True, Rule Name: clausification
[duper.proofReconstruction] #5's newProof: fun a a_1 =>
      (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.3.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : person),
      (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) =
        True ≡≡ ∀ (x_0 x_1 : person),
      (fun a a_1 => (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) = True) x_0
        x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #6 : [] ↦ [] @ ∀ (a a_1 : person),
      shaves (skol.0 a) a_1 = True ∨ (¬shaves a_1 a_1) = False, Rule Name: clausification
[duper.proofReconstruction] #6's newProof: fun a a_1 => (fun h => Duper.clausify_iff1 h) (clause.5.0 a a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : person),
      (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) =
        True ≡≡ ∀ (x_0 x_1 : person),
      (fun a a_1 => (shaves (@skS.0 Type 0 (person → person) a) a_1 ↔ ¬shaves a_1 a_1) = True) x_0
        x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #7 : [] ↦ [] @ ∀ (a a_1 : person),
      shaves (skol.0 a) a_1 = False ∨ (¬shaves a_1 a_1) = True, Rule Name: clausification
[duper.proofReconstruction] #7's newProof: fun a a_1 => (fun h => Duper.clausify_iff2 h) (clause.5.0 a a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨
        (¬shaves a_1 a_1) =
          False ≡≡ ∀ (x_0 x_1 : person),
      (fun a a_1 => shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ (¬shaves a_1 a_1) = False) x_0
        x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #8 : [] ↦ [] @ ∀ (a a_1 : person),
      shaves (skol.0 a) a_1 = True ∨ shaves a_1 a_1 = True, Rule Name: clausification
[duper.proofReconstruction] #8's newProof: fun a a_1 =>
      (fun h => Or.elim h (fun h => Or.inl h) fun h => Or.inr (Duper.clausify_not_false h)) (clause.6.0 a a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨
        shaves a_1 a_1 =
          True ≡≡ ∀ (x_0 : person),
      (fun a a_1 => shaves (@skS.0 Type 0 (person → person) a) a_1 = True ∨ shaves a_1 a_1 = True) x_0
        (@skS.0 Type 0 (person → person) x_0) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #9 : [] ↦ [] @ ∀ (a : person),
      True ≠ True ∨ shaves (skol.0 a) (skol.0 a) = True, Rule Name: equality factoring
[duper.proofReconstruction] #9's newProof: fun a =>
      (fun h => Or.elim h (fun h => Duper.equality_factoring_soundness1 True h) fun h => Or.inr h)
        (clause.8.0 a (skol.0 a))
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨
        (¬shaves a_1 a_1) =
          True ≡≡ ∀ (x_0 x_1 : person),
      (fun a a_1 => shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ (¬shaves a_1 a_1) = True) x_0
        x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #10 : [] ↦ [] @ ∀ (a a_1 : person),
      shaves (skol.0 a) a_1 = False ∨ shaves a_1 a_1 = False, Rule Name: clausification
[duper.proofReconstruction] #10's newProof: fun a a_1 =>
      (fun h => Or.elim h (fun h => Or.inl h) fun h => Or.inr (Duper.clausify_not h)) (clause.7.0 a a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a : person),
      True ≠ True ∨
        shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) =
          True ≡≡ ∀ (x_0 : person),
      (fun a => True ≠ True ∨ shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True)
        x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #13 : [] ↦ [] @ ∀ (a : person),
      shaves (skol.0 a) (skol.0 a) = True ∨ True = False ∨ True = False, Rule Name: clausification
[duper.proofReconstruction] #13's newProof: fun a =>
      (fun h => Or.elim h (fun h => Or.inr (Duper.clausify_prop_inequality1 h)) fun h => Or.inl h) (clause.9.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨
        True = False ∨
          True =
            False ≡≡ ∀ (x_0 : person),
      (fun a =>
          shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨
            True = False ∨ True = False)
        x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #15 : [] ↦ [] @ ∀ (a : person),
      shaves (skol.0 a) (skol.0 a) = True ∨ True = False, Rule Name: clausification
[duper.proofReconstruction] #15's newProof: fun a =>
      (fun h =>
          Or.elim h (fun h => Or.inl h) fun h =>
            Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => Or.inr h)
        (clause.13.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨
        True =
          False ≡≡ ∀ (x_0 : person),
      (fun a => shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True ∨ True = False)
        x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #16 : [] ↦ [] @ ∀ (a : person),
      shaves (skol.0 a) (skol.0 a) = True, Rule Name: clausification
[duper.proofReconstruction] #16's newProof: fun a =>
      (fun h => Or.elim h (fun h => h) fun h => False.elim (Duper.true_neq_false h)) (clause.15.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : person),
      shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) =
        True ≡≡ ∀ (x_0 : person),
      (fun a => shaves (@skS.0 Type 0 (person → person) a) (@skS.0 Type 0 (person → person) a) = True)
        x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : person),
      shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨
        shaves a_1 a_1 =
          False ≡≡ ∀ (x_0 : person),
      (fun a a_1 => shaves (@skS.0 Type 0 (person → person) a) a_1 = False ∨ shaves a_1 a_1 = False) x_0
        (@skS.0 Type 0 (person → person) x_0) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #17 : [] ↦ [] @ person →
      True = False ∨ True = False, Rule Name: superposition
[duper.proofReconstruction] #17's newProof: fun a =>
      (fun heq =>
          (fun h =>
              Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => x = False) heq) h)) fun h =>
                Or.inr (Eq.mp (congrArg (fun x => x = False) heq) h))
            (clause.10.0 a (skol.0 a)))
        (clause.16.0 a)
[duper.proofReconstruction] Instantiating parent person →
      True = False ∨
        True = False ≡≡ ∀ (x_0 : person), (fun a => True = False ∨ True = False) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent Nonempty person =
      True ≡≡ person → Nonempty person = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #20 : [] ↦ [] @ True = False ∨
      True = False, Rule Name: removeVanishedVars
[duper.proofReconstruction] #20's newProof: clause.17.0 Classical.ofNonempty
[duper.proofReconstruction] Instantiating parent True = False ∨
      True = False ≡≡ True = False ∨ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #21 : [] ↦ [] @ True = False, Rule Name: clausification
[duper.proofReconstruction] #21's newProof: (fun h =>
        Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => h)
      clause.20.0
[duper.proofReconstruction] Instantiating parent True = False ≡≡ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #22 : [] ↦ [] @ False, Rule Name: clausification
[duper.proofReconstruction] #22's newProof: (fun h => False.elim (Duper.true_neq_false h)) clause.21.0
[duper.proofReconstruction] Proof: let clause.1.0 := eq_true h;
    let skol.0 := Duper.Skolem.some fun x => ∀ (p : person), shaves x p ↔ ¬shaves p p;
    let clause.3.0 := fun a => (fun h => eq_true (Duper.Skolem.spec ((fun x_0 => x_0) a) (of_eq_true h))) clause.1.0;
    let clause.4.0 := (fun h => eq_true (Duper.nonempty_of_exists h)) clause.1.0;
    let clause.5.0 := fun a a_1 => (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.3.0 a);
    let clause.6.0 := fun a a_1 => (fun h => Duper.clausify_iff1 h) (clause.5.0 a a_1);
    let clause.7.0 := fun a a_1 => (fun h => Duper.clausify_iff2 h) (clause.5.0 a a_1);
    let clause.8.0 := fun a a_1 =>
      (fun h => Or.elim h (fun h => Or.inl h) fun h => Or.inr (Duper.clausify_not_false h)) (clause.6.0 a a_1);
    let clause.9.0 := fun a =>
      (fun h => Or.elim h (fun h => Duper.equality_factoring_soundness1 True h) fun h => Or.inr h)
        (clause.8.0 a (skol.0 a));
    let clause.10.0 := fun a a_1 =>
      (fun h => Or.elim h (fun h => Or.inl h) fun h => Or.inr (Duper.clausify_not h)) (clause.7.0 a a_1);
    let clause.13.0 := fun a =>
      (fun h => Or.elim h (fun h => Or.inr (Duper.clausify_prop_inequality1 h)) fun h => Or.inl h) (clause.9.0 a);
    let clause.15.0 := fun a =>
      (fun h =>
          Or.elim h (fun h => Or.inl h) fun h =>
            Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => Or.inr h)
        (clause.13.0 a);
    let clause.16.0 := fun a =>
      (fun h => Or.elim h (fun h => h) fun h => False.elim (Duper.true_neq_false h)) (clause.15.0 a);
    let clause.17.0 := fun a =>
      (fun heq =>
          (fun h =>
              Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => x = False) heq) h)) fun h =>
                Or.inr (Eq.mp (congrArg (fun x => x = False) heq) h))
            (clause.10.0 a (skol.0 a)))
        (clause.16.0 a);
    let clause.20.0 := clause.17.0 Classical.ofNonempty;
    let clause.21.0 := (fun h => Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => h) clause.20.0;
    (fun h => False.elim (Duper.true_neq_false h)) clause.21.0
Goals accomplished! 🐙

example: ∀ {G : Type} [hG : Group G] (x y : G), x * y * y⁻¹ = x
example {
G: Type
G : 
Type: Type 1
Type} [
hG: Group G
hG : 
Group: Type → Type
Group 
G: Type
G] (
x: G
x 
y: G
y : 
G: Type
G) : 
x: G
x * 
y: G
y * 
y: G
y⁻¹ = 
x: G
x :=
  by
Goals accomplished! 🐙 duper? [
inv_mul_cancel: ∀ {G : Type ?u.19485} [inst : Group G] (a : G), a⁻¹ * a = 1
inv_mul_cancel, 
one_mul: ∀ {M : Type ?u.19819} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul, 
mul_assoc: ∀ {G : Type ?u.20008} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc]
Try this: duper [inv_mul_cancel, one_mul, mul_assoc] {portfolioInstance := 1}
[duper.printProof] Clause #0 (by assumption []): (∀ (x x_1 x_2 : _exTy_0),
        e!_0 (e!_0 x x_1) x_2 = e!_0 x (e!_0 x_1 x_2)) =
      True
[duper.printProof] Clause #1 (by assumption []): (∀ (x : _exTy_0), e!_0 e!_1 x = x) = True
[duper.printProof] Clause #2 (by assumption []): (∀ (x : _exTy_0), e!_0 (e!_2 x) x = e!_1) = True
[duper.printProof] Clause #3 (by assumption []): (¬e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = True
[duper.printProof] Clause #4 (by clausification [3]): (e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = False
[duper.printProof] Clause #5 (by clausification [4]): e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) ≠ e!_3
[duper.printProof] Clause #6 (by clausification [1]): ∀ (a : _exTy_0), (e!_0 e!_1 a = a) = True
[duper.printProof] Clause #7 (by clausification [6]): ∀ (a : _exTy_0), e!_0 e!_1 a = a
[duper.printProof] Clause #8 (by clausification [2]): ∀ (a : _exTy_0), (e!_0 (e!_2 a) a = e!_1) = True
[duper.printProof] Clause #9 (by clausification [8]): ∀ (a : _exTy_0), e!_0 (e!_2 a) a = e!_1
[duper.printProof] Clause #10 (by clausification [0]): ∀ (a : _exTy_0),
      (∀ (x x_1 : _exTy_0), e!_0 (e!_0 a x) x_1 = e!_0 a (e!_0 x x_1)) = True
[duper.printProof] Clause #11 (by clausification [10]): ∀ (a a_1 : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_0 a a_1) x = e!_0 a (e!_0 a_1 x)) = True
[duper.printProof] Clause #12 (by clausification [11]): ∀ (a a_1 a_2 : _exTy_0),
      (e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) = True
[duper.printProof] Clause #13 (by clausification [12]): ∀ (a a_1 a_2 : _exTy_0),
      e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)
[duper.printProof] Clause #14 (by backward demodulation [13, 5]): e!_0 e!_3 (e!_0 e!_4 (e!_2 e!_4)) ≠ e!_3
[duper.printProof] Clause #17 (by superposition [13,
     9]): ∀ (a a_1 : _exTy_0), e!_0 e!_1 a = e!_0 (e!_2 a_1) (e!_0 a_1 a)
[duper.printProof] Clause #29 (by forward demodulation [17, 7]): ∀ (a a_1 : _exTy_0), a = e!_0 (e!_2 a_1) (e!_0 a_1 a)
[duper.printProof] Clause #35 (by superposition [29, 9]): ∀ (a : _exTy_0), a = e!_0 (e!_2 (e!_2 a)) e!_1
[duper.printProof] Clause #93 (by superposition [35, 29]): ∀ (a : _exTy_0), e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) a
[duper.printProof] Clause #137 (by superposition [93, 29]): ∀ (a : _exTy_0), a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) e!_1
[duper.printProof] Clause #179 (by superposition [137, 35]): ∀ (a : _exTy_0), e!_2 (e!_2 a) = a
[duper.printProof] Clause #188 (by backward demodulation [179, 35]): ∀ (a : _exTy_0), a = e!_0 a e!_1
[duper.printProof] Clause #190 (by superposition [179, 9]): ∀ (a : _exTy_0), e!_0 a (e!_2 a) = e!_1
[duper.printProof] Clause #204 (by backward demodulation [190, 14]): e!_0 e!_3 e!_1 ≠ e!_3
[duper.printProof] Clause #217 (by forward demodulation [204, 188]): e!_3 ≠ e!_3
[duper.printProof] Clause #218 (by eliminate resolved literals [217]): False
[duper.proofReconstruction] Collected clauses: [(∀ (x x_1 x_2 : _exTy_0),
         e!_0 (e!_0 x x_1) x_2 = e!_0 x (e!_0 x_1 x_2)) =
       True,
     (∀ (x : _exTy_0), e!_0 e!_1 x = x) = True,
     (∀ (x : _exTy_0), e!_0 (e!_2 x) x = e!_1) = True,
     (¬e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = True,
     (e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = False,
     e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) ≠ e!_3,
     ∀ (a : _exTy_0), (e!_0 e!_1 a = a) = True,
     ∀ (a : _exTy_0), e!_0 e!_1 a = a,
     ∀ (a : _exTy_0), (e!_0 (e!_2 a) a = e!_1) = True,
     ∀ (a : _exTy_0), e!_0 (e!_2 a) a = e!_1,
     ∀ (a : _exTy_0), (∀ (x x_1 : _exTy_0), e!_0 (e!_0 a x) x_1 = e!_0 a (e!_0 x x_1)) = True,
     ∀ (a a_1 : _exTy_0), (∀ (x : _exTy_0), e!_0 (e!_0 a a_1) x = e!_0 a (e!_0 a_1 x)) = True,
     ∀ (a a_1 a_2 : _exTy_0), (e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) = True,
     ∀ (a a_1 a_2 : _exTy_0), e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2),
     e!_0 e!_3 (e!_0 e!_4 (e!_2 e!_4)) ≠ e!_3,
     ∀ (a a_1 : _exTy_0), e!_0 e!_1 a = e!_0 (e!_2 a_1) (e!_0 a_1 a),
     ∀ (a a_1 : _exTy_0), a = e!_0 (e!_2 a_1) (e!_0 a_1 a),
     ∀ (a : _exTy_0), a = e!_0 (e!_2 (e!_2 a)) e!_1,
     ∀ (a : _exTy_0), e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) a,
     ∀ (a : _exTy_0), a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) e!_1,
     ∀ (a : _exTy_0), e!_2 (e!_2 a) = a,
     ∀ (a : _exTy_0), a = e!_0 a e!_1,
     ∀ (a : _exTy_0), e!_0 a (e!_2 a) = e!_1,
     e!_0 e!_3 e!_1 ≠ e!_3,
     e!_3 ≠ e!_3,
     False]
[duper.proofReconstruction] Request [] ↦ [] for False
[duper.proofReconstruction] Request [] ↦ [] for e!_3 ≠ e!_3
[duper.proofReconstruction] Request [] ↦ [] for e!_0 e!_3 e!_1 ≠ e!_3
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_0 a (e!_2 a) = e!_1
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_2 (e!_2 a) = a
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) e!_1
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) a
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), a = e!_0 (e!_2 (e!_2 a)) e!_1
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : _exTy_0), a = e!_0 (e!_2 a_1) (e!_0 a_1 a)
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : _exTy_0), e!_0 e!_1 a = e!_0 (e!_2 a_1) (e!_0 a_1 a)
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 a_2 : _exTy_0), e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 a_2 : _exTy_0),
      (e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_0 a a_1) x = e!_0 a (e!_0 a_1 x)) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0),
      (∀ (x x_1 : _exTy_0), e!_0 (e!_0 a x) x_1 = e!_0 a (e!_0 x x_1)) = True
[duper.proofReconstruction] Request [] ↦ [] for (∀ (x x_1 x_2 : _exTy_0),
        e!_0 (e!_0 x x_1) x_2 = e!_0 x (e!_0 x_1 x_2)) =
      True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_0 (e!_2 a) a = e!_1
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), (e!_0 (e!_2 a) a = e!_1) = True
[duper.proofReconstruction] Request [] ↦ [] for (∀ (x : _exTy_0), e!_0 (e!_2 x) x = e!_1) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_0 e!_1 a = a
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), (e!_0 e!_1 a = a) = True
[duper.proofReconstruction] Request [] ↦ [] for (∀ (x : _exTy_0), e!_0 e!_1 x = x) = True
[duper.proofReconstruction] Request [] ↦ [] for e!_0 e!_3 (e!_0 e!_4 (e!_2 e!_4)) ≠ e!_3
[duper.proofReconstruction] Request [] ↦ [] for e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) ≠ e!_3
[duper.proofReconstruction] Request [] ↦ [] for (e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = False
[duper.proofReconstruction] Request [] ↦ [] for (¬e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), a = e!_0 a e!_1
[duper.proofReconstruction] Reconstructing proof for #0 : [] ↦ [] @ (∀ (x x_1 x_2 : _exTy_0),
        e!_0 (e!_0 x x_1) x_2 = e!_0 x (e!_0 x_1 x_2)) =
      True, Rule Name: assumption
[duper.proofReconstruction] #0's newProof: eq_true «_exHyp_uniq.21408»
[duper.proofReconstruction] Reconstructing proof for #1 : [] ↦ [] @ (∀ (x : _exTy_0), e!_0 e!_1 x = x) =
      True, Rule Name: assumption
[duper.proofReconstruction] #1's newProof: eq_true «_exHyp_uniq.21410»
[duper.proofReconstruction] Reconstructing proof for #2 : [] ↦ [] @ (∀ (x : _exTy_0), e!_0 (e!_2 x) x = e!_1) =
      True, Rule Name: assumption
[duper.proofReconstruction] #2's newProof: eq_true «_exHyp_uniq.21412»
[duper.proofReconstruction] Reconstructing proof for #3 : [] ↦ [] @ (¬e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) =
      True, Rule Name: assumption
[duper.proofReconstruction] #3's newProof: eq_true «_exHyp_uniq.21414»
[duper.proofReconstruction] Instantiating parent (¬e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) =
      True ≡≡ (¬e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #4 : [] ↦ [] @ (e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) =
      False, Rule Name: clausification
[duper.proofReconstruction] #4's newProof: (fun h => Duper.clausify_not h) clause.3.0
[duper.proofReconstruction] Instantiating parent (e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) =
      False ≡≡ (e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) = e!_3) = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #5 : [] ↦ [] @ e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) ≠
      e!_3, Rule Name: clausification
[duper.proofReconstruction] #5's newProof: (fun h => Duper.not_of_eq_false h) clause.4.0
[duper.proofReconstruction] Instantiating parent (∀ (x : _exTy_0), e!_0 e!_1 x = x) =
      True ≡≡ _exTy_0 → (∀ (x : _exTy_0), e!_0 e!_1 x = x) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #6 : [] ↦ [] @ ∀ (a : _exTy_0),
      (e!_0 e!_1 a = a) = True, Rule Name: clausification
[duper.proofReconstruction] #6's newProof: fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.1.0
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      (e!_0 e!_1 a = a) = True ≡≡ ∀ (x_0 : _exTy_0), (fun a => (e!_0 e!_1 a = a) = True) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #7 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_0 e!_1 a = a, Rule Name: clausification
[duper.proofReconstruction] #7's newProof: fun a => (fun h => of_eq_true h) (clause.6.0 a)
[duper.proofReconstruction] Instantiating parent (∀ (x : _exTy_0), e!_0 (e!_2 x) x = e!_1) =
      True ≡≡ _exTy_0 → (∀ (x : _exTy_0), e!_0 (e!_2 x) x = e!_1) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #8 : [] ↦ [] @ ∀ (a : _exTy_0),
      (e!_0 (e!_2 a) a = e!_1) = True, Rule Name: clausification
[duper.proofReconstruction] #8's newProof: fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.2.0
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      (e!_0 (e!_2 a) a = e!_1) =
        True ≡≡ ∀ (x_0 : _exTy_0), (fun a => (e!_0 (e!_2 a) a = e!_1) = True) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #9 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_0 (e!_2 a) a = e!_1, Rule Name: clausification
[duper.proofReconstruction] #9's newProof: fun a => (fun h => of_eq_true h) (clause.8.0 a)
[duper.proofReconstruction] Instantiating parent (∀ (x x_1 x_2 : _exTy_0),
        e!_0 (e!_0 x x_1) x_2 = e!_0 x (e!_0 x_1 x_2)) =
      True ≡≡ _exTy_0 →
      (∀ (x x_1 x_2 : _exTy_0), e!_0 (e!_0 x x_1) x_2 = e!_0 x (e!_0 x_1 x_2)) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #10 : [] ↦ [] @ ∀ (a : _exTy_0),
      (∀ (x x_1 : _exTy_0), e!_0 (e!_0 a x) x_1 = e!_0 a (e!_0 x x_1)) = True, Rule Name: clausification
[duper.proofReconstruction] #10's newProof: fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.0.0
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      (∀ (x x_1 : _exTy_0), e!_0 (e!_0 a x) x_1 = e!_0 a (e!_0 x x_1)) =
        True ≡≡ ∀ (x_0 : _exTy_0),
      _exTy_0 →
        (fun a => (∀ (x x_2 : _exTy_0), e!_0 (e!_0 a x) x_2 = e!_0 a (e!_0 x x_2)) = True) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #11 : [] ↦ [] @ ∀ (a a_1 : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_0 a a_1) x = e!_0 a (e!_0 a_1 x)) = True, Rule Name: clausification
[duper.proofReconstruction] #11's newProof: fun a a_1 =>
      (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.10.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_0 a a_1) x = e!_0 a (e!_0 a_1 x)) =
        True ≡≡ ∀ (x_0 x_1 : _exTy_0),
      _exTy_0 →
        (fun a a_1 => (∀ (x : _exTy_0), e!_0 (e!_0 a a_1) x = e!_0 a (e!_0 a_1 x)) = True) x_0
          x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #12 : [] ↦ [] @ ∀ (a a_1 a_2 : _exTy_0),
      (e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) = True, Rule Name: clausification
[duper.proofReconstruction] #12's newProof: fun a a_1 a_2 =>
      (fun h => Duper.clausify_forall ((fun x_0 x_1 x_2 => x_2) a a_1 a_2) h) (clause.11.0 a a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 a_2 : _exTy_0),
      (e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) =
        True ≡≡ ∀ (x_0 x_1 x_2 : _exTy_0),
      (fun a a_1 a_2 => (e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) = True) x_0 x_1 x_2 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #13 : [] ↦ [] @ ∀ (a a_1 a_2 : _exTy_0),
      e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2), Rule Name: clausification
[duper.proofReconstruction] #13's newProof: fun a a_1 a_2 => (fun h => of_eq_true h) (clause.12.0 a a_1 a_2)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 a_2 : _exTy_0),
      e!_0 (e!_0 a a_1) a_2 =
        e!_0 a
          (e!_0 a_1
            a_2) ≡≡ (fun a a_1 a_2 => e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) e!_3 e!_4
      (e!_2 e!_4) with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) ≠
      e!_3 ≡≡ e!_0 (e!_0 e!_3 e!_4) (e!_2 e!_4) ≠ e!_3 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #14 : [] ↦ [] @ e!_0 e!_3 (e!_0 e!_4 (e!_2 e!_4)) ≠
      e!_3, Rule Name: backward demodulation
[duper.proofReconstruction] #14's newProof: (fun heq =>
        (fun h => Eq.mp (congrArg (fun x => x ≠ e!_3) heq) h) clause.5.0)
      (clause.13.0 e!_3 e!_4 (e!_2 e!_4))
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 a_2 : _exTy_0),
      e!_0 (e!_0 a a_1) a_2 =
        e!_0 a
          (e!_0 a_1
            a_2) ≡≡ ∀ (x_0 x_1 : _exTy_0),
      (fun a a_1 a_2 => e!_0 (e!_0 a a_1) a_2 = e!_0 a (e!_0 a_1 a_2)) (e!_2 x_1) x_1 x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_0 (e!_2 a) a =
        e!_1 ≡≡ _exTy_0 → ∀ (x_1 : _exTy_0), (fun a => e!_0 (e!_2 a) a = e!_1) x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #17 : [] ↦ [] @ ∀ (a a_1 : _exTy_0),
      e!_0 e!_1 a = e!_0 (e!_2 a_1) (e!_0 a_1 a), Rule Name: superposition
[duper.proofReconstruction] #17's newProof: fun a a_1 =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_0 x a = e!_0 (e!_2 a_1) (e!_0 a_1 a)) heq) h)
            (clause.13.0 (e!_2 a_1) a_1 a))
        (clause.9.0 a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : _exTy_0),
      e!_0 e!_1 a =
        e!_0 (e!_2 a_1)
          (e!_0 a_1
            a) ≡≡ ∀ (x_0 x_1 : _exTy_0),
      (fun a a_1 => e!_0 e!_1 a = e!_0 (e!_2 a_1) (e!_0 a_1 a)) x_0 x_1 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_0 e!_1 a = a ≡≡ ∀ (x_0 : _exTy_0), _exTy_0 → (fun a => e!_0 e!_1 a = a) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #29 : [] ↦ [] @ ∀ (a a_1 : _exTy_0),
      a = e!_0 (e!_2 a_1) (e!_0 a_1 a), Rule Name: forward demodulation
[duper.proofReconstruction] #29's newProof: fun a a_1 =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => x = e!_0 (e!_2 a_1) (e!_0 a_1 a)) heq) h) (clause.17.0 a a_1))
        (clause.7.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : _exTy_0),
      a =
        e!_0 (e!_2 a_1)
          (e!_0 a_1
            a) ≡≡ ∀ (x_0 : _exTy_0),
      (fun a a_1 => a = e!_0 (e!_2 a_1) (e!_0 a_1 a)) x_0 (e!_2 x_0) with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_0 (e!_2 a) a = e!_1 ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_0 (e!_2 a) a = e!_1) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #35 : [] ↦ [] @ ∀ (a : _exTy_0),
      a = e!_0 (e!_2 (e!_2 a)) e!_1, Rule Name: superposition
[duper.proofReconstruction] #35's newProof: fun a =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => a = e!_0 (e!_2 (e!_2 a)) x) heq) h) (clause.29.0 a (e!_2 a)))
        (clause.9.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      a =
        e!_0 (e!_2 (e!_2 a))
          e!_1 ≡≡ ∀ (x_0 : _exTy_0), (fun a => a = e!_0 (e!_2 (e!_2 a)) e!_1) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : _exTy_0),
      a =
        e!_0 (e!_2 a_1)
          (e!_0 a_1
            a) ≡≡ ∀ (x_0 : _exTy_0),
      (fun a a_1 => a = e!_0 (e!_2 a_1) (e!_0 a_1 a)) e!_1 (e!_2 (e!_2 x_0)) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #93 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) a, Rule Name: superposition
[duper.proofReconstruction] #93's newProof: fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) x) (Eq.symm heq)) h)
            (clause.29.0 e!_1 (e!_2 (e!_2 a))))
        (clause.35.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_1 =
        e!_0 (e!_2 (e!_2 (e!_2 a)))
          a ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) a) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : _exTy_0),
      a =
        e!_0 (e!_2 a_1)
          (e!_0 a_1
            a) ≡≡ ∀ (x_0 : _exTy_0),
      (fun a a_1 => a = e!_0 (e!_2 a_1) (e!_0 a_1 a)) x_0 (e!_2 (e!_2 (e!_2 x_0))) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #137 : [] ↦ [] @ ∀ (a : _exTy_0),
      a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) e!_1, Rule Name: superposition
[duper.proofReconstruction] #137's newProof: fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) x) (Eq.symm heq)) h)
            (clause.29.0 a (e!_2 (e!_2 (e!_2 a)))))
        (clause.93.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      a =
        e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a))))
          e!_1 ≡≡ ∀ (x_0 : _exTy_0), (fun a => a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) e!_1) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      a =
        e!_0 (e!_2 (e!_2 a))
          e!_1 ≡≡ ∀ (x_0 : _exTy_0), (fun a => a = e!_0 (e!_2 (e!_2 a)) e!_1) (e!_2 (e!_2 x_0)) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #179 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_2 (e!_2 a) = a, Rule Name: superposition
[duper.proofReconstruction] #179's newProof: fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_2 (e!_2 a) = x) (Eq.symm heq)) h) (clause.35.0 (e!_2 (e!_2 a))))
        (clause.137.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 (e!_2 a) = a ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_2 (e!_2 a) = a) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      a =
        e!_0 (e!_2 (e!_2 a))
          e!_1 ≡≡ ∀ (x_0 : _exTy_0), (fun a => a = e!_0 (e!_2 (e!_2 a)) e!_1) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #188 : [] ↦ [] @ ∀ (a : _exTy_0),
      a = e!_0 a e!_1, Rule Name: backward demodulation
[duper.proofReconstruction] #188's newProof: fun a =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => a = e!_0 x e!_1) heq) h) (clause.35.0 a)) (clause.179.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 (e!_2 a) = a ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_2 (e!_2 a) = a) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_0 (e!_2 a) a = e!_1 ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_0 (e!_2 a) a = e!_1) (e!_2 x_0) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #190 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_0 a (e!_2 a) = e!_1, Rule Name: superposition
[duper.proofReconstruction] #190's newProof: fun a =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => e!_0 x (e!_2 a) = e!_1) heq) h) (clause.9.0 (e!_2 a)))
        (clause.179.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_0 a (e!_2 a) = e!_1 ≡≡ (fun a => e!_0 a (e!_2 a) = e!_1) e!_4 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent e!_0 e!_3 (e!_0 e!_4 (e!_2 e!_4)) ≠
      e!_3 ≡≡ e!_0 e!_3 (e!_0 e!_4 (e!_2 e!_4)) ≠ e!_3 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #204 : [] ↦ [] @ e!_0 e!_3 e!_1 ≠
      e!_3, Rule Name: backward demodulation
[duper.proofReconstruction] #204's newProof: (fun heq =>
        (fun h => Eq.mp (congrArg (fun x => e!_0 e!_3 x ≠ e!_3) heq) h) clause.14.0)
      (clause.190.0 e!_4)
[duper.proofReconstruction] Instantiating parent e!_0 e!_3 e!_1 ≠ e!_3 ≡≡ e!_0 e!_3 e!_1 ≠ e!_3 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      a = e!_0 a e!_1 ≡≡ (fun a => a = e!_0 a e!_1) e!_3 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #217 : [] ↦ [] @ e!_3 ≠ e!_3, Rule Name: forward demodulation
[duper.proofReconstruction] #217's newProof: (fun heq =>
        (fun h => Eq.mp (congrArg (fun x => x ≠ e!_3) (Eq.symm heq)) h) clause.204.0)
      (clause.188.0 e!_3)
[duper.proofReconstruction] Instantiating parent e!_3 ≠ e!_3 ≡≡ e!_3 ≠ e!_3 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #218 : [] ↦ [] @ False, Rule Name: eliminate resolved literals
[duper.proofReconstruction] #218's newProof: (fun h => False.elim (h rfl)) clause.217.0
[duper.proofReconstruction] Proof: let clause.0.0 := eq_true «_exHyp_uniq.21408»;
    let clause.1.0 := eq_true «_exHyp_uniq.21410»;
    let clause.2.0 := eq_true «_exHyp_uniq.21412»;
    let clause.3.0 := eq_true «_exHyp_uniq.21414»;
    let clause.4.0 := (fun h => Duper.clausify_not h) clause.3.0;
    let clause.5.0 := (fun h => Duper.not_of_eq_false h) clause.4.0;
    let clause.6.0 := fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.1.0;
    let clause.7.0 := fun a => (fun h => of_eq_true h) (clause.6.0 a);
    let clause.8.0 := fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.2.0;
    let clause.9.0 := fun a => (fun h => of_eq_true h) (clause.8.0 a);
    let clause.10.0 := fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.0.0;
    let clause.11.0 := fun a a_1 => (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.10.0 a);
    let clause.12.0 := fun a a_1 a_2 =>
      (fun h => Duper.clausify_forall ((fun x_0 x_1 x_2 => x_2) a a_1 a_2) h) (clause.11.0 a a_1);
    let clause.13.0 := fun a a_1 a_2 => (fun h => of_eq_true h) (clause.12.0 a a_1 a_2);
    let clause.14.0 :=
      (fun heq => (fun h => Eq.mp (congrArg (fun x => x ≠ e!_3) heq) h) clause.5.0) (clause.13.0 e!_3 e!_4 (e!_2 e!_4));
    let clause.17.0 := fun a a_1 =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_0 x a = e!_0 (e!_2 a_1) (e!_0 a_1 a)) heq) h)
            (clause.13.0 (e!_2 a_1) a_1 a))
        (clause.9.0 a_1);
    let clause.29.0 := fun a a_1 =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => x = e!_0 (e!_2 a_1) (e!_0 a_1 a)) heq) h) (clause.17.0 a a_1))
        (clause.7.0 a);
    let clause.35.0 := fun a =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => a = e!_0 (e!_2 (e!_2 a)) x) heq) h) (clause.29.0 a (e!_2 a)))
        (clause.9.0 a);
    let clause.93.0 := fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_1 = e!_0 (e!_2 (e!_2 (e!_2 a))) x) (Eq.symm heq)) h)
            (clause.29.0 e!_1 (e!_2 (e!_2 a))))
        (clause.35.0 a);
    let clause.137.0 := fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => a = e!_0 (e!_2 (e!_2 (e!_2 (e!_2 a)))) x) (Eq.symm heq)) h)
            (clause.29.0 a (e!_2 (e!_2 (e!_2 a)))))
        (clause.93.0 a);
    let clause.179.0 := fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_2 (e!_2 a) = x) (Eq.symm heq)) h) (clause.35.0 (e!_2 (e!_2 a))))
        (clause.137.0 a);
    let clause.188.0 := fun a =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => a = e!_0 x e!_1) heq) h) (clause.35.0 a)) (clause.179.0 a);
    let clause.190.0 := fun a =>
      (fun heq => (fun h => Eq.mp (congrArg (fun x => e!_0 x (e!_2 a) = e!_1) heq) h) (clause.9.0 (e!_2 a)))
        (clause.179.0 a);
    let clause.204.0 :=
      (fun heq => (fun h => Eq.mp (congrArg (fun x => e!_0 e!_3 x ≠ e!_3) heq) h) clause.14.0) (clause.190.0 e!_4);
    let clause.217.0 :=
      (fun heq => (fun h => Eq.mp (congrArg (fun x => x ≠ e!_3) (Eq.symm heq)) h) clause.204.0) (clause.188.0 e!_3);
    (fun h => False.elim (h rfl)) clause.217.0
Goals accomplished! 🐙

example: ∀ (a b : ℝ), |a| - |b| ≤ |a - b|
example (
a: ℝ
a 
b: ℝ
b : 
ℝ: Type
ℝ) : |
a: ℝ
a| - |
b: ℝ
b| ≤ |
a: ℝ
a - 
b: ℝ
b| := by
Goals accomplished! 🐙
  duper? [
abs_le: ∀ {α : Type ?u.34863} [inst : LinearOrderedAddCommGroup α] {a b : α}, |a| ≤ b ↔ -b ≤ a ∧ a ≤ b
abs_le, 
abs_sub_abs_le_abs_sub: ∀ {α : Type ?u.34941} [inst : LinearOrderedAddCommGroup α] (a b : α), |a| - |b| ≤ |a - b|
abs_sub_abs_le_abs_sub]
[duper.printProof] Clause #0 (by assumption []): (∀ (x x_1 : _exTy_0),
        e!_0 (e!_1 (e!_2 x) (e!_2 x_1)) (e!_2 (e!_1 x x_1))) =
      True
[duper.printProof] Clause #2 (by assumption []): (¬e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5))) = True
[duper.printProof] Clause #3 (by clausification [2]): e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5)) =
      False
[duper.printProof] Clause #4 (by clausification [0]): ∀ (a : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 x)) (e!_2 (e!_1 a x))) = True
[duper.printProof] Clause #5 (by clausification [4]): ∀ (a a_1 : _exTy_0),
      e!_0 (e!_1 (e!_2 a) (e!_2 a_1)) (e!_2 (e!_1 a a_1)) = True
[duper.printProof] Clause #6 (by superposition [5, 3]): True = False
[duper.printProof] Clause #7 (by clausification [6]): False
[duper.proofReconstruction] Collected clauses: [(∀ (x x_1 : _exTy_0),
         e!_0 (e!_1 (e!_2 x) (e!_2 x_1)) (e!_2 (e!_1 x x_1))) =
       True,
     (¬e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5))) = True,
     e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5)) = False,
     ∀ (a : _exTy_0), (∀ (x : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 x)) (e!_2 (e!_1 a x))) = True,
     ∀ (a a_1 : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 a_1)) (e!_2 (e!_1 a a_1)) = True,
     True = False,
     False]
[duper.proofReconstruction] Request [] ↦ [] for False
[duper.proofReconstruction] Request [] ↦ [] for True = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a a_1 : _exTy_0),
      e!_0 (e!_1 (e!_2 a) (e!_2 a_1)) (e!_2 (e!_1 a a_1)) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 x)) (e!_2 (e!_1 a x))) = True
[duper.proofReconstruction] Request [] ↦ [] for (∀ (x x_1 : _exTy_0),
        e!_0 (e!_1 (e!_2 x) (e!_2 x_1)) (e!_2 (e!_1 x x_1))) =
      True
[duper.proofReconstruction] Request [] ↦ [] for e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5)) = False
[duper.proofReconstruction] Request [] ↦ [] for (¬e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5))) = True
[duper.proofReconstruction] Reconstructing proof for #0 : [] ↦ [] @ (∀ (x x_1 : _exTy_0),
        e!_0 (e!_1 (e!_2 x) (e!_2 x_1)) (e!_2 (e!_1 x x_1))) =
      True, Rule Name: assumption
[duper.proofReconstruction] #0's newProof: eq_true «_exHyp_uniq.35868»
[duper.proofReconstruction] Reconstructing proof for #2 : [] ↦ [] @ (¬e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5))
          (e!_2 (e!_1 e!_4 e!_5))) =
      True, Rule Name: assumption
[duper.proofReconstruction] #2's newProof: eq_true «_exHyp_uniq.35872»
[duper.proofReconstruction] Instantiating parent (¬e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5))) =
      True ≡≡ (¬e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5))) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #3 : [] ↦ [] @ e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5))
        (e!_2 (e!_1 e!_4 e!_5)) =
      False, Rule Name: clausification
[duper.proofReconstruction] #3's newProof: (fun h => Duper.clausify_not h) clause.2.0
[duper.proofReconstruction] Instantiating parent (∀ (x x_1 : _exTy_0),
        e!_0 (e!_1 (e!_2 x) (e!_2 x_1)) (e!_2 (e!_1 x x_1))) =
      True ≡≡ _exTy_0 →
      (∀ (x x_1 : _exTy_0), e!_0 (e!_1 (e!_2 x) (e!_2 x_1)) (e!_2 (e!_1 x x_1))) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #4 : [] ↦ [] @ ∀ (a : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 x)) (e!_2 (e!_1 a x))) = True, Rule Name: clausification
[duper.proofReconstruction] #4's newProof: fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.0.0
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      (∀ (x : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 x)) (e!_2 (e!_1 a x))) =
        True ≡≡ ∀ (x_0 : _exTy_0),
      _exTy_0 →
        (fun a => (∀ (x : _exTy_0), e!_0 (e!_1 (e!_2 a) (e!_2 x)) (e!_2 (e!_1 a x))) = True)
          x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #5 : [] ↦ [] @ ∀ (a a_1 : _exTy_0),
      e!_0 (e!_1 (e!_2 a) (e!_2 a_1)) (e!_2 (e!_1 a a_1)) = True, Rule Name: clausification
[duper.proofReconstruction] #5's newProof: fun a a_1 =>
      (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.4.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a a_1 : _exTy_0),
      e!_0 (e!_1 (e!_2 a) (e!_2 a_1)) (e!_2 (e!_1 a a_1)) =
        True ≡≡ (fun a a_1 => e!_0 (e!_1 (e!_2 a) (e!_2 a_1)) (e!_2 (e!_1 a a_1)) = True) e!_4
      e!_5 with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5)) =
      False ≡≡ e!_0 (e!_1 (e!_2 e!_4) (e!_2 e!_5)) (e!_2 (e!_1 e!_4 e!_5)) = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #6 : [] ↦ [] @ True = False, Rule Name: superposition
[duper.proofReconstruction] #6's newProof: (fun heq =>
        (fun h => Eq.mp (congrArg (fun x => x = False) heq) h) clause.3.0)
      (clause.5.0 e!_4 e!_5)
[duper.proofReconstruction] Instantiating parent True = False ≡≡ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #7 : [] ↦ [] @ False, Rule Name: clausification
[duper.proofReconstruction] #7's newProof: (fun h => False.elim (Duper.true_neq_false h)) clause.6.0
[duper.proofReconstruction] Proof: let clause.0.0 := eq_true «_exHyp_uniq.35868»;
    let clause.2.0 := eq_true «_exHyp_uniq.35872»;
    let clause.3.0 := (fun h => Duper.clausify_not h) clause.2.0;
    let clause.4.0 := fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.0.0;
    let clause.5.0 := fun a a_1 => (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.4.0 a);
    let clause.6.0 :=
      (fun heq => (fun h => Eq.mp (congrArg (fun x => x = False) heq) h) clause.3.0) (clause.5.0 e!_4 e!_5);
    (fun h => False.elim (Duper.true_neq_false h)) clause.6.0
Try this: duper [abs_le, abs_sub_abs_le_abs_sub] {portfolioInstance := 1}
Goals accomplished! 🐙

/- Attempting to call `duper` directly on the original goal will fail because it isn't able to generate a
   counterexample to Surjf on its own. But if we provide the counterexample, `duper` can solve from there. -/
example : ∀ f : α → Set α, ¬Surjective f := by
Goals accomplished! 🐙
  intro 
f: α → Set α
f 
Surjf: Surjective f
Surjf
κ: Type uκ
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
Cl: CliffordAlgebra Q
Ex: ExteriorAlgebra R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
α: Type u_1
f: α → Set α
Surjf: Surjective f
False
  have 
counterexample: ∃ a, f a = {i | i ∉ f i}
counterexample := 
Surjf: Surjective f
Surjf {
i: α
i | 
i: α
i ∉ 
f: α → Set α
f 
i: α
i}
κ: Type uκ
R: Type uR
inst✝⁶: CommRing R
inst✝⁵: Invertible 2
inst✝⁴: Nontrivial R
M: Type uM
inst✝³: AddCommGroup M
inst✝²: Module R M
Q: QuadraticForm R M
Cl: CliffordAlgebra Q
Ex: ExteriorAlgebra R M
inst✝¹: Module.Finite R M
inst✝: Module.Free R M
α: Type u_1
f: α → Set α
Surjf: Surjective f
counterexample: ∃ a, f a = {i | i ∉ f i}
False
  duper [
Set.mem_setOf_eq: ∀ {α : Type ?u.39890} {x : α} {p : α → Prop}, (x ∈ {y | p y}) = p x
Set.mem_setOf_eq, 
counterexample: ∃ a, f a = {i | i ∉ f i}
counterexample]
[duper.printProof] Clause #0 (by assumption []): (e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) = True
[duper.printProof] Clause #1 (by assumption []): (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop),
        e!_2 x (e!_1 fun eb!_2 => x_1 eb!_2) = x_1 x) =
      True
[duper.printProof] Clause #4 (by clausification [0]): e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)
[duper.printProof] Clause #5 (by betaEtaReduce [1]): (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop),
        e!_2 x (e!_1 x_1) = x_1 x) =
      True
[duper.printProof] Clause #6 (by clausification [5]): ∀ (a : _exTy_0),
      (∀ (x : _exTy_0 → Prop), e!_2 a (e!_1 x) = x a) = True
[duper.printProof] Clause #7 (by clausification [6]): ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop),
      (e!_2 a (e!_1 a_1) = a_1 a) = True
[duper.printProof] Clause #8 (by clausification [7]): ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop), e!_2 a (e!_1 a_1) = a_1 a
[duper.printProof] Clause #12 (by superposition [8, 4]): ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬e!_2 a (e!_0 a)
[duper.printProof] Clause #23 (by identity loobHoist [12]): ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬True ∨ e!_2 a (e!_0 a) = False
[duper.printProof] Clause #24 (by identity boolHoist [12]): ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬False ∨ e!_2 a (e!_0 a) = True
[duper.printProof] Clause #25 (by bool simp [23]): ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = False ∨ e!_2 a (e!_0 a) = False
[duper.printProof] Clause #35 (by bool simp [24]): ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = True ∨ e!_2 a (e!_0 a) = True
[duper.printProof] Clause #37 (by equality factoring [35]): True ≠ True ∨ e!_2 e?_0 (e!_0 e?_0) = True
[duper.printProof] Clause #38 (by clausification [37]): e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False ∨ True = False
[duper.printProof] Clause #40 (by clausification [38]): e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False
[duper.printProof] Clause #41 (by clausification [40]): e!_2 e?_0 (e!_0 e?_0) = True
[duper.printProof] Clause #42 (by superposition [41, 25]): True = False ∨ True = False
[duper.printProof] Clause #43 (by clausification [42]): True = False
[duper.printProof] Clause #44 (by clausification [43]): False
[duper.proofReconstruction] Collected clauses: [(e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) = True,
     (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop), e!_2 x (e!_1 fun eb!_2 => x_1 eb!_2) = x_1 x) = True,
     e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0),
     (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop), e!_2 x (e!_1 x_1) = x_1 x) = True,
     ∀ (a : _exTy_0), (∀ (x : _exTy_0 → Prop), e!_2 a (e!_1 x) = x a) = True,
     ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop), (e!_2 a (e!_1 a_1) = a_1 a) = True,
     ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop), e!_2 a (e!_1 a_1) = a_1 a,
     ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬e!_2 a (e!_0 a),
     ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬True ∨ e!_2 a (e!_0 a) = False,
     ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬False ∨ e!_2 a (e!_0 a) = True,
     ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = False ∨ e!_2 a (e!_0 a) = False,
     ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = True ∨ e!_2 a (e!_0 a) = True,
     True ≠ True ∨ e!_2 e?_0 (e!_0 e?_0) = True,
     e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False ∨ True = False,
     e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False,
     e!_2 e?_0 (e!_0 e?_0) = True,
     True = False ∨ True = False,
     True = False,
     False]
[duper.proofReconstruction] Request [] ↦ [] for False
[duper.proofReconstruction] Request [] ↦ [] for True = False
[duper.proofReconstruction] Request [] ↦ [] for True = False ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for e!_2 e?_0 (e!_0 e?_0) = True
[duper.proofReconstruction] Request [] ↦ [] for e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False ∨ True = False
[duper.proofReconstruction] Request [] ↦ [] for True ≠ True ∨ e!_2 e?_0 (e!_0 e?_0) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = True ∨ e!_2 a (e!_0 a) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬False ∨ e!_2 a (e!_0 a) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬e!_2 a (e!_0 a)
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop), e!_2 a (e!_1 a_1) = a_1 a
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop),
      (e!_2 a (e!_1 a_1) = a_1 a) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), (∀ (x : _exTy_0 → Prop), e!_2 a (e!_1 x) = x a) = True
[duper.proofReconstruction] Request [] ↦ [] for (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop), e!_2 x (e!_1 x_1) = x_1 x) =
      True
[duper.proofReconstruction] Request [] ↦ [] for (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop),
        e!_2 x (e!_1 fun eb!_2 => x_1 eb!_2) = x_1 x) =
      True
[duper.proofReconstruction] Request [] ↦ [] for e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)
[duper.proofReconstruction] Request [] ↦ [] for (e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) = True
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = False ∨ e!_2 a (e!_0 a) = False
[duper.proofReconstruction] Request [] ↦ [] for ∀ (a : _exTy_0), e!_2 a (e!_0 e?_0) = ¬True ∨ e!_2 a (e!_0 a) = False
[duper.proofReconstruction] Reconstructing proof for #0 : [] ↦ [] @ (e!_0 e?_0 =
        e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) =
      True, Rule Name: assumption
[duper.proofReconstruction] #0's newProof: eq_true «_exHyp_uniq.40213»
[duper.proofReconstruction] Reconstructing proof for #1 : [] ↦ [] @ (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop),
        e!_2 x (e!_1 fun eb!_2 => x_1 eb!_2) = x_1 x) =
      True, Rule Name: assumption
[duper.proofReconstruction] #1's newProof: eq_true «_exHyp_uniq.40215»
[duper.proofReconstruction] Instantiating parent (e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) =
      True ≡≡ (e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #4 : [] ↦ [] @ e!_0 e?_0 =
      e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0), Rule Name: clausification
[duper.proofReconstruction] #4's newProof: (fun h => of_eq_true h) clause.0.0
[duper.proofReconstruction] Instantiating parent (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop),
        e!_2 x (e!_1 fun eb!_2 => x_1 eb!_2) = x_1 x) =
      True ≡≡ (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop), e!_2 x (e!_1 fun eb!_2 => x_1 eb!_2) = x_1 x) =
      True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #5 : [] ↦ [] @ (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop),
        e!_2 x (e!_1 x_1) = x_1 x) =
      True, Rule Name: betaEtaReduce
[duper.proofReconstruction] #5's newProof: clause.1.0
[duper.proofReconstruction] Instantiating parent (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop), e!_2 x (e!_1 x_1) = x_1 x) =
      True ≡≡ _exTy_0 →
      (∀ (x : _exTy_0) (x_1 : _exTy_0 → Prop), e!_2 x (e!_1 x_1) = x_1 x) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #6 : [] ↦ [] @ ∀ (a : _exTy_0),
      (∀ (x : _exTy_0 → Prop), e!_2 a (e!_1 x) = x a) = True, Rule Name: clausification
[duper.proofReconstruction] #6's newProof: fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.5.0
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      (∀ (x : _exTy_0 → Prop), e!_2 a (e!_1 x) = x a) =
        True ≡≡ ∀ (x_0 : _exTy_0),
      (_exTy_0 → Prop) → (fun a => (∀ (x : _exTy_0 → Prop), e!_2 a (e!_1 x) = x a) = True) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #7 : [] ↦ [] @ ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop),
      (e!_2 a (e!_1 a_1) = a_1 a) = True, Rule Name: clausification
[duper.proofReconstruction] #7's newProof: fun a a_1 =>
      (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.6.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop),
      (e!_2 a (e!_1 a_1) = a_1 a) =
        True ≡≡ ∀ (x_0 : _exTy_0) (x_1 : _exTy_0 → Prop),
      (fun a a_1 => (e!_2 a (e!_1 a_1) = a_1 a) = True) x_0 x_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #8 : [] ↦ [] @ ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop),
      e!_2 a (e!_1 a_1) = a_1 a, Rule Name: clausification
[duper.proofReconstruction] #8's newProof: fun a a_1 => (fun h => of_eq_true h) (clause.7.0 a a_1)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0) (a_1 : _exTy_0 → Prop),
      e!_2 a (e!_1 a_1) =
        a_1
          a ≡≡ ∀ (x_0 : _exTy_0),
      (fun a a_1 => e!_2 a (e!_1 a_1) = a_1 a) x_0 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0) with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent e!_0 e?_0 =
      e!_1 fun eb!_0 =>
        ¬e!_2 eb!_0
            (e!_0 eb!_0) ≡≡ _exTy_0 → e!_0 e?_0 = e!_1 fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0) with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #12 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬e!_2 a (e!_0 a), Rule Name: superposition
[duper.proofReconstruction] #12's newProof: fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_2 a x = (fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) a) (Eq.symm heq)) h)
            (clause.8.0 a fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)))
        clause.4.0
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) =
        ¬e!_2 a
            (e!_0 a) ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_2 a (e!_0 e?_0) = ¬e!_2 a (e!_0 a)) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #23 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬True ∨ e!_2 a (e!_0 a) = False, Rule Name: identity loobHoist
[duper.proofReconstruction] #23's newProof: fun a =>
      (fun h => Duper.loob_hoist_proof (fun h => e!_2 a (e!_0 e?_0) = ¬h) (e!_2 a (e!_0 a)) h) (clause.12.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) =
        ¬e!_2 a
            (e!_0 a) ≡≡ ∀ (x_0 : _exTy_0), (fun a => e!_2 a (e!_0 e?_0) = ¬e!_2 a (e!_0 a)) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #24 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬False ∨ e!_2 a (e!_0 a) = True, Rule Name: identity boolHoist
[duper.proofReconstruction] #24's newProof: fun a =>
      (fun h => Duper.bool_hoist_proof (fun h => e!_2 a (e!_0 e?_0) = ¬h) (e!_2 a (e!_0 a)) h) (clause.12.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬True ∨
        e!_2 a (e!_0 a) =
          False ≡≡ ∀ (x_0 : _exTy_0),
      (fun a => e!_2 a (e!_0 e?_0) = ¬True ∨ e!_2 a (e!_0 a) = False) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #25 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = False ∨ e!_2 a (e!_0 a) = False, Rule Name: bool simp
[duper.proofReconstruction] #25's newProof: fun a =>
      (fun h =>
          Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => e!_2 a (e!_0 e?_0) = x) Duper.rule14Theorem) h))
            fun h => Or.inr h)
        (clause.23.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = ¬False ∨
        e!_2 a (e!_0 a) =
          True ≡≡ ∀ (x_0 : _exTy_0),
      (fun a => e!_2 a (e!_0 e?_0) = ¬False ∨ e!_2 a (e!_0 a) = True) x_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #35 : [] ↦ [] @ ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = True ∨ e!_2 a (e!_0 a) = True, Rule Name: bool simp
[duper.proofReconstruction] #35's newProof: fun a =>
      (fun h =>
          Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => e!_2 a (e!_0 e?_0) = x) Duper.rule7Theorem) h)) fun h =>
            Or.inr h)
        (clause.24.0 a)
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = True ∨
        e!_2 a (e!_0 a) =
          True ≡≡ (fun a => e!_2 a (e!_0 e?_0) = True ∨ e!_2 a (e!_0 a) = True) e?_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #37 : [] ↦ [] @ True ≠ True ∨
      e!_2 e?_0 (e!_0 e?_0) = True, Rule Name: equality factoring
[duper.proofReconstruction] #37's newProof: (fun h =>
        Or.elim h (fun h => Duper.equality_factoring_soundness1 True h) fun h => Or.inr h)
      (clause.35.0 e?_0)
[duper.proofReconstruction] Instantiating parent True ≠ True ∨
      e!_2 e?_0 (e!_0 e?_0) = True ≡≡ True ≠ True ∨ e!_2 e?_0 (e!_0 e?_0) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #38 : [] ↦ [] @ e!_2 e?_0 (e!_0 e?_0) = True ∨
      True = False ∨ True = False, Rule Name: clausification
[duper.proofReconstruction] #38's newProof: (fun h =>
        Or.elim h (fun h => Or.inr (Duper.clausify_prop_inequality1 h)) fun h => Or.inl h)
      clause.37.0
[duper.proofReconstruction] Instantiating parent e!_2 e?_0 (e!_0 e?_0) = True ∨
      True = False ∨ True = False ≡≡ e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False ∨ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #40 : [] ↦ [] @ e!_2 e?_0 (e!_0 e?_0) = True ∨
      True = False, Rule Name: clausification
[duper.proofReconstruction] #40's newProof: (fun h =>
        Or.elim h (fun h => Or.inl h) fun h =>
          Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => Or.inr h)
      clause.38.0
[duper.proofReconstruction] Instantiating parent e!_2 e?_0 (e!_0 e?_0) = True ∨
      True = False ≡≡ e!_2 e?_0 (e!_0 e?_0) = True ∨ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #41 : [] ↦ [] @ e!_2 e?_0 (e!_0 e?_0) =
      True, Rule Name: clausification
[duper.proofReconstruction] #41's newProof: (fun h =>
        Or.elim h (fun h => h) fun h => False.elim (Duper.true_neq_false h))
      clause.40.0
[duper.proofReconstruction] Instantiating parent e!_2 e?_0 (e!_0 e?_0) =
      True ≡≡ e!_2 e?_0 (e!_0 e?_0) = True with param subst [] ↦ []
[duper.proofReconstruction] Instantiating parent ∀ (a : _exTy_0),
      e!_2 a (e!_0 e?_0) = False ∨
        e!_2 a (e!_0 a) =
          False ≡≡ (fun a => e!_2 a (e!_0 e?_0) = False ∨ e!_2 a (e!_0 a) = False) e?_0 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #42 : [] ↦ [] @ True = False ∨
      True = False, Rule Name: superposition
[duper.proofReconstruction] #42's newProof: (fun heq =>
        (fun h =>
            Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => x = False) heq) h)) fun h =>
              Or.inr (Eq.mp (congrArg (fun x => x = False) heq) h))
          (clause.25.0 e?_0))
      clause.41.0
[duper.proofReconstruction] Instantiating parent True = False ∨
      True = False ≡≡ True = False ∨ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #43 : [] ↦ [] @ True = False, Rule Name: clausification
[duper.proofReconstruction] #43's newProof: (fun h =>
        Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => h)
      clause.42.0
[duper.proofReconstruction] Instantiating parent True = False ≡≡ True = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #44 : [] ↦ [] @ False, Rule Name: clausification
[duper.proofReconstruction] #44's newProof: (fun h => False.elim (Duper.true_neq_false h)) clause.43.0
[duper.proofReconstruction] Proof: let clause.0.0 := eq_true «_exHyp_uniq.40213»;
    let clause.1.0 := eq_true «_exHyp_uniq.40215»;
    let clause.4.0 := (fun h => of_eq_true h) clause.0.0;
    let clause.5.0 := clause.1.0;
    let clause.6.0 := fun a => (fun h => Duper.clausify_forall ((fun x_0 => x_0) a) h) clause.5.0;
    let clause.7.0 := fun a a_1 => (fun h => Duper.clausify_forall ((fun x_0 x_1 => x_1) a a_1) h) (clause.6.0 a);
    let clause.8.0 := fun a a_1 => (fun h => of_eq_true h) (clause.7.0 a a_1);
    let clause.12.0 := fun a =>
      (fun heq =>
          (fun h => Eq.mp (congrArg (fun x => e!_2 a x = (fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)) a) (Eq.symm heq)) h)
            (clause.8.0 a fun eb!_0 => ¬e!_2 eb!_0 (e!_0 eb!_0)))
        clause.4.0;
    let clause.23.0 := fun a =>
      (fun h => Duper.loob_hoist_proof (fun h => e!_2 a (e!_0 e?_0) = ¬h) (e!_2 a (e!_0 a)) h) (clause.12.0 a);
    let clause.24.0 := fun a =>
      (fun h => Duper.bool_hoist_proof (fun h => e!_2 a (e!_0 e?_0) = ¬h) (e!_2 a (e!_0 a)) h) (clause.12.0 a);
    let clause.25.0 := fun a =>
      (fun h =>
          Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => e!_2 a (e!_0 e?_0) = x) Duper.rule14Theorem) h))
            fun h => Or.inr h)
        (clause.23.0 a);
    let clause.35.0 := fun a =>
      (fun h =>
          Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => e!_2 a (e!_0 e?_0) = x) Duper.rule7Theorem) h)) fun h =>
            Or.inr h)
        (clause.24.0 a);
    let clause.37.0 :=
      (fun h => Or.elim h (fun h => Duper.equality_factoring_soundness1 True h) fun h => Or.inr h) (clause.35.0 e?_0);
    let clause.38.0 :=
      (fun h => Or.elim h (fun h => Or.inr (Duper.clausify_prop_inequality1 h)) fun h => Or.inl h) clause.37.0;
    let clause.40.0 :=
      (fun h =>
          Or.elim h (fun h => Or.inl h) fun h =>
            Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => Or.inr h)
        clause.38.0;
    let clause.41.0 := (fun h => Or.elim h (fun h => h) fun h => False.elim (Duper.true_neq_false h)) clause.40.0;
    let clause.42.0 :=
      (fun heq =>
          (fun h =>
              Or.elim h (fun h => Or.inl (Eq.mp (congrArg (fun x => x = False) heq) h)) fun h =>
                Or.inr (Eq.mp (congrArg (fun x => x = False) heq) h))
            (clause.25.0 e?_0))
        clause.41.0;
    let clause.43.0 := (fun h => Or.elim h (fun h => False.elim (Duper.true_neq_false h)) fun h => h) clause.42.0;
    (fun h => False.elim (Duper.true_neq_false h)) clause.43.0
Goals accomplished! 🐙


example: ∀ {R : Type uR} [inst : CommRing R] [inst_1 : Nontrivial R] {M : Type uM} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module.Finite R M], Module.rank R M = ↑(finrank R M)
example : 
Module.rank: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst : Module R M] → Cardinal.{uM}
Module.rank 
R: Type uR
R 
M: Type uM
M = 
finrank: (R : Type uR) → (M : Type uM) → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst : Module R M] → ℕ
finrank 
R: Type uR
R 
M: Type uM
M := by
Goals accomplished! 🐙
  duper [
finrank_eq_rank: ∀ (R : Type ?u.90201) (M : Type ?u.90200) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : StrongRankCondition R] [inst_4 : Module.Finite R M], ↑(finrank R M) = Module.rank R M
finrank_eq_rank]
[duper.printProof] Clause #0 (by assumption []): (¬e!_0 e!_1 = e!_0 e!_1) = True
[duper.printProof] Clause #1 (by clausification [0]): (e!_0 e!_1 = e!_0 e!_1) = False
[duper.printProof] Clause #2 (by clausification [1]): e!_0 e!_1 ≠ e!_0 e!_1
[duper.printProof] Clause #3 (by eliminate resolved literals [2]): False
[duper.proofReconstruction] Collected clauses: [(¬e!_0 e!_1 = e!_0 e!_1) = True,
     (e!_0 e!_1 = e!_0 e!_1) = False,
     e!_0 e!_1 ≠ e!_0 e!_1,
     False]
[duper.proofReconstruction] Request [] ↦ [] for False
[duper.proofReconstruction] Request [] ↦ [] for e!_0 e!_1 ≠ e!_0 e!_1
[duper.proofReconstruction] Request [] ↦ [] for (e!_0 e!_1 = e!_0 e!_1) = False
[duper.proofReconstruction] Request [] ↦ [] for (¬e!_0 e!_1 = e!_0 e!_1) = True
[duper.proofReconstruction] Reconstructing proof for #0 : [] ↦ [] @ (¬e!_0 e!_1 = e!_0 e!_1) =
      True, Rule Name: assumption
[duper.proofReconstruction] #0's newProof: eq_true «_exHyp_uniq.90683»
[duper.proofReconstruction] Instantiating parent (¬e!_0 e!_1 = e!_0 e!_1) =
      True ≡≡ (¬e!_0 e!_1 = e!_0 e!_1) = True with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #1 : [] ↦ [] @ (e!_0 e!_1 = e!_0 e!_1) =
      False, Rule Name: clausification
[duper.proofReconstruction] #1's newProof: (fun h => Duper.clausify_not h) clause.0.0
[duper.proofReconstruction] Instantiating parent (e!_0 e!_1 = e!_0 e!_1) =
      False ≡≡ (e!_0 e!_1 = e!_0 e!_1) = False with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #2 : [] ↦ [] @ e!_0 e!_1 ≠ e!_0 e!_1, Rule Name: clausification
[duper.proofReconstruction] #2's newProof: (fun h => Duper.not_of_eq_false h) clause.1.0
[duper.proofReconstruction] Instantiating parent e!_0 e!_1 ≠ e!_0 e!_1 ≡≡ e!_0 e!_1 ≠ e!_0 e!_1 with param subst [] ↦ []
[duper.proofReconstruction] Reconstructing proof for #3 : [] ↦ [] @ False, Rule Name: eliminate resolved literals
[duper.proofReconstruction] #3's newProof: (fun h => False.elim (h rfl)) clause.2.0
[duper.proofReconstruction] Proof: let clause.0.0 := eq_true «_exHyp_uniq.90683»;
    let clause.1.0 := (fun h => Duper.clausify_not h) clause.0.0;
    let clause.2.0 := (fun h => Duper.not_of_eq_false h) clause.1.0;
    (fun h => False.elim (h rfl)) clause.2.0
Goals accomplished! 🐙
  done
Warning: 'done' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
Goals accomplished! 🐙