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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ ord I (↑(↑l : Products I) : List I).head! = o

Tactic:
eq_of_le_of_not_lt this (not_lt.mpr ?_)

Premises used: Iff.mpr, not_lt, eq_of_le_of_not_lt
-- 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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
refine : o ≤ ord I (↑(↑l : Products I) : List I).head!
⊢ ord I (↑(↑l : Products I) : List I).head! = o

Tactic:
refine eq_of_le_of_not_lt this (not_lt.mpr ?_)

Premises used: Iff.mpr, not_lt, eq_of_le_of_not_lt
-- 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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
simp : term I ho ≤ (↑(↑l : Products I) : List I).head!
⊢ ord I (term I ho) ≤ ord I (↑(↑l : Products I) : List I).head!

Tactic:
simp only [ord, Ordinal.typein_le_typein, not_lt]

Premises used: Ordinal.typein_le_typein, Profinite.NobelingProof.ord, not_lt
-- 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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ term I ho ≤ (↑(↑l : Products I) : List I).head!

Tactic:
Products.rel_head!_of_mem hm

Premises used: Profinite.NobelingProof.Products.rel_head!_of_mem
-- 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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ term I ho ≤ (↑(↑l : Products I) : List I).head!

Tactic:
exact Products.rel_head!_of_mem hm

Premises used: Profinite.NobelingProof.Products.rel_head!_of_mem
-- 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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
⊢ ord I (term I ho) ≤ ord I (↑(↑l : Products I) : List I).head!

Tactic:
have h : ord I (term I ho) ≤ ord I l.val.val.head! := by
    simp only [ord, Ordinal.typein_le_typein, not_lt]
    exact Products.rel_head!_of_mem hm
-- 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 : (↑(MaxProducts C ho) : Type u)
hm : term I ho ∈ (↑(↑l : Products I) : List I)
this : ord I (↑(↑l : Products I) : List I).head! ≤ o
h : ord I (term I ho) ≤ ord I (↑(↑l : Products I) : List I).head!
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : o ≤ ord I (↑(↑l : Products I) : List I).head!), o ≤ ord I (↑(↑l : Products I) : List I).head!
⊢ o ≤ ord I (↑(↑l : Products I) : List I).head!

Tactic:
rwa [ord_term_aux] at h

Premises used: Profinite.NobelingProof.ord_term_aux
-- 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
l : (↑(MaxProducts C ho) : Type u)
⊢ (↑(↑l : Products I) : List I) = term I ho :: (↑(↑l : Products I).Tail : List I)

Tactic:
have : Inhabited I := ⟨term I ho⟩
  Products.max_eq_o_cons_tail ho l.val (List.ne_nil_of_mem l.prop.2)
    (head!_eq_o_of_maxProducts _ hsC ho l)

Premises used: List.ne_nil_of_mem, Profinite.NobelingProof.term, And.right, Subtype.prop, Subtype.val, Profinite.NobelingProof.Products.max_eq_o_cons_tail, Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts, Inhabited.mk
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u_1
inst : LinearOrder I
C : Set (I → Bool)
l : List I
a : I
hla : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: l)
⊢ eval C (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (a :: l) hla) =
    e C a * eval C (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) l ⋯)

Tactic:
simp only [eval.eq_1, List.map, List.prod_cons]

Premises used: List.map, List.prod_cons, Profinite.NobelingProof.Products.eval.eq_1
-- 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
rw : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑l : List I)
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))

Tactic:
rw [← max_eq_o_cons_tail ho l hl hlh]

Premises used: Profinite.NobelingProof.Products.max_eq_o_cons_tail
-- 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
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑l : List I)

Tactic:
l.prop

Premises used: Subtype.prop
-- 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
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑l : List I)

Tactic:
exact l.prop

Premises used: Subtype.prop
-- 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
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (term I ho :: (↑l.Tail : List I))

Tactic:
have hlc : ((term I ho) :: l.Tail.val).IsChain (· > ·) := by
    rw [← max_eq_o_cons_tail ho l hl hlh]; exact l.prop
