-- Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
theorem basis_le_iff {J K : TwoSidedIdeal R} {d e : σ →₀ ℕ} (hK : K ≠ ⊤) :
    basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩ ↔ J ≤ K ∧ e ≤ d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
⊢ (if d' = 0 then x else 0) ∈ J

Tactic:
split_ifs <;> [exact hx; exact J.zero_mem]

Result:
no goals

Proof state:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
⊢ x ∈ ↑K

Tactic:
have (d') : coeff R d' (C σ R x) ∈ J := by
  rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]

Result:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
this : ∀ (d' : σ →₀ ℕ), (coeff R d') ((C σ R) x) ∈ J
⊢ x ∈ ↑K

Proof state:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
⊢ False

Tactic:
apply hK

Result:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
⊢ K = ⊤

Proof state:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
⊢ ⊤ ≤ K

Tactic:
intro x _

Result:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
⊢ x ∈ K

Proof state:
case mpr.intro
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
hJK : J ≤ K
hed : e ≤ d
⊢ basis σ R (J, d) ≤ basis σ R (K, e)

Tactic:
exact basis_le hJK hed

Result:
no goals

Proof state:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
⊢ K = ⊤

Tactic:
rw [eq_top_iff]

Result:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
⊢ ⊤ ≤ K

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d

Tactic:
simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', setOf_subset_setOf]

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ (∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K) → ↑J ⊆ ↑K ∧ e ≤ d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
⊢ (coeff R d') ((C σ R) x) ∈ J

Tactic:
rw [coeff_C]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
⊢ (if d' = 0 then x else 0) ∈ J

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
d' : σ →₀ ℕ
hd'_le : d' ≤ d
⊢ (if d' = e then x else 0) ∈ J

Tactic:
split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]

Result:
no goals

Proof state:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
this : ∀ (d' : σ →₀ ℕ), (coeff R d') ((C σ R) x) ∈ J
⊢ x ∈ ↑K

Tactic:
simpa using h (C σ R x) (fun _ _ ↦ this _) _ (zero_le _)

Result:
no goals

Proof state:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
this : ∀ d' ≤ d, (coeff R d') ((monomial R e) x) ∈ J
⊢ x ∈ K

Tactic:
simpa using h (monomial R e x) this _ le_rfl

Result:
no goals

Proof state:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
⊢ e ≤ d

Tactic:
by_contra h'

Result:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
⊢ False

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ (∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K) → ↑J ⊆ ↑K ∧ e ≤ d

Tactic:
intro h

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
⊢ ↑J ⊆ ↑K ∧ e ≤ d

Proof state:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)

Tactic:
rintro ⟨hJK, hed⟩

Result:
case mpr.intro
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
hJK : J ≤ K
hed : e ≤ d
⊢ basis σ R (J, d) ≤ basis σ R (K, e)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
d' : σ →₀ ℕ
hd'_le : d' ≤ d
⊢ (coeff R d') ((monomial R e) x) ∈ J

Tactic:
rw [coeff_monomial]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
d' : σ →₀ ℕ
hd'_le : d' ≤ d
⊢ (if d' = e then x else 0) ∈ J

Proof state:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
⊢ ↑J ⊆ ↑K

Tactic:
intro x hx

Result:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
x : R
hx : x ∈ ↑J
⊢ x ∈ ↑K

Proof state:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
⊢ x ∈ K

Tactic:
have (d') (hd'_le : d' ≤ d) : coeff R d' (monomial R e x) ∈ J := by
  rw [coeff_monomial]
  split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]

Result:
case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
h' : ¬e ≤ d
x : R
a✝ : x ∈ ⊤
this : ∀ d' ≤ d, (coeff R d') ((monomial R e) x) ∈ J
⊢ x ∈ K