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

Proof state:
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 ≤ ⊥
⊢ k = ⊥

Tactic:
simpa using hkj

Result:
no goals

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'
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) k'

Tactic:
dsimp

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'
⊢ transfiniteIterate φ k i₀ ≤ transfiniteIterate φ k' i₀

Proof state:
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
⊢ Monotone fun j => transfiniteIterate φ j i₀

Tactic:
intro k j hkj

Result:
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 : J
hkj : k ≤ j
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) j

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
hk : IsMin ⊥
hkj : ⊥ ≤ ⊥
⊢ (fun j => transfiniteIterate φ j i₀) ⊥ ≤ (fun j => transfiniteIterate φ j i₀) ⊥

Tactic:
rfl

Result:
no goals

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 : J
hk : IsMin ⊥
hkj : k ≤ ⊥
⊢ (fun j => transfiniteIterate φ j i₀) k ≤ (fun j => transfiniteIterate φ j i₀) ⊥

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

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
hk : IsMin ⊥
hkj : ⊥ ≤ ⊥
⊢ (fun j => transfiniteIterate φ j i₀) ⊥ ≤ (fun j => transfiniteIterate φ j 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₀ ≤ transfiniteIterate φ k' i₀

Tactic:
rw [transfiniteIterate_limit _ _ _ hk']

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'
⊢ transfiniteIterate φ k i₀ ≤ ⨆ x, transfiniteIterate φ (↑x) i₀

Proof state:
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')

Tactic:
rfl

Result:
no goals