awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.TransfiniteIteration
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
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) ⋯)
        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)
⊢ transfiniteIterate φ j i₀ = ⨆ (x : (↑(Set.Iio j) : Type w)), transfiniteIterate φ (↑x : J) i₀

Tactic:
dsimp [transfiniteIterate]

Premises used: transfiniteIterate
-- Module: Mathlib.Order.TransfiniteIteration
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
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) ⋯ :
              I → I))
          (↑x : J) ⋯)
      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₀)
⊢ 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)

Tactic:
rw [SuccOrder.limitRecOn_of_isSuccLimit _ _ _ hj]

Premises used: SuccOrder.limitRecOn_of_isSuccLimit
-- Module: Mathlib.Order.TransfiniteIteration
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)
    ((⨆ (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) ⋯ :
              I → I))
          (↑x : J) ⋯)
      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₀)

Tactic:
simp only [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.Order.TransfiniteIteration
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
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₀) ⊥)
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k_1) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)

Tactic:
obtain rfl := hk.eq_bot

Premises used: IsMin.eq_bot, rfl
-- Module: Mathlib.Order.TransfiniteIteration
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 ≤ ⊥
⊢ k = ⊥

Tactic:
simpa using hkj
-- Module: Mathlib.Order.TransfiniteIteration
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 ≤ ⊥
isMin :
  ∀ (hkj : LE.le.{w} (α := J) ⊥ ⊥),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥)
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥)

Tactic:
obtain rfl : k = ⊥ := by simpa using hkj

Premises used: rfl
-- Module: Mathlib.Order.TransfiniteIteration
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
hk : IsMin.{w} (α := J) ⊥
hkj : LE.le.{w} (α := J) ⊥ ⊥
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥) ((fun (j : J) ↦ transfiniteIterate φ j i₀) ⊥)

Tactic:
rfl
-- Module: Mathlib.Order.TransfiniteIteration
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'))
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'))
⊢ 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

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Order.TransfiniteIteration
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'))

Tactic:
(hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_

Premises used: Iff.mp, Order.lt_succ_iff_of_not_isMax, LE.le.trans
-- Module: Mathlib.Order.TransfiniteIteration
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'
succ :
  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'))

Tactic:
refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_

Premises used: Iff.mp, Order.lt_succ_iff_of_not_isMax, LE.le.trans
-- Module: Mathlib.Order.TransfiniteIteration
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'
succ : transfiniteIterate φ k' i₀ ≤ transfiniteIterate φ (Order.succ k') i₀
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
    ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))

Tactic:
dsimp
-- Module: Mathlib.Order.TransfiniteIteration
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'
succ : transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)
⊢ transfiniteIterate φ k' i₀ ≤ transfiniteIterate φ (Order.succ k') i₀

Tactic:
rw [transfiniteIterate_succ _ _ _ hk']

Premises used: transfiniteIterate_succ
-- Module: Mathlib.Order.TransfiniteIteration
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 φ k' i₀)

Tactic:
apply hφ
-- Module: Mathlib.Order.TransfiniteIteration
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' : ¬IsMax k'
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:
rfl
-- Module: Mathlib.Order.TransfiniteIteration
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')
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)
⊢ 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

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Order.TransfiniteIteration
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'
isSuccLimit : transfiniteIterate φ k i₀ ≤ transfiniteIterate φ k' i₀
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')

Tactic:
dsimp
-- Module: Mathlib.Order.TransfiniteIteration
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'
isSuccLimit : transfiniteIterate φ k i₀ ≤ ⨆ (x : (↑(Set.Iio k') : Type w)), transfiniteIterate φ (↑x : J) i₀
⊢ transfiniteIterate φ k i₀ ≤ transfiniteIterate φ k' i₀

Tactic:
rw [transfiniteIterate_limit _ _ _ hk']

Premises used: transfiniteIterate_limit
-- Module: Mathlib.Order.TransfiniteIteration
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₀ ≤ ⨆ (x : (↑(Set.Iio k') : Type w)), transfiniteIterate φ (↑x : J) i₀

Tactic:
le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩

Premises used: Set.Mem, le_iSup
-- Module: Mathlib.Order.TransfiniteIteration
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₀ ≤ ⨆ (x : (↑(Set.Iio k') : Type w)), transfiniteIterate φ (↑x : J) i₀

Tactic:
exact le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩

Premises used: le_iSup
-- Module: Mathlib.Order.TransfiniteIteration
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' : 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)

Tactic:
rfl
-- Module: Mathlib.Order.TransfiniteIteration
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)
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'))
isSuccLimit :
  ∀ (k' : J) (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')
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) j)

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

Premises used: LE.le.lt_or_eq, le_iSup, rfl
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
pos : ∀ (hi : i = ⊤), i ≤ φ i
neg : ∀ (hi : ¬i = ⊤), i ≤ φ i
⊢ i ≤ φ i

Tactic:
by_cases hi : i = ⊤
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
hi : i = ⊤
pos : ⊤ ≤ φ ⊤
⊢ i ≤ φ i

Tactic:
subst hi
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
pos pos₁ : LE.le.{u} (α := I) ⊤ ⊤
⊢ ⊤ ≤ φ ⊤

Tactic:
rw [φtop]
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
hi : ¬i = ⊤
⊢ i ≤ φ i

Tactic:
(hφ' i hi).le

Premises used: LT.lt.le
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
hi : ¬i = ⊤
⊢ i ≤ φ i

Tactic:
exact (hφ' i hi).le

Premises used: LT.lt.le
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
⊢ ∀ (i : I), i ≤ φ i

Tactic:
have hφ (i : I) : i ≤ φ i := by
    by_cases hi : i = ⊤
    · subst hi
      rw [φtop]
    · exact (hφ' i hi).le
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
⊢ ∃ (j₁ : J) (j₂ : J) (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
grind [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
obtain :
  ∀ (j₁ j₂ : J) (hj : j₁ < j₂) (eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀),
    ∃ (j : J), transfiniteIterate φ j i₀ = ⊤
⊢ ∃ (j : J), transfiniteIterate φ j i₀ = ⊤

Tactic:
obtain ⟨j₁, j₂, hj, eq⟩ : ∃ (j₁ j₂ : J) (hj : j₁ < j₂),
      transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀ := by
    grind [Function.Injective]
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
by_contra! : ∀ (this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤), False
⊢ ∃ (j : J), transfiniteIterate φ j i₀ = ⊤

Tactic:
by_contra!
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this_1 : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
this : transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
⊢ False

Tactic:
simp only [eq, lt_self_iff_false] at this

Premises used: lt_self_iff_false
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
suffices : transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
⊢ False

Tactic:
suffices transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀ by
    simp only [eq, lt_self_iff_false] at this
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
simp : ∃ (b : J), j₁ < b
⊢ ¬IsMax j₁

Tactic:
simp only [not_isMax_iff]

Premises used: not_isMax_iff
-- Module: Mathlib.Order.TransfiniteIteration
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 < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ ∃ (b : J), j₁ < b

Tactic:
⟨_, hj⟩

Premises used: Exists.intro