case mp
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂
⊢ ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂

case mpr
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
⊢ ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂) ↔
    ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
constructor <;> intro h
no goals
case mp
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂
⊢ ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
exact h 1 0
case mpr
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂
case mpr
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
⊢ ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂
intro n₁ n₂ a₁ a₂
no goals
case mpr
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
⊢ (↑f^[n₁ + n₂]) (a₁ ⊔ a₂) ≤ (↑f^[n₁]) a₁ ⊔ (↑f^[n₂]) a₂
calc
  (f^[n₁ + n₂]) (a₁ ⊔ a₂) = (f^[n₁]) ((f^[n₂]) (a₁ ⊔ a₂)) :=
    Function.iterate_add_apply f n₁ n₂ _
  _ = (f^[n₁]) ((f^[n₂]) (a₂ ⊔ a₁)) := by rw [sup_comm]
  _ ≤ (f^[n₁]) ((f^[n₂]) a₂ ⊔ a₁) := f.mono.iterate n₁ (h' n₂ _ _)
  _ = (f^[n₁]) (a₁ ⊔ (f^[n₂]) a₂) := by rw [sup_comm]
  _ ≤ (f^[n₁]) a₁ ⊔ (f^[n₂]) a₂ := h' n₁ a₁ _
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
⊢ ∀ (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ ∀ (n : ℕ) (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
intro n
case zero
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ a₁ a₂ : α
⊢ (↑f^[Nat.zero]) (a₁ ⊔ a₂) ≤ (↑f^[Nat.zero]) a₁ ⊔ a₂

case succ
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
a₁ a₂ : α
⊢ (↑f^[Nat.succ n]) (a₁ ⊔ a₂) ≤ (↑f^[Nat.succ n]) a₁ ⊔ a₂
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
⊢ ∀ (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
induction' n with n ih <;> intro a₁ a₂
no goals
case zero
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ a₁ a₂ : α
⊢ (↑f^[Nat.zero]) (a₁ ⊔ a₂) ≤ (↑f^[Nat.zero]) a₁ ⊔ a₂
rfl
no goals
case succ
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
a₁ a₂ : α
⊢ (↑f^[Nat.succ n]) (a₁ ⊔ a₂) ≤ (↑f^[Nat.succ n]) a₁ ⊔ a₂
calc
  (f^[n + 1]) (a₁ ⊔ a₂) = (f^[n]) (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
  _ ≤ (f^[n]) (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
  _ ≤ (f^[n]) (f a₁) ⊔ a₂ := ih _ _
  _ = (f^[n + 1]) a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
no goals
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
a₁ a₂ : α
⊢ (↑f^[n]) (↑f a₁) ⊔ a₂ = (↑f^[n + 1]) a₁ ⊔ a₂
rw [← Function.iterate_succ_apply]
no goals
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
⊢ (↑f^[n₁]) ((↑f^[n₂]) (a₁ ⊔ a₂)) = (↑f^[n₁]) ((↑f^[n₂]) (a₂ ⊔ a₁))
rw [sup_comm]
no goals
α✝ : Type ?u.11841
β : Type ?u.11844
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (↑f^[n]) (a₁ ⊔ a₂) ≤ (↑f^[n]) a₁ ⊔ a₂
⊢ (↑f^[n₁]) ((↑f^[n₂]) a₂ ⊔ a₁) = (↑f^[n₁]) (a₁ ⊔ (↑f^[n₂]) a₂)
rw [sup_comm]