awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)
have rw : lift.{u, max u v} (Module.rank K (MvPolynomial σ K)) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
Tactic: rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
rw : lift.{u, max u v} (Module.rank K (MvPolynomial σ K)) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)
have rw₁ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
Tactic: rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
rw : lift.{u, max u v} (Module.rank K (MvPolynomial σ K)) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
rw₁ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)
have rw₂ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{max v u, u} #(σ →₀ ℕ)
Tactic: rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
rw : lift.{u, max u v} (Module.rank K (MvPolynomial σ K)) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
rw₁ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{u, max u v} (lift.{v, u} #(σ →₀ ℕ))
rw₂ : lift.{max u v, u} #(σ →₀ ℕ) = lift.{max v u, u} #(σ →₀ ℕ)
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)
have rw₃ : lift.{v, u} #(σ →₀ ℕ) = lift.{v, u} #(σ →₀ ℕ)
Tactic: rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank, lift_lift, lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
σ : Type v
⊢ Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)
have rw : lift.{v, v} (Module.rank K (MvPolynomial σ K)) = lift.{v, v} #(σ →₀ ℕ)
Tactic: rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
K : Type v
inst : CommRing K
inst_1 : Nontrivial K
σ : Type v
rw : lift.{v, v} (Module.rank K (MvPolynomial σ K)) = lift.{v, v} #(σ →₀ ℕ)
⊢ Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)
have rw₁ : lift.{v, v} #(σ →₀ ℕ) = lift.{v, v} #(σ →₀ ℕ)
Tactic: rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : IsEmpty σ
⊢ Module.rank K (MvPolynomial σ K) = 1
have inl : Subsingleton K → Module.rank K (MvPolynomial σ K) = 1
Tactic: cases subsingleton_or_nontrivial K
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial (goal)
Goal:
σ : Type u
K : Type v
inst : CommRing K
inst_1 : IsEmpty σ
inl : Subsingleton K → Module.rank K (MvPolynomial σ K) = 1
⊢ Module.rank K (MvPolynomial σ K) = 1
have inr : Nontrivial K → Module.rank K (MvPolynomial σ K) = 1
Tactic: cases subsingleton_or_nontrivial K
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) =
    if m = n then a else 0
