awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: { rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: { rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₂ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: { rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₂ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₃ : a ⊓ b ⊓ c ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: { rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
rw : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₁ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₂ : a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
rw₃ : a ⊓ b ⊓ c ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
have rw₄ : a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Tactic: { rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
have e_a : a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
e_a : a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
have e_a₁ : c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ
have e_a : b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ
have e_a : aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ b ⊓ cᶜ
Tactic: rw [inf_comm, inf_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
e_a : aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ b ⊓ cᶜ
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ
have e_a₁ : aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ (b ⊓ cᶜ)
Tactic: rw [inf_comm, inf_assoc]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c
have trans : c ≤ c \ (a ⊓ b)
Tactic: trans c \ (a ⊓ b)
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
trans : c ≤ c \ (a ⊓ b)
⊢ c ≤ a ∆ c ⊔ b ∆ c
have trans₁ : c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
Tactic: trans c \ (a ⊓ b)
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)
have rw : c ≤ c \ ⊥
Tactic: rw [h.eq_bot, sdiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
rw : c ≤ c \ ⊥
⊢ c ≤ c \ (a ⊓ b)
have rw₁ : c ≤ c
Tactic: rw [h.eq_bot, sdiff_bot]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
have rw : c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c
Tactic: rw [sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.SymmDiff (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c
have simp_rw : a ≤ b ∆ a ⊔ c ∆ a
Tactic: simp_rw [symmDiff_comm a]
-- Lean 4 proof step from Mathlib.Order.TeichmullerTukey (goal)
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
⊢ ∃ (m : Set α), x ⊆ m ∧ Maximal (fun (x : Set α) ↦ x ∈ F) m
have refine : ∀ (c : Set (Set α)) (cF : c ⊆ F) (cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c) (cne : c.Nonempty), ⋃₀ c ∈ F
Tactic: refine zorn_subset_nonempty F (fun c cF cch cne ↦
    ⟨sUnion c, ?_, fun s sc ↦ subset_sUnion_of_mem sc⟩) x xF
-- Lean 4 proof step from Mathlib.Order.TeichmullerTukey (goal)
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
⊢ ⋃₀ c ∈ F
have refine : ∀ (s : Set α) (sc : s ⊆ ⋃₀ c) (sfin : s.Finite), s ∈ F
Tactic: refine (hF (sUnion c)).mpr fun s sc sfin ↦ ?_
-- Lean 4 proof step from Mathlib.Order.TeichmullerTukey (goal)
Goal:
α : Type u_1
F : Set (Set α)
hF : IsOfFiniteCharacter F
x : Set α
xF : x ∈ F
c : Set (Set α)
cF : c ⊆ F
cch : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
cne : c.Nonempty
s : Set α
sc : s ⊆ ⋃₀ c
sfin : s.Finite
⊢ s ∈ F
have obtain : ∀ (t : Set α) (tc : t ∈ c) (st : s ⊆ t), s ∈ F
Tactic: obtain ⟨t, tc, st⟩ := cch.directedOn.exists_mem_subset_of_finite_of_subset_sUnion cne sfin sc
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
inst_4 : OrderBot J
i₀ : I
⊢ transfiniteIterate.{w, u} φ (J := J) ⊥ i₀ = i₀
have dsimp : SuccOrder.limitRecOn ⊥ (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
    (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
    (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
      ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
    i₀ =
  i₀
Tactic: dsimp [transfiniteIterate]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀)
have dsimp : SuccOrder.limitRecOn (Order.succ j) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
    (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
    (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
      ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
    i₀ =
  φ
    (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
      i₀)
Tactic: dsimp [transfiniteIterate]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ SuccOrder.limitRecOn (Order.succ j) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
        i₀)
have rw : (φ ∘
      SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
    i₀ =
  φ
    (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
      i₀)
Tactic: rw [SuccOrder.limitRecOn_succ_of_not_isMax _ _ _ hj]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ transfiniteIterate φ j i₀ = ⨆ (x : (↑(Set.Iio j) : Type w)), transfiniteIterate φ (↑x : J) i₀
have dsimp : Eq.{u + 1} (α := I)
  (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
      i₀ :
    I)
  (⨆ (x : (↑(Set.Iio j) : Type w)),
      SuccOrder.limitRecOn (↑x : J) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
        i₀ :
    I)
Tactic: dsimp [transfiniteIterate]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : SupSet I
φ : I → I
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ Eq.{u + 1} (α := I)
    (SuccOrder.limitRecOn j (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
        (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
        (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
          ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
        i₀ :
      I)
    (⨆ (x : (↑(Set.Iio j) : Type w)),
        SuccOrder.limitRecOn (↑x : J) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
          (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
          (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
            ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) ⋯)
          i₀ :
      I)
have rw : Eq.{u + 1} (α := I)
  ((⨆ (x : (↑(Set.Iio j) : Type w)),
      (fun (x : J) (x_1 : x < j) ↦
          (SuccOrder.limitRecOn x (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_2 : IsMin x) ↦ id)
              (fun (x : J) (x_2 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
              fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
              ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry :
            I → I))
        (↑x : J) sorry)
    i₀)
  (⨆ (x : (↑(Set.Iio j) : Type w)),
    SuccOrder.limitRecOn (↑x : J) (motive := fun (x : J) ↦ I → I) (fun (x : J) (x_1 : IsMin x) ↦ id)
      (fun (x : J) (x_1 : ¬IsMax x) (g : I → I) ↦ φ ∘ g)
      (fun (y : J) (x : Order.IsSuccLimit y) (h : (b : J) → b < y → I → I) ↦
        ⨆ (x : (↑(Set.Iio y) : Type w)), h (↑x : J) sorry)
      i₀)
Tactic: rw [SuccOrder.limitRecOn_of_isSuccLimit _ _ _ hj]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k_1 k : J
hk : IsMin k
hkj : k_1 ≤ k
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k_1) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
have isMin : ∀ (hk : IsMin.{w} (α := J) ⊥) (hkj : k_1 ≤ ⊥),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k_1) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥)
Tactic: obtain rfl := hk.eq_bot
Cleared hypotheses: k, hk, hkj
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk : IsMin.{w} (α := J) ⊥
hkj : k ≤ ⊥
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥)
have isMin : ∀ (hkj : LE.le.{w} (α := J) ⊥ ⊥),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥)
Tactic: obtain rfl : k = ⊥ := by simpa using hkj
Cleared hypotheses: k, hkj
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' :
  ∀ (hkj : k ≤ k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
hkj : k ≤ Order.succ k'
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
have succ : ∀ (hkj : k < Order.succ k'),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
Tactic: obtain hkj | rfl := hkj.lt_or_eq
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' :
  ∀ (hkj : k ≤ k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
hkj : k ≤ Order.succ k'
succ :
  ∀ (hkj : k < Order.succ k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
      ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
have succ₁ : ∀
  (hkk' :
    ∀ (hkj : Order.succ k' ≤ k'),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
        ((fun (j : J) ↦ transfiniteIterate φ j i₀) k'))
  (hkj : Order.succ k' ≤ Order.succ k'),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
Tactic: obtain hkj | rfl := hkj.lt_or_eq
Cleared hypotheses: k, hkk', hkj
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' :
  ∀ (hkj : k ≤ k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
hkj_1 : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
have succ : LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
  ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
Tactic: refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' :
  ∀ (hkj : k ≤ k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
hkj_1 : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ transfiniteIterate φ (Order.succ k') i₀
have succ : transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)
Tactic: rw [transfiniteIterate_succ _ _ _ hk']
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
h :
  ∀ b < k',
    ∀ (hkj : k ≤ b),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) b)
hkj : k ≤ k'
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
have isSuccLimit : ∀ (hkj : k < k'),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
Tactic: obtain hkj | rfl := hkj.lt_or_eq
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
h :
  ∀ b < k',
    ∀ (hkj : k ≤ b),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) b)
hkj : k ≤ k'
isSuccLimit :
  ∀ (hkj : k < k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
have isSuccLimit₁ : ∀ (hk' : Order.IsSuccLimit k),
  (∀ b < k,
      ∀ (hkj : k ≤ b),
        LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
          ((fun (j : J) ↦ transfiniteIterate φ j i₀) b)) →
    ∀ (hkj : k ≤ k),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
Tactic: obtain hkj | rfl := hkj.lt_or_eq
Cleared hypotheses: k', hk', h, hkj
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
h :
  ∀ b < k',
    ∀ (hkj : k ≤ b),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) b)
hkj_1 : k ≤ k'
hkj : k < k'
⊢ transfiniteIterate φ k i₀ ≤ transfiniteIterate φ k' i₀
have isSuccLimit : transfiniteIterate φ k i₀ ≤ ⨆ (x : (↑(Set.Iio k') : Type w)), transfiniteIterate φ (↑x : J) i₀
Tactic: rw [transfiniteIterate_limit _ _ _ hk']
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k j : J
hkj : k ≤ j
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) j)
have isMin : ∀ (k_1 : J) (hk : IsMin k_1) (hkj : k ≤ k_1),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k_1)
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin k hk =>
    obtain rfl := hk.eq_bot
    obtain rfl : k = ⊥ := by simpa using hkj
    rfl
  | succ k' hk' hkk' =>
    obtain hkj | rfl := hkj.lt_or_eq
    · refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
      dsimp
      rw [transfiniteIterate_succ _ _ _ hk']
      apply hφ
    · rfl
  | isSuccLimit k' hk' _ =>
    obtain hkj | rfl := hkj.lt_or_eq
    · dsimp
      rw [transfiniteIterate_limit _ _ _ hk']
      exact le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩
    · rfl
Cleared hypotheses: j, hkj
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k j : J
hkj : k ≤ j
isMin :
  ∀ (k_1 : J) (hk : IsMin k_1) (hkj : k ≤ k_1),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k_1)
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) j)
have succ : ∀ (k' : J) (hk' : ¬IsMax k')
  (hkk' :
    ∀ (hkj : k ≤ k'),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k'))
  (hkj : k ≤ Order.succ k'),
  LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin k hk =>
    obtain rfl := hk.eq_bot
    obtain rfl : k = ⊥ := by simpa using hkj
    rfl
  | succ k' hk' hkk' =>
    obtain hkj | rfl := hkj.lt_or_eq
    · refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
      dsimp
      rw [transfiniteIterate_succ _ _ _ hk']
      apply hφ
    · rfl
  | isSuccLimit k' hk' _ =>
    obtain hkj | rfl := hkj.lt_or_eq
    · dsimp
      rw [transfiniteIterate_limit _ _ _ hk']
      exact le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩
    · rfl
Cleared hypotheses: j, hkj