-- 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))
rw :
  (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (e C (term I ho) *
        eval C (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (↑l.Tail : List I) ⋯)) =
    eval (C' C ho)
      (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))
⊢ (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ) (eval C l) =
    eval (C' C ho) l.Tail

Tactic:
rw [max_eq_o_cons_tail' ho l hl hlh hlc, Products.evalCons]

Premises used: Profinite.NobelingProof.Products.evalCons, Profinite.NobelingProof.Products.max_eq_o_cons_tail'
-- 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))
h :
  ∀ (x : (↑(C' C ho) : Type u)),
    Eq (α := ℤ)
      ((((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
                (e C (term I ho) *
                  eval C
                    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (↑l.Tail : List I)
                      ⋯)) :
              LocallyConstant (↑(C' C ho) : Type u) ℤ) :
            (a : (↑(C' C ho) : Type u)) → ℤ)
          x :
        ℤ)
      ((eval (C' C ho)
              (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)) :
            (a : (↑(C' C ho) : Type u)) → ℤ)
          x :
        ℤ)
⊢ (Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (e C (term I ho) *
        eval C (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (↑l.Tail : List I) ⋯)) =
    eval (C' C ho)
      (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))

Tactic:
ext x
-- 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)
h :
  HMul.hMul (α := ℤ) (β := ℤ) ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (CC'₁ C hsC ho x) : ℤ)
        ((eval C l.Tail : (a : (↑C : Type u)) → ℤ) (CC'₁ C hsC ho x) : ℤ) -
      HMul.hMul (α := ℤ) (β := ℤ) ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (CC'₀ C ho x) : ℤ)
        ((eval C l.Tail : (a : (↑C : Type u)) → ℤ) (CC'₀ C ho x) : ℤ) =
    (eval (C' C ho)
          (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)) :
        (a : (↑(C' C ho) : Type u)) → ℤ)
      x
⊢ Eq (α := ℤ)
    ((((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
              (e C (term I ho) *
                eval C
                  (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (↑l.Tail : List I)
                    ⋯)) :
            LocallyConstant (↑(C' C ho) : Type u) ℤ) :
          (a : (↑(C' C ho) : Type u)) → ℤ)
        x :
      ℤ)
    ((eval (C' C ho)
            (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)) :
          (a : (↑(C' C ho) : Type u)) → ℤ)
        x :
      ℤ)

Tactic:
simp only [Linear_CC', Linear_CC'₁, LocallyConstant.comapₗ, Linear_CC'₀, Subtype.coe_eta,
    LinearMap.sub_apply, LinearMap.coe_mk, AddHom.coe_mk, LocallyConstant.sub_apply,
    LocallyConstant.coe_comap, LocallyConstant.coe_mul, ContinuousMap.coe_mk, Function.comp_apply,
    Pi.mul_apply]

Premises used: LinearMap.coe_mk, Pi.mul_apply, LocallyConstant.coe_comap, LocallyConstant.coe_mul, Profinite.NobelingProof.Linear_CC', LocallyConstant.comapₗ, ContinuousMap.coe_mk, Subtype.coe_eta, LocallyConstant.sub_apply, LinearMap.sub_apply, Function.comp_apply, Profinite.NobelingProof.Linear_CC'₀, Profinite.NobelingProof.Linear_CC'₁, AddHom.coe_mk
-- 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)
h :
  HMul.hMul (α := ℤ) (β := ℤ)
        ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) :
          ℤ)
        (if
              ∀ i ∈ (↑l.Tail : List I),
                (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) : I → Bool) i =
                  true then
            1
          else 0 :
          ℤ) -
      HMul.hMul (α := ℤ) (β := ℤ)
        ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
          ℤ)
        (if
              ∀ i ∈ (↑l.Tail : List I),
                (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) : I → Bool) i = true then
            1
          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
⊢ HMul.hMul (α := ℤ) (β := ℤ) ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (CC'₁ C hsC ho x) : ℤ)
        ((eval C l.Tail : (a : (↑C : Type u)) → ℤ) (CC'₁ C hsC ho x) : ℤ) -
      HMul.hMul (α := ℤ) (β := ℤ) ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (CC'₀ C ho x) : ℤ)
        ((eval C l.Tail : (a : (↑C : Type u)) → ℤ) (CC'₀ C ho x) : ℤ) =
    (eval (C' C ho)
          (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)) :
        (a : (↑(C' C ho) : Type u)) → ℤ)
      x

Tactic:
rw [CC'₁, CC'₀, Products.eval_eq, Products.eval_eq, Products.eval_eq]

Premises used: Profinite.NobelingProof.Products.eval_eq, Profinite.NobelingProof.CC'₁, Profinite.NobelingProof.CC'₀
-- 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)
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), (↑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
⊢ HMul.hMul (α := ℤ) (β := ℤ)
        ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) :
          ℤ)
        (if
              ∀ i ∈ (↑l.Tail : List I),
                (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯) : I → Bool) i =
                  true then
            1
          else 0 :
          ℤ) -
      HMul.hMul (α := ℤ) (β := ℤ)
        ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
          ℤ)
        (if
              ∀ i ∈ (↑l.Tail : List I),
                (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) : I → Bool) i = true then
            1
          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 [mul_ite, mul_one, mul_zero]

Premises used: mul_ite, MulZeroClass.mul_zero, mul_one
-- 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)
i : I
hi : i ∈ (↑l.Tail : List I)
simp : term I ho = i → true = (↑x : I → Bool) i
⊢ (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i

Tactic:
simp only [SwapTrue, @eq_comm _ (x.val i), ite_eq_right_iff, ord_term ho]

Premises used: Profinite.NobelingProof.ord_term, eq_comm, Profinite.NobelingProof.SwapTrue, ite_eq_right_iff
-- 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 : term I ho ∈ (↑l.Tail : List I)
⊢ true = (↑x : I → Bool) (term I ho)

Tactic:
((List.IsChain.rel_cons hlc hi).ne rfl).elim

Premises used: List.IsChain.rel_cons, False.elim, rfl, LT.lt.ne
-- 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 : term I ho ∈ (↑l.Tail : List I)
⊢ true = (↑x : I → Bool) (term I ho)

Tactic:
exact ((List.IsChain.rel_cons hlc hi).ne rfl).elim

Premises used: List.IsChain.rel_cons, False.elim, rfl, LT.lt.ne
-- 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)
⊢ ∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i

Tactic:
have hi' : ∀ i, i ∈ l.Tail.val → (x.val i = SwapTrue o x.val i) := by
    intro i hi
    simp only [SwapTrue, @eq_comm _ (x.val i), ite_eq_right_iff, ord_term ho]
    rintro rfl
    exact ((List.IsChain.rel_cons hlc hi).ne rfl).elim
-- 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 :
  ∀ (a : I),
    Eq (α := Prop) (a ∈ (↑l.Tail : List I) → (↑x : I → Bool) a = true)
      (a ∈ (↑l.Tail : List I) → SwapTrue o (↑x : I → Bool) a = true)
⊢ Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)

Tactic:
apply forall_congr

Premises used: forall_congr
-- 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
i : I
h : ∀ (a : i ∈ (↑l.Tail : List I)), ((↑x : I → Bool) i = true) = (SwapTrue o (↑x : I → Bool) i = true)
⊢ Eq (α := Prop) (i ∈ (↑l.Tail : List I) → (↑x : I → Bool) i = true)
    (i ∈ (↑l.Tail : List I) → SwapTrue o (↑x : I → Bool) i = true)

Tactic:
apply forall_congr

Premises used: forall_congr
-- 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
i : I
hi : i ∈ (↑l.Tail : List I)
h h₁ : (SwapTrue o (↑x : I → Bool) i = true) = (SwapTrue o (↑x : I → Bool) i = true)
⊢ ((↑x : I → Bool) i = true) = (SwapTrue o (↑x : I → Bool) i = true)

Tactic:
rw [hi' i hi]
-- 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
⊢ Eq (α := Prop) (∀ i ∈ (↑l.Tail : List I), (↑x : I → Bool) i = true)
    (∀ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i = true)

Tactic:
have H : (∀ i, i ∈ l.Tail.val → (x.val i = true)) =
      (∀ i, i ∈ l.Tail.val → (SwapTrue o x.val i = true)) := by
    apply forall_congr; intro i; apply forall_congr; intro hi; rw [hi' i hi]