awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s * φ) : R) (0 : R)
have rw : Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * X s) : R) (0 : R)
Tactic: rw [← (φ.commute_X s).eq, coeff_zero_mul_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
rw : Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * X s) : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s * φ) : R) (0 : R)
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [← (φ.commute_X s).eq, coeff_zero_mul_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
a : R
⊢ a • f = HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) f
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (a • f) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) f) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq (α := MvPowerSeries σ R) (X s) (X t)
⊢ s = t
have h₁ : Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
  ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)
Tactic: replace h := congr_arg (coeff (single s 1)) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h :
  Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
    ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)
⊢ s = t
have h₁ : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)
Tactic: rw [coeff_X, if_pos rfl, coeff_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)
⊢ s = t
have pos : ∀ (H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 1), s = t
Tactic: split_ifs at h with H
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)
pos : ∀ (H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 1), s = t
⊢ s = t
have neg : ∀ (H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 0), s = t
Tactic: split_ifs at h with H
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 1
⊢ s = t
have H₁ : s = t ∧ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
Tactic: rw [Finsupp.single_eq_single_iff] at H
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : s = t ∧ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
h : Eq.{u_2 + 1} (α := R) 1 1
⊢ s = t
have pos : ∀ (H : s = t ∧ Eq (α := ℕ) 1 1), s = t
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : s = t ∧ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
h : Eq.{u_2 + 1} (α := R) 1 1
pos : ∀ (H : s = t ∧ Eq (α := ℕ) 1 1), s = t
⊢ s = t
have pos₁ : ∀ (H : Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0), s = t
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
h : Eq.{u_2 + 1} (α := R) 1 1
H : Eq (α := ℕ) 1 0 ∧ Eq (α := ℕ) 1 0
⊢ s = t
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)
h : Eq.{u_2 + 1} (α := R) 1 0
⊢ s = t
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
intro : ∀ (h : Eq (α := MvPowerSeries σ R) (X s) (X t)), s = t
⊢ Eq (α := MvPowerSeries σ R) (X s) (X t) → s = t
have intro₁ : ∀
  (h :
    Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
      ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)),
  s = t
Tactic: classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
intro : ∀ (h : Eq (α := MvPowerSeries σ R) (X s) (X t)), s = t
intro₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
        ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)),
    s = t
⊢ Eq (α := MvPowerSeries σ R) (X s) (X t) → s = t
have intro₂ : ∀ (h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)), s = t
Tactic: classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
intro : ∀ (h : Eq (α := MvPowerSeries σ R) (X s) (X t)), s = t
intro₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
        ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)),
    s = t
intro₂ : ∀ (h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)), s = t
⊢ Eq (α := MvPowerSeries σ R) (X s) (X t) → s = t
have pos : ∀ (H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 1), s = t
Tactic: classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Nontrivial R
s t : σ
intro : ∀ (h : Eq (α := MvPowerSeries σ R) (X s) (X t)), s = t
intro₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R)
        ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X t) : R)),
    s = t
intro₂ : ∀ (h : Eq.{u_2 + 1} (α := R) 1 (if Eq (α := σ →₀ ℕ) (single s 1) (single t 1) then 1 else 0)), s = t
pos : ∀ (H : Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 1), s = t
⊢ Eq (α := MvPowerSeries σ R) (X s) (X t) → s = t
have neg : ∀ (H : ¬Eq (α := σ →₀ ℕ) (single s 1) (single t 1)) (h : Eq.{u_2 + 1} (α := R) 1 0), s = t
Tactic: classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
have rw : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
Tactic: rw [coeff_one, coeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
have pos : ∀ (h : n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
pos : ∀ (h : n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
have neg : ∀ (h : ¬n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
have rw : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
Tactic: classical
        rw [coeff_one, coeff_one]
        split_ifs with h
        · simp only [map_one]
        · simp only [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
have rw₁ : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
Tactic: classical
        rw [coeff_one, coeff_one]
        split_ifs with h
        · simp only [map_one]
        · simp only [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
rw₁ rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
have pos : ∀ (h : n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
Tactic: classical
        rw [coeff_one, coeff_one]
        split_ifs with h
        · simp only [map_one]
        · simp only [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
rw₁ rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (if n = 0 then 1 else 0) : S) (if n = 0 then 1 else 0 : S)
pos : ∀ (h : n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S) 1 : S)
have neg : ∀ (h : ¬n = 0), Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: classical
        rw [coeff_one, coeff_one]
        split_ifs with h
        · simp only [map_one]
        · simp only [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
have rw : Eq.{u_3 + 1} (α := S)
  (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
    (f : (a : R) → S)
      (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
  (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
    HMul.hMul (α := S) (β := S)
      ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S))
Tactic: rw [coeff_mul, map_sum, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := S) (β := S)
        ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S))
have apply : ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
  (f : (a : R) → S)
      (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
    HMul.hMul (α := S) (β := S)
      ((coeff x.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff x.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n i j : σ →₀ ℕ
h : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
⊢ (f : (a : R) → S)
      (HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
    HMul.hMul (α := S) (β := S)
      ((coeff (i, j).1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff (i, j).2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S)
have rw : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R) : S)
    ((f : (a : R) → S) ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) ψ : R) : S) =
  HMul.hMul (α := S) (β := S)
    ((coeff (i, j).1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
        (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
      S)
    ((coeff (i, j).2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
        (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
      S)
Tactic: rw [f.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
have rw : Eq.{u_3 + 1} (α := S)
  ((f : (a : R) → S)
      (∑ 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)) :
    S)
  ((coeff n : (a : MvPowerSeries σ S) → S)
      (HMul.hMul (α := MvPowerSeries σ S)
        (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
        (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
    S)
Tactic: classical
        rw [coeff_mul, map_sum, coeff_mul]
        apply Finset.sum_congr rfl
        rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        (∑ 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)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
have rw₁ : Eq.{u_3 + 1} (α := S)
  (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) :
    S)
  ((coeff n : (a : MvPowerSeries σ S) → S)
      (HMul.hMul (α := MvPowerSeries σ S)
        (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
        (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
    S)
Tactic: classical
        rw [coeff_mul, map_sum, coeff_mul]
        apply Finset.sum_congr rfl
        rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        (∑ 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)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
rw₁ :
  Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        (f : (a : R) → S)
          (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
have rw₂ : Eq.{u_3 + 1} (α := S)
  (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
    (f : (a : R) → S)
      (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
  (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
    HMul.hMul (α := S) (β := S)
      ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S))
Tactic: classical
        rw [coeff_mul, map_sum, coeff_mul]
        apply Finset.sum_congr rfl
        rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl