awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
q : σ →₀ ℕ
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
apply : Ne.{u_2 + 1} (α := R) ((coeff (p + q) : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)
⊢ (φ * ψ).lexOrder ≤
    HAdd.hAdd (α := WithTop (Lex (σ →₀ ℕ))) (β := WithTop (Lex (σ →₀ ℕ)))
      ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
      ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
apply lexOrder_le_of_coeff_ne_zero (d := p + q)

Premises used: MvPowerSeries.lexOrder_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
q : σ →₀ ℕ
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
rw :
  Ne.{u_2 + 1} (α := R) ((coeff p : (a : MvPowerSeries σ R) → R) φ : R) (0 : R) ∧
    Ne.{u_2 + 1} (α := R) ((coeff q : (a : MvPowerSeries σ R) → R) ψ : R) (0 : R)
⊢ Ne.{u_2 + 1} (α := R) ((coeff (p + q) : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)

Tactic:
rw [coeff_mul_of_add_lexOrder hp hq, mul_ne_zero_iff]

Premises used: MvPowerSeries.coeff_mul_of_add_lexOrder, mul_ne_zero_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
q : σ →₀ ℕ
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
⊢ Ne.{u_2 + 1} (α := R) ((coeff p : (a : MvPowerSeries σ R) → R) φ : R) (0 : R) ∧
    Ne.{u_2 + 1} (α := R) ((coeff q : (a : MvPowerSeries σ R) → R) ψ : R) (0 : R)

Tactic:
⟨coeff_ne_zero_of_lexOrder hp.symm, coeff_ne_zero_of_lexOrder hq.symm⟩

Premises used: MvPowerSeries.coeff_ne_zero_of_lexOrder, And.intro, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
hφ : φ ≠ 0
hψ : ψ ≠ 0
p : σ →₀ ℕ
hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))
q : σ →₀ ℕ
hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))
⊢ Ne.{u_2 + 1} (α := R) ((coeff p : (a : MvPowerSeries σ R) → R) φ : R) (0 : R) ∧
    Ne.{u_2 + 1} (α := R) ((coeff q : (a : MvPowerSeries σ R) → R) ψ : R) (0 : R)

Tactic:
exact ⟨coeff_ne_zero_of_lexOrder hp.symm, coeff_ne_zero_of_lexOrder hq.symm⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
⊢ Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} 0

Tactic:
simp [coeff_zero]

Premises used: MvPowerSeries.coeff_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
x y : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} x
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} y
e : σ →₀ ℕ
he : e ≤ Jd.2
rw :
  HAdd.hAdd (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) y : R) ∈
    Jd.1
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (x + y) : R)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
x y : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} x
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} y
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ HAdd.hAdd (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) y : R) ∈
    Jd.1

Tactic:
add_mem (hf e he) (hg e he)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
x y : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} x
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} y
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ HAdd.hAdd (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) y : R) ∈
    Jd.1

Tactic:
exact add_mem (hf e he) (hg e he)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} f
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (-f) : R)

Tactic:
simp only [map_neg, neg_mem, hf e he]

Premises used: map_neg, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} g
e : σ →₀ ℕ
he : e ≤ Jd.2
rw :
  ∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)

