case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), i ≥ n → u i ≤ ⨆ (i : ℕ), u (i + n)

case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ) (_ : i ≥ n), u i
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ (⨆ (i : ℕ) (_ : i ≥ n), u i) = ⨆ (i : ℕ), u (i + n)
apply le_antisymm <;> simp only [iSup_le_iff]
case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i => u (i + n)) (i - n) = u i
case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), i ≥ n → u i ≤ ⨆ (i : ℕ), u (i + n)
refine fun i hi => le_sSup ⟨i - n, ?_⟩
case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i
case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ (fun i => u (i + n)) (i - n) = u i
dsimp only
no goals
case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n i : ℕ
hi : i ≥ n
⊢ u (i - n + n) = u i
rw [Nat.sub_add_cancel hi]
no goals
case a
α : Type u_1
β : Type ?u.176393
β₂ : Type ?u.176396
γ : Type ?u.176399
ι : Sort ?u.176402
ι' : Sort ?u.176405
κ : ι → Sort ?u.176410
κ' : ι' → Sort ?u.176415
inst✝ : CompleteLattice α
f g s t : ι → α
a b : α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ) (_ : i ≥ n), u i
exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