α : Type u_1
β : Type ?u.181361
β₂ : Type ?u.181364
γ : Type ?u.181367
ι : Sort ?u.181370
ι' : Sort ?u.181373
κ : ι → Sort ?u.181378
κ' : ι' → Sort ?u.181383
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
⊢ (⨅ (i : ℕ) (_ : i > 0), f i) = ⨅ (b : ℕ) (_ : b ∈ {i | 0 < i}), f b
α : Type u_1
β : Type ?u.181361
β₂ : Type ?u.181364
γ : Type ?u.181367
ι : Sort ?u.181370
ι' : Sort ?u.181373
κ : ι → Sort ?u.181378
κ' : ι' → Sort ?u.181383
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
⊢ (⨅ (i : ℕ) (_ : i > 0), f i) = ⨅ (i : ℕ), f (i + 1)
rw [← iInf_range, Nat.range_succ]
no goals
α : Type u_1
β : Type ?u.181361
β₂ : Type ?u.181364
γ : Type ?u.181367
ι : Sort ?u.181370
ι' : Sort ?u.181373
κ : ι → Sort ?u.181378
κ' : ι' → Sort ?u.181383
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : ℕ → α
⊢ (⨅ (i : ℕ) (_ : i > 0), f i) = ⨅ (b : ℕ) (_ : b ∈ {i | 0 < i}), f b
simp