awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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))
have rw : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (↑l : List I)
Tactic: rw [← max_eq_o_cons_tail ho l hl hlh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ (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
have hlc : 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
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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))
⊢ (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
have 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) sorry)) =
  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: rw [max_eq_o_cons_tail' ho l hl hlh hlc, Products.evalCons]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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))
⊢ (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))
have 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)
                    sorry)) :
            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: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ 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 :
      ℤ)
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ 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
have 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)) sorry) :
        ℤ)
      (if
            ∀ i ∈ (↑l.Tail : List I),
              (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) sorry) : 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) sorry) : ℤ)
      (if
            ∀ i ∈ (↑l.Tail : List I),
              (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) sorry) : 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: rw [CC'₁, CC'₀, Products.eval_eq, Products.eval_eq, Products.eval_eq]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ 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
have 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)) sorry)
      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) sorry)
      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]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ (↑x : I → Bool) i = SwapTrue o (↑x : I → Bool) i
have simp : term I ho = i → true = (↑x : I → Bool) i
Tactic: simp only [SwapTrue, @eq_comm _ (x.val i), ite_eq_right_iff, ord_term ho]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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)
⊢ 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
have hi' : ∀ 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
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
have 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)
Tactic: apply forall_congr
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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
⊢ Eq (α := Prop) (i ∈ (↑l.Tail : List I) → (↑x : I → Bool) i = true)
    (i ∈ (↑l.Tail : List I) → SwapTrue o (↑x : I → Bool) i = true)
have h : ∀ (a : i ∈ (↑l.Tail : List I)), ((↑x : I → Bool) i = true) = (SwapTrue o (↑x : I → Bool) i = true)
Tactic: apply forall_congr
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ ((↑x : I → Bool) i = true) = (SwapTrue o (↑x : I → Bool) i = true)
have h : (SwapTrue o (↑x : I → Bool) i = true) = (SwapTrue o (↑x : I → Bool) i = true)
Tactic: rw [hi' i hi]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ 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
have 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)) sorry)
      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) sorry)
      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]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
⊢ 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
have pos : ∀ (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 (α := ℤ) (β := ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) sorry) :
        ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) sorry) :
        ℤ) =
    1
Tactic: split_ifs with h₁ h₂ h₃
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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)
pos :
  ∀ (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 (α := ℤ) (β := ℤ)
        ((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
⊢ 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
have neg : ∀ (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 (α := ℤ) (β := ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) sorry) :
        ℤ)
      ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) sorry) :
        ℤ) =
    0
Tactic: split_ifs with h₁ h₂ h₃