awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
inl : HMul.hMul (α := R) (β := R) (0 : R) ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have inl₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hv : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have inr : HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R) (0 : R) = 0
Tactic: rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hv : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
inr : HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R) (0 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have inr₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) ψ : R) =
    0
have h₁ : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∨
  (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
Tactic: suffices toLex u < lexOrder φ ∨ toLex v < lexOrder ψ by
    rcases this with (hu | hv)
    · rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]
    · rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder ∨
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ))) < ψ.lexOrder
have h₁ : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))) →
  ¬ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
Tactic: rw [or_iff_not_imp_left, not_lt, ← not_le]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ)))
hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
⊢ False
have h₁ : ∀ (hd : ¬φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))) (u v : σ →₀ ℕ)
  (h : u + v = d) (hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ))))
  (hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))), False
Tactic: rw [← not_le] at hd
Cleared hypotheses: hd, u, v, h, hu, hv
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ¬φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) u) : WithTop (Lex (σ →₀ ℕ)))
hv : ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) v) : WithTop (Lex (σ →₀ ℕ)))
⊢ False
have h₁ : φ.lexOrder + ψ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have inl : (0 * ψ).lexOrder = lexOrder.{u_1, u_2} (R := R) 0 + ψ.lexOrder
Tactic: obtain rfl | hφ := eq_or_ne φ 0
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
inst_3 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
inl : (0 * ψ).lexOrder = lexOrder.{u_1, u_2} (R := R) 0 + ψ.lexOrder
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have inr : ∀ (hφ : φ ≠ 0), (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
Tactic: obtain rfl | hφ := eq_or_ne φ 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have inr : (φ * 0).lexOrder = φ.lexOrder + lexOrder.{u_1, u_2} (R := R) 0
Tactic: obtain rfl | hψ := eq_or_ne ψ 0
Cleared hypotheses: ψ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
inr : (φ * 0).lexOrder = φ.lexOrder + lexOrder.{u_1, u_2} (R := R) 0
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have inr₁ : ∀ (hψ : ψ ≠ 0), (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
Tactic: obtain rfl | hψ := eq_or_ne ψ 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have inr : ∀ (p : σ →₀ ℕ) (hp : φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ)))),
  (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
Tactic: rcases exists_finsupp_eq_lexOrder_of_ne_zero hφ with ⟨p, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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 (σ →₀ ℕ)))
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have inr : ∀ (q : σ →₀ ℕ) (hq : ψ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ)))),
  (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
Tactic: rcases exists_finsupp_eq_lexOrder_of_ne_zero hψ with ⟨q, hq⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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 (σ →₀ ℕ)))
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder
have apply : (φ * ψ).lexOrder ≤ φ.lexOrder + ψ.lexOrder
Tactic: apply le_antisymm _ (lexOrder_mul_ge φ ψ)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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 (σ →₀ ℕ)))
⊢ (φ * ψ).lexOrder ≤ φ.lexOrder + ψ.lexOrder
have rw : (φ * ψ).lexOrder ≤
  HAdd.hAdd (α := WithTop (Lex (σ →₀ ℕ))) (β := WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
    ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
Tactic: rw [hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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 (σ →₀ ℕ)))
⊢ (φ * ψ).lexOrder ≤
    HAdd.hAdd (α := WithTop (Lex (σ →₀ ℕ))) (β := WithTop (Lex (σ →₀ ℕ)))
      ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
      ((↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) q) : WithTop (Lex (σ →₀ ℕ))) : WithTop (Lex (σ →₀ ℕ)))
have apply : Ne.{u_2 + 1} (α := R) ((coeff (p + q) : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)
Tactic: apply lexOrder_le_of_coeff_ne_zero (d := p + q)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
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 + q) : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) (0 : R)
have 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)
Tactic: rw [coeff_mul_of_add_lexOrder hp hq, mul_ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (x + y) : R)
have rw : HAdd.hAdd (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
    ((coeff e : (a : MvPowerSeries σ R) → R) y : R) ∈
  Jd.1
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)
have 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
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ ∑ 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
have 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
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)
have 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
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))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)
have 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
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))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)
have 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
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ ∑ 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
have 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
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)
have 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
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))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ Membership.mem (α := R) Jd.1 ((coeff e : (a : MvPowerSeries σ R) → R) (f * g) : R)
have 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
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))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
Goal:
σ : 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
have mp : basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d
have mpr : J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
Goal:
σ : 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
have 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
Tactic: simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', setOf_subset_setOf]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ (↑J : Set R) ⊆ (↑K : Set R) ∧ e ≤ d
have mp : (↑J : Set R) ⊆ (↑K : Set R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
⊢ (↑J : Set R) ⊆ (↑K : Set R) ∧ e ≤ d
have mp₁ : e ≤ d
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
have rw : (if d' = 0 then x else 0) ∈ J
Tactic: rw [coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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' : σ →₀ ℕ
⊢ (if d' = 0 then x else 0) ∈ J
have pos : d' = 0 → x ∈ J
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (if d' = 0 then x else 0) ∈ J
have neg : ¬d' = 0 → 0 ∈ J
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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' : σ →₀ ℕ
⊢ (if d' = 0 then x else 0) ∈ J
have pos : d' = 0 → x ∈ J
Tactic: split_ifs <;> [exact hx; exact J.zero_mem]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ (if d' = 0 then x else 0) ∈ J
have neg : ¬d' = 0 → 0 ∈ J
Tactic: split_ifs <;> [exact hx; exact J.zero_mem]