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
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 (α := ℤ) (β := ℤ)
      ((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
have 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
Tactic: dsimp [e]
-- 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)
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
have 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
Tactic: try (dsimp [e])
-- 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)
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
have 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
Tactic: dsimp [e]
-- 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)
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
have 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
Tactic: try (dsimp [e])
-- 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)
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 (α := ℤ) (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
have pos : HSub.hSub (α := ℤ) 1 0 = 1
Tactic: rw [if_pos (swapTrue_eq_true _ _), if_neg]
-- 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)
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
⊢ 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
have pos₁ : ¬(↑x : I → Bool) (term I ho) = true
Tactic: rw [if_pos (swapTrue_eq_true _ _), if_neg]
-- 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
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 (α := ℤ) (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
have 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
Tactic: push Not at h₂
Cleared hypotheses: 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)
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 (α := ℤ) (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
have 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
Tactic: obtain ⟨i, hi⟩ := h₂
Cleared hypotheses: 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)
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
⊢ 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
have neg : False
Tactic: exfalso
-- 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
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
⊢ False
have 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
Tactic: rw [hi' i hi.1] at hi
Cleared hypotheses: 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
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
⊢ Eq (α := ℤ) 0 1
have h₂ : ∃ i ∈ (↑l.Tail : List I), SwapTrue o (↑x : I → Bool) i ≠ true
Tactic: push Not at h₁
Cleared hypotheses: 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)
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
⊢ Eq (α := ℤ) 0 1
have pos : ∀ (i : I) (hi : i ∈ (↑l.Tail : List I) ∧ SwapTrue o (↑x : I → Bool) i ≠ true), Eq (α := ℤ) 0 1
Tactic: obtain ⟨i, hi⟩ := h₁
Cleared hypotheses: 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)
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 : I
hi : i ∈ (↑l.Tail : List I) ∧ SwapTrue o (↑x : I → Bool) i ≠ true
⊢ Eq (α := ℤ) 0 1
have pos : False
Tactic: exfalso
-- 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
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
i : I
hi : i ∈ (↑l.Tail : List I) ∧ SwapTrue o (↑x : I → Bool) i ≠ true
⊢ False
have hi₁ : i ∈ (↑l.Tail : List I) ∧ (↑x : I → Bool) i ≠ true
Tactic: rw [← hi' i hi.1] at hi
Cleared hypotheses: 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
⊢ Eq (α := (↑(MaxProducts C ho) : Type u) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
      (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
    fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval (C' C ho) (↑l : Products I).Tail
have h : ∀ (l : (↑(MaxProducts C ho) : Type u)),
  Function.comp (β := LocallyConstant (↑C : Type u) ℤ)
      (⇑(Linear_CC' C hsC ho) : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
      (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) l =
    Products.eval (C' C ho) (↑l : Products I).Tail
Tactic: ext1 l
-- 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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
⊢ List.IsChain (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
have have : ∀ (this : Inhabited I), List.IsChain (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
Tactic: have : Inhabited I := ⟨term I ho⟩
-- 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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
⊢ List.IsChain (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
have rw : List.Pairwise (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
Tactic: rw [List.isChain_iff_pairwise]
-- 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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
⊢ List.Pairwise (fun (x x_1 : I) ↦ x > x_1) (term I ho :: (↑q : List I))
have simp : (∀ a' ∈ (↑q : List I), a' < term I ho) ∧ List.Pairwise (fun (x x_1 : I) ↦ x_1 < x) (↑q : List I)
Tactic: simp only [gt_iff_lt, List.pairwise_cons]
-- 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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
⊢ (∀ a' ∈ (↑q : List I), a' < term I ho) ∧ List.Pairwise (fun (x x_1 : I) ↦ x_1 < x) (↑q : List I)
have refine : ∀ (a : I) (ha : a ∈ (↑q : List I)), (↑q : List I).head! < term I ho
Tactic: refine ⟨fun a ha ↦ lt_of_le_of_lt (Products.rel_head!_of_mem ha) ?_,
    List.isChain_iff_pairwise.mp q.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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
⊢ (↑q : List I).head! < term I ho
have refine : (↑(↑l : Products I).Tail : List I).head! < term I ho
Tactic: refine lt_of_le_of_lt (Products.head!_le_of_lt hq (q.val.ne_nil_of_mem ha)) ?_
-- 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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho
have pos : ∀ (hM : (↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
Tactic: by_cases hM : l.val.Tail.val = []
-- 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
l : (↑(MaxProducts C ho) : Type u)
q : Products I
hq : q < (↑l : Products I).Tail
this : Inhabited I
a : I
ha : a ∈ (↑q : List I)
pos : ∀ (hM : (↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
⊢ (↑(↑l : Products I).Tail : List I).head! < term I ho
have neg : ∀ (hM : ¬(↑(↑l : Products I).Tail : List I) = []), (↑(↑l : Products I).Tail : List I).head! < term I ho
Tactic: by_cases hM : l.val.Tail.val = []