awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h :
  HSub.hSub (α := ℤ) (β := ℤ)
      (if ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true then
          (e C (term I ho) : (a : (↑C : Type u)) → ℤ)
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯)
        else 0 :
        ℤ)
      (if ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true then
          (e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯)
        else 0 :
        ℤ) =
    if
        ∀
          i ∈
            (↑(Tail
                  (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                    (term I ho :: (↑l.Tail : List I)) hlc)) :
              List I),
          (↑x : I → Bool) i = true then
      1
    else 0
⊢ HSub.hSub (α := ℤ) (β := ℤ)
      (if ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true then
          (e C (term I ho) : (a : (↑C : Type u)) → ℤ)
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯)
        else 0 :
        ℤ)
      (if ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true then
          (e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯)
        else 0 :
        ℤ) =
    if
        ∀
          i ∈
            (↑(Tail
                  (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                    (term I ho :: (↑l.Tail : List I)) hlc)) :
              List I),
          (↑x : I → Bool) i = true then
      1
    else 0

Tactic:
simp only [H]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
pos :
  HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    1
⊢ HSub.hSub (α := ℤ) (β := ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) :
        ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
        ℤ) =
    1

Tactic:
dsimp [e]

Premises used: Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
pos :
  HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    1
⊢ HSub.hSub (α := ℤ) (β := ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) :
        ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
        ℤ) =
    1

Tactic:
try (dsimp [e])

Premises used: Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ¬∀
      i ∈
        (↑(Tail
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                (term I ho :: (↑l.Tail : List I)) hlc)) :
          List I),
      (↑x : I → Bool) i = true
neg :
  HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    0
⊢ HSub.hSub (α := ℤ) (β := ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) :
        ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
        ℤ) =
    0

Tactic:
dsimp [e]

Premises used: Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ¬∀
      i ∈
        (↑(Tail
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                (term I ho :: (↑l.Tail : List I)) hlc)) :
          List I),
      (↑x : I → Bool) i = true
neg :
  HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    0
⊢ HSub.hSub (α := ℤ) (β := ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) :
        ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
        ℤ) =
    0

Tactic:
try (dsimp [e])

Premises used: Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ¬∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₃ :
  ¬∀
      i ∈
        (↑(Tail
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                (term I ho :: (↑l.Tail : List I)) hlc)) :
          List I),
      (↑x : I → Bool) i = true
⊢ HSub.hSub (α := ℤ) 0 0 = 0

Tactic:
dsimp [e]

Premises used: Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ¬∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₃ :
  ¬∀
      i ∈
        (↑(Tail
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                (term I ho :: (↑l.Tail : List I)) hlc)) :
          List I),
      (↑x : I → Bool) i = true
⊢ HSub.hSub (α := ℤ) 0 0 = 0

Tactic:
try (dsimp [e])

Premises used: Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
pos : HSub.hSub (α := ℤ) 1 0 = 1
pos₁ : ¬(↑x : I → Bool) (term I ho) = true
⊢ HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    1

Tactic:
rw [if_pos (swapTrue_eq_true _ _), if_neg]

Premises used: if_pos, Profinite.NobelingProof.swapTrue_eq_true, if_neg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
⊢ HSub.hSub (α := ℤ) 1 0 = 1

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
⊢ ¬(↑x : I → Bool) (term I ho) = true

Tactic:
simp [mem_C'_eq_false C ho x x.prop]

Premises used: Profinite.NobelingProof.mem_C'_eq_false, Subtype.prop, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ¬∀
      i ∈
        (↑(Tail
              (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                (term I ho :: (↑l.Tail : List I)) hlc)) :
          List I),
      (↑x : I → Bool) i = true
⊢ ∃
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i ≠ true

Tactic:
push Not at h₂

Premises used: Not
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₂ :
  ∃
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i ≠ true
neg :
  ∀ (i : I)
    (hi :
      i ∈
          (↑(Tail
                (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
                  (term I ho :: (↑l.Tail : List I)) hlc)) :
            List I) ∧
        (↑x : I → Bool) i ≠ true),
    HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
        (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
      0
⊢ HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    0

Tactic:
obtain ⟨i, hi⟩ := h₂
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
i : I
hi :
  i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I) ∧
    (↑x : I → Bool) i ≠ true
neg : False
⊢ HSub.hSub (α := ℤ) (if SwapTrue o (↑x : I → Bool) (term I ho) = true then 1 else 0)
      (if (↑x : I → Bool) (term I ho) = true then 1 else 0) =
    0

Tactic:
exfalso
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
i : I
hi :
  i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I) ∧
    (↑x : I → Bool) i ≠ true
⊢ i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I) ∧
    SwapTrue o (↑x : I → Bool) i ≠ true

Tactic:
rw [hi' i hi.1] at hi

Premises used: And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
i : I
hi :
  i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I) ∧
    SwapTrue o (↑x : I → Bool) i ≠ true
⊢ False

Tactic:
hi.2 (h₁ i hi.1)

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
i : I
hi :
  i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I) ∧
    SwapTrue o (↑x : I → Bool) i ≠ true
⊢ False

Tactic:
exact hi.2 (h₁ i hi.1)

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₁ : ¬∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true
h₃ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
⊢ ∃ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i ≠ true

Tactic:
push Not at h₁

Premises used: Not
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
inst_2 : Inhabited I
l : Products I
hl : (↑l : List I) ≠ []
hlh : (↑l : List I).head! = term I ho
hlc : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))
x : (↑(C' C ho) : Type u)
hi' : ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
H :
  Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)
h₃ :
  ∀
    i ∈
      (↑(Tail
            (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l)
              (term I ho :: (↑l.Tail : List I)) hlc)) :
        List I),
    (↑x : I → Bool) i = true
h₁ : ∃ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i ≠ true
pos : ∀ (i : I) (hi : i ∈ (↑l.Tail : List I) ∧ SwapTrue o (↑x : I → Bool) i ≠ true), Eq (α := ℤ) 0 1
⊢ Eq (α := ℤ) 0 1

Tactic:
obtain ⟨i, hi⟩ := h₁