-- 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
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)) ⋯) :
          ℤ)
        ((e C (term I ho) : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯) :
          ℤ) =
      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), 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 (α := ℤ) 0 0 = 1
Tactic: split_ifs with h₁ h₂ h₃