have dsimp : (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
    ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
  if m = n then a else 0
Tactic: dsimp only [coeff, MvPowerSeries]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
    if m = n then a else 0
have rw : (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
    (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a :
      (σ →₀ ℕ) → R) =
  if m = n then a else 0
Tactic: rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
rw :
  (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a :
        (σ →₀ ℕ) → R) =
    if m = n then a else 0
⊢ (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
    if m = n then a else 0
have rw₁ : ((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a m =
  if m = n then a else 0
Tactic: rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
rw :
  (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a :
        (σ →₀ ℕ) → R) =
    if m = n then a else 0
rw₁ :
  ((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a m =
    if m = n then a else 0
⊢ (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
    if m = n then a else 0
have rw₂ : Pi.single (M := fun (x : σ →₀ ℕ) ↦ R) n a m = if m = n then a else 0
Tactic: rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m n : σ →₀ ℕ
a : R
rw :
  (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a :
        (σ →₀ ℕ) → R) =
    if m = n then a else 0
rw₁ :
  ((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → (σ →₀ ℕ) → R) a m =
    if m = n then a else 0
rw₂ : Pi.single (M := fun (x : σ →₀ ℕ) ↦ R) n a m = if m = n then a else 0
⊢ (LinearMap.proj (φ := fun (a : σ →₀ ℕ) ↦ R) m : (a : (σ →₀ ℕ) → R) → R)
      ((monomial n : (a : R) → (σ →₀ ℕ) → R) a : (σ →₀ ℕ) → R) =
    if m = n then a else 0
have rw₃ : (if m = n then a else 0) = if m = n then a else 0
Tactic: rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = a
have rw : (coeff n : (a : MvPowerSeries σ R) → R)
    (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
      MvPowerSeries σ R) =
  a
Tactic: rw [monomial_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = a
have rw : (coeff n : (a : MvPowerSeries σ R) → R)
    (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
      MvPowerSeries σ R) =
  a
Tactic: classical
  rw [monomial_def]
  exact Pi.single_eq_same _ _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)
have rw : Eq.{u_2 + 1} (α := R)
  ((coeff m : (a : MvPowerSeries σ R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
        MvPowerSeries σ R) :
    R)
  (0 : R)
Tactic: rw [monomial_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)
have rw : Eq.{u_2 + 1} (α := R)
  ((coeff m : (a : MvPowerSeries σ R) → R)
      (((LinearMap.single R (fun (x : σ →₀ ℕ) ↦ R) n : R →ₗ[R] (i : σ →₀ ℕ) → R) : (a : R) → MvPowerSeries σ R) a :
        MvPowerSeries σ R) :
    R)
  (0 : R)
Tactic: classical
  rw [monomial_def]
  exact Pi.single_eq_of_ne h _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst_1 : DecidableEq σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R) :
      R)
have refine : @antidiagonal _ Finsupp.instAddMonoid _ n = @antidiagonal _ Finsupp.instAddMonoid _ n
Tactic: refine Finset.sum_congr ?_ fun _ _ => rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst_1 : DecidableEq σ
⊢ @antidiagonal _ Finsupp.instAddMonoid _ n = @antidiagonal _ Finsupp.instAddMonoid _ n
have rw : @antidiagonal _ Finsupp.instAddMonoid _ n = @antidiagonal _ Finsupp.instAddMonoid _ n
Tactic: rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have this : ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
  HMul.hMul (α := R) (β := R)
        ((coeff p.1 : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
      0 →
    p.1 = n
Tactic: have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this :
  ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
          ((coeff p.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
        0 →
      p.1 = n
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have rw : (if n ≤ m then
    ∑ x ∈ {(n, m - n)},
      HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)
  else
    ∑ x ∈ ∅,
      HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)) =
  if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
Tactic: rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
    Finset.sum_ite_index]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have have : ∀
  (this :
    ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
      HMul.hMul (α := R) (β := R)
            ((coeff p.1 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R)
            ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
          0 →
        p.1 = n),
  (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
Tactic: classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
    Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
have have₁ have₂ :
  ∀
    (this :
      ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
        HMul.hMul (α := R) (β := R)
              ((coeff p.1 : (a : MvPowerSeries σ R) → R)
                  ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
                R)
              ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
            0 →
          p.1 = n),
    (coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
      if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
have have₃ : ∀
  (this :
    ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
      HMul.hMul (α := R) (β := R)
            ((coeff p.1 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R)
            ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) ≠
          0 →
        p.1 = n),
  (if n ≤ m then
      ∑ x ∈ {(n, m - n)},
        HMul.hMul (α := R) (β := R)
          ((coeff x.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)
    else
      ∑ x ∈ ∅,
        HMul.hMul (α := R) (β := R)
          ((coeff x.1 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R)) =
    if n ≤ m then HMul.hMul (β := R) a ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) else 0
Tactic: classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_fst_eq_antidiagonal _ n,
    Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
have this : ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
  HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R) ≠
      0 →
    p.2 = n
Tactic: have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this :
  ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R) ≠
        0 →
      p.2 = n
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
have rw : (if n ≤ m then
    ∑ x ∈ {(m - n, n)},
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
  else
    ∑ x ∈ ∅,
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)) =
  if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
Tactic: rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
    Finset.sum_ite_index]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
have have : ∀
  (this :
    ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff p.2 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R) ≠
          0 →
        p.2 = n),
  (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
Tactic: classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
    Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
have have₁ have₂ :
  ∀
    (this :
      ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff p.2 : (a : MvPowerSeries σ R) → R)
                  ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
                R) ≠
            0 →
          p.2 = n),
    (coeff m : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
      if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
⊢ (coeff m : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
have have₃ : ∀
  (this :
    ∀ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff p.2 : (a : MvPowerSeries σ R) → R)
                ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
              R) ≠
          0 →
        p.2 = n),
  (if n ≤ m then
      ∑ x ∈ {(m - n, n)},
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
    else
      ∑ x ∈ ∅,
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R)
              ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)) =
    if n ≤ m then HMul.hMul (α := R) ((coeff (m - n) : (a : MvPowerSeries σ R) → R) φ : R) a else 0
Tactic: classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff p.2 (monomial n a) ≠ 0 → p.2 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
    Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff (m + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    HMul.hMul (β := R) a ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
have hc : m ≤ m + n
Tactic: rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff (m + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((monomial n : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    HMul.hMul (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) a
have hc : n ≤ m + n
Tactic: rw [coeff_mul_monomial, if_pos, add_tsub_cancel_right]