[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ ↑(⨅ (i : ι), f i) x = iInf (fun i => ↑(f i)) x
[PROOFSTEP]
simp [iInf_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)
[PROOFSTEP]
funext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ ↑(⨆ (i : ι), f i) x = iSup (fun i => ↑(f i)) x
[PROOFSTEP]
simp [iSup_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
src✝² : Lattice (α →o β) := lattice
src✝¹ : OrderTop (α →o β) := orderTop
src✝ : OrderBot (α →o β) := orderBot
s : Set (α →o β)
f : α →o β
hf : f ∈ s
x : α
⊢ toFun f x ≤ ⨆ (_ : f ∈ s), ↑f x
[PROOFSTEP]
apply le_iSup _ hf
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (a₁ a₂ : α), ↑f (a₁ ⊔ a₂) ≤ ↑f a₁ ⊔ a₂) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (↑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (↑f)^[n₁] a₁ ⊔ (↑f)^[n₂] a₂
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
exact h 1 0
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
intro n₁ n₂ a₁ a₂
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ := by
  intro n
  induction' n with n ih <;> intro a₁ a₂
  · rfl
  ·
    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]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
intro n
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
intro a₁ a₂
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
intro a₁ a₂
[GOAL]
case zero
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
rfl
[GOAL]
case succ
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
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]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
rw [← Function.iterate_succ_apply]
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂
[PROOFSTEP]
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₁ _
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₁))
[PROOFSTEP]
rw [sup_comm]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : Preorder α✝
α : Type u_3
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₂)
[PROOFSTEP]
rw [sup_comm]
