-- Mathlib/Order/TransfiniteIteration.lean
lemma monotone_transfiniteIterate (hφ : ∀ (i : I), i ≤ φ i) :
    Monotone (fun (j : J) ↦ transfiniteIterate φ j i₀)

Proof state:
case hl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
a✝ : ∀ b < k', k ≤ b → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) b
hkj : k ≤ k'
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'

Tactic:
obtain hkj | rfl := hkj.lt_or_eq

Result:
case hl.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
a✝ : ∀ b < k', k ≤ b → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) b
hkj✝ : k ≤ k'
hkj : k < k'
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'

case hl.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk' : Order.IsSuccLimit k
a✝ : ∀ b < k, k ≤ b → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) b
hkj : k ≤ k
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k

Proof state:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ (fun j => transfiniteIterate φ j i₀) k' ≤ (fun j => transfiniteIterate φ j i₀) (Order.succ k')

Tactic:
dsimp

Result:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ transfiniteIterate φ (Order.succ k') i₀

Proof state:
case hm
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k✝ k : J
hk : IsMin k
hkj : k✝ ≤ k
⊢ (fun j => transfiniteIterate φ j i₀) k✝ ≤ (fun j => transfiniteIterate φ j i₀) k

Tactic:
obtain rfl := hk.eq_bot

Result:
case hm
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk : IsMin ⊥
hkj : k ≤ ⊥
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) ⊥

Proof state:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) (Order.succ k')

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

Result:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ (fun j => transfiniteIterate φ j i₀) k' ≤ (fun j => transfiniteIterate φ j i₀) (Order.succ k')

Proof state:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)

Tactic:
apply hφ

Result:
no goals

Proof state:
case hl.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk' : Order.IsSuccLimit k
a✝ : ∀ b < k, k ≤ b → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) b
hkj : k ≤ k
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k

Tactic:
rfl

Result:
no goals

Proof state:
case hs
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj : k ≤ Order.succ k'
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) (Order.succ k')

Tactic:
obtain hkj | rfl := hkj.lt_or_eq

Result:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) (Order.succ k')

case hs.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k' : J
hk' : ¬IsMax k'
hkk' :
  Order.succ k' ≤ k' → (fun j => transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj : Order.succ k' ≤ Order.succ k'
⊢ (fun j => transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j => transfiniteIterate φ j i₀) (Order.succ k')

Proof state:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ transfiniteIterate φ (Order.succ k') i₀

Tactic:
rw [transfiniteIterate_succ _ _ _ hk']

Result:
case hs.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)

Proof state:
case hl.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : Order.IsSuccLimit k'
a✝ : ∀ b < k', k ≤ b → (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) b
hkj✝ : k ≤ k'
hkj : k < k'
⊢ transfiniteIterate φ k i₀ ≤ ⨆ x, transfiniteIterate φ (↑x) i₀

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

Result:
no goals