Theorem: MvPowerSeries.idealIsBasis (DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ⊓ basis σ α e
Tactic:
use d ⊔ e
State after:
case h
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
d e : σ →₀ ℕ
⊢ basis σ α (d ⊔ e) ≤ basis σ α d ⊓ basis σ α e

State before:
case h
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
d e : σ →₀ ℕ
⊢ basis σ α (d ⊔ e) ≤ basis σ α d ⊓ basis σ α e
Tactic:
apply Antitone.map_sup_le (basis_antitone σ α)
State after:
no goals