Tactic:
rw [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} g
e : σ →₀ ℕ
he : e ≤ Jd.2
h :
  ∀ c ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
    HMul.hMul (α := R) (β := R) ((coeff c.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff c.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
      Jd.1
⊢ ∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} g
e : σ →₀ ℕ
he : e ≤ Jd.2
uv : (σ →₀ ℕ) × (σ →₀ ℕ)
huv : uv ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e
⊢ HMul.hMul (α := R) (β := R) ((coeff uv.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff uv.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1

Tactic:
TwoSidedIdeal.mul_mem_left _ _ _ (hg _ (le_trans (Finset.antidiagonal.snd_le huv) he))

Premises used: TwoSidedIdeal.mul_mem_left, Set.Mem, setOf, Finset.antidiagonal.snd_le, le_trans
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} g
e : σ →₀ ℕ
he : e ≤ Jd.2
uv : (σ →₀ ℕ) × (σ →₀ ℕ)
huv : uv ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e
⊢ HMul.hMul (α := R) (β := R) ((coeff uv.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff uv.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1

Tactic:
exact TwoSidedIdeal.mul_mem_left _ _ _ (hg _ (le_trans (Finset.antidiagonal.snd_le huv) he))

Premises used: TwoSidedIdeal.mul_mem_left, Finset.antidiagonal.snd_le, le_trans
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hg :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} g
e : σ →₀ ℕ
he : e ≤ Jd.2
rw rw₁ rw₂ :
  ∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1
h h₁ :
  ∀ (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) (huv : uv ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e),
    HMul.hMul (α := R) (β := R) ((coeff uv.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff uv.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
      Jd.1
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)

Tactic:
classical
      rw [coeff_mul]
      apply sum_mem
      rintro uv huv
      exact TwoSidedIdeal.mul_mem_left _ _ _ (hg _ (le_trans (Finset.antidiagonal.snd_le huv) he))

Premises used: sum_mem, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} f
e : σ →₀ ℕ
he : e ≤ Jd.2
rw :
  ∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)

Tactic:
rw [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} f
e : σ →₀ ℕ
he : e ≤ Jd.2
h :
  ∀ c ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
    HMul.hMul (α := R) (β := R) ((coeff c.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff c.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
      Jd.1
⊢ ∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} f
e : σ →₀ ℕ
he : e ≤ Jd.2
uv : (σ →₀ ℕ) × (σ →₀ ℕ)
huv : uv ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e
⊢ HMul.hMul (α := R) (β := R) ((coeff uv.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff uv.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1

Tactic:
TwoSidedIdeal.mul_mem_right _ _ _ (hf _ (le_trans (Finset.antidiagonal.fst_le huv) he))

Premises used: TwoSidedIdeal.mul_mem_right, Set.Mem, setOf, Finset.antidiagonal.fst_le, le_trans
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} f
e : σ →₀ ℕ
he : e ≤ Jd.2
uv : (σ →₀ ℕ) × (σ →₀ ℕ)
huv : uv ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e
⊢ HMul.hMul (α := R) (β := R) ((coeff uv.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff uv.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1

Tactic:
exact TwoSidedIdeal.mul_mem_right _ _ _ (hf _ (le_trans (Finset.antidiagonal.fst_le huv) he))

Premises used: TwoSidedIdeal.mul_mem_right, Finset.antidiagonal.fst_le, le_trans
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
f g : MvPowerSeries σ R
hf :
  Membership.mem (γ := Set (MvPowerSeries σ R))
    {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)} f
e : σ →₀ ℕ
he : e ≤ Jd.2
rw rw₁ rw₂ :
  ∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
    Jd.1
h h₁ :
  ∀ (uv : (σ →₀ ℕ) × (σ →₀ ℕ)) (huv : uv ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ e),
    HMul.hMul (α := R) (β := R) ((coeff uv.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff uv.2 : (a : MvPowerSeries σ R) → R) g : R) ∈
      Jd.1
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)

Tactic:
classical
      rw [coeff_mul]
      apply sum_mem
      rintro uv huv
      exact TwoSidedIdeal.mul_mem_right _ _ _ (hf _ (le_trans (Finset.antidiagonal.fst_le huv) he))

Premises used: sum_mem, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
f : MvPowerSeries σ R
Jd : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
⊢ f ∈ basis σ R Jd ↔ ∀ e ≤ Jd.2, Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simp [basis]

Premises used: MvPowerSeries.LinearTopology.basis
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
Jd Ke : Prod.{u_2, u_1} (TwoSidedIdeal R) (σ →₀ ℕ)
hJK : Jd.1 ≤ Ke.1
hed : Ke.2 ≤ Jd.2
⊢ basis σ R Jd ≤ basis σ R Ke

Tactic:
fun _ ↦ forall_imp (fun _ h hue ↦ hJK (h (le_trans hue hed)))

Premises used: Set.Mem, setOf, forall_imp, le_trans
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
mp : basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d
mpr : J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
mp :
  (∀ (a : MvPowerSeries σ R),
      (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
        ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)) →
    (↑J : Set R) ⊆ (↑K : Set R) ∧ e ≤ d
⊢ 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]

Premises used: TwoSidedIdeal.coe_mk', MvPowerSeries.LinearTopology.basis, TwoSidedIdeal.le_iff, Set.setOf_subset_setOf
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
mp : (↑J : Set R) ⊆ (↑K : Set R)
mp₁ : e ≤ d
⊢ (↑J : Set R) ⊆ (↑K : Set R) ∧ e ≤ d

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
rw : (if d' = 0 then x else 0) ∈ J
⊢ Membership.mem (α := R) J
    ((coeff d' : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)

Tactic:
rw [coeff_C]

Premises used: MvPowerSeries.coeff_C
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
pos : d' = 0 → x ∈ J
neg : ¬d' = 0 → 0 ∈ J
⊢ (if d' = 0 then x else 0) ∈ J

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
h_1 : d' = 0
⊢ x ∈ J

Tactic:
hx
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
h_1 : d' = 0
⊢ x ∈ J

Tactic:
exact hx
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
h_1 : ¬d' = 0
⊢ 0 ∈ J

Tactic:
J.zero_mem

Premises used: Set.Mem, setOf, TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
h_1 : ¬d' = 0
⊢ 0 ∈ J

Tactic:
exact J.zero_mem

Premises used: TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
d' : σ →₀ ℕ
pos : d' = 0 → x ∈ J
neg : ¬d' = 0 → 0 ∈ J
pos₁ : d' = 0 → x ∈ J
neg₁ : ¬d' = 0 → 0 ∈ J
⊢ (if d' = 0 then x else 0) ∈ J

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

Premises used: TwoSidedIdeal.zero_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
⊢ ∀ (d' : σ →₀ ℕ),
    Membership.mem (α := R) J
      ((coeff d' : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)

Tactic:
have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
x : R
hx : x ∈ (↑J : Set R)
this :
  ∀ (d' : σ →₀ ℕ),
    Membership.mem (α := R) J
      ((coeff d' : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) x : MvPowerSeries σ R) : R)
⊢ x ∈ (↑K : Set R)

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

Premises used: zero_le, DFunLike.coe, MvPowerSeries.C
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
mp : ∀ (h' : ¬e ≤ d), False
⊢ e ≤ d

Tactic:
by_contra h'
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
mp : K = ⊤
⊢ False

Tactic:
apply hK
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
mp : ⊤ ≤ K
⊢ K = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h :
  ∀ (a : MvPowerSeries σ R),
    (∀ e ≤ d, Membership.mem (α := R) J ((coeff e : (a : MvPowerSeries σ R) → R) a : R)) →
      ∀ e_1 ≤ e, Membership.mem (α := R) K ((coeff e_1 : (a : MvPowerSeries σ R) → R) a : R)
h' : ¬e ≤ d
x : R
mp : Membership.mem (γ := TwoSidedIdeal R) ⊤ x → x ∈ K
⊢ Membership.mem (γ := TwoSidedIdeal R) ⊤ x → x ∈ K

Tactic:
_