awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
e : σ →₀ ℕ
r : R
rw :
  (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
⊢ subst.{u_1, u_3, u_4, u_5} (R := R) a ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
have rw₁ : HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S) =
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
Tactic: rw [← coe_substAlgHom ha, substAlgHom_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
⊢ Continuous (X := MvPowerSeries σ R) (subst a)
have rw : Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)
Tactic: rw [subst_eq_eval₂]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ Eq.{u_5 + 1} (α := S) ((coeff e : (a : MvPowerSeries τ S) → S) (subst a f) : S)
    (∑ᶠ (d : σ →₀ ℕ),
        HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) :
      S)
have this₁ : HasSum.{u_5, u_1} (α := S) (β := σ →₀ ℕ)
  (Function.comp (β := MvPowerSeries τ S) (⇑(coeff e) : (a : MvPowerSeries τ S) → S) fun (d : σ →₀ ℕ) ↦
      HSMul.hSMul (α := R) (β := MvPowerSeries τ S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
    (σ →₀ ℕ) → S)
  ((coeff e : (a : MvPowerSeries τ S) → S)
      (((aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) sorry : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
            (a : MvPowerSeries σ R) → MvPowerSeries τ S)
          f :
        MvPowerSeries τ S) :
    S)
Tactic: have := ((hasSum_aeval ha.hasEval f).map (coeff e) (continuous_coeff S e))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)
have rw : ∀ (x : σ →₀ ℕ),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: rw [constantCoeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have pos : ∀ (hd : d = 0),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
pos :
  ∀ (hd : d = 0),
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
      0
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have neg : ∀ (hd : ¬d = 0),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ (i : σ), Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have by_contra! : ∀ (hc : ∀ (i : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
    (0 : S)
have obtain : ∀ (i : σ) (hi : Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
  Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
    (0 : S)
Tactic: obtain ⟨i, hi⟩ : ∃ i : σ, d i ≠ 0 := by
        by_contra! hc
        exact hd <| Finsupp.ext hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have this : Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) (0 : S)
Tactic: have : constantCoeff (d.prod fun s e ↦ a s ^ e) = 0 := by
      obtain ⟨i, hi⟩ : ∃ i : σ, d i ≠ 0 := by
        by_contra! hc
        exact hd <| Finsupp.ext hc
      simpa [map_finsuppProd, ha'] using
        Finset.prod_eq_zero (i := i) (by simp [hi]) (by simp [zero_pow hi])
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : ¬d = 0
this :
  Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
    (0 : S)
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have neg : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) 0 = 0
Tactic: rw [this, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a i) : S) (0 : S)
f : MvPowerSeries σ R
hf : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : ¬d = 0
this :
  Eq.{u_5 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
    (0 : S)
neg : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) 0 = 0
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have neg₁ : Eq.{u_5 + 1} (α := S) 0 0
Tactic: rw [this, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ S)
    ((map (algebraMap R S) : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S)
    (subst X f : MvPowerSeries σ S)
have h : ∀ (e : σ →₀ ℕ),
  Eq.{u_5 + 1} (α := S)
    ((coeff e : (a : MvPowerSeries σ S) → S)
        ((map (algebraMap R S) : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S) :
      S)
    ((coeff e : (a : MvPowerSeries σ S) → S) (subst X f) : S)
Tactic: ext e
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ Eq.{u_5 + 1} (α := S)
    ((coeff e : (a : MvPowerSeries σ S) → S)
        ((map (algebraMap R S) : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S) :
      S)
    ((coeff e : (a : MvPowerSeries σ S) → S) (subst X f) : S)
have h : (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff e : (a : MvPowerSeries σ S) → S) (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
      S)
Tactic: rw [coeff_map, coeff_subst HasSubst.X f e, finsum_eq_single _ e]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
h :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S)
⊢ Eq.{u_5 + 1} (α := S)
    ((coeff e : (a : MvPowerSeries σ S) → S)
        ((map (algebraMap R S) : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S) :
      S)
    ((coeff e : (a : MvPowerSeries σ S) → S) (subst X f) : S)
have h₁ : ∀ (x : σ →₀ ℕ),
  x ≠ e →
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff e : (a : MvPowerSeries σ S) → S)
            (x.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
          S) =
      0
Tactic: rw [coeff_map, coeff_subst HasSubst.X f e, finsum_eq_single _ e]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S)
have h : (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial e : (a : S) → MvPowerSeries σ S) 1) : S)
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
h :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial e : (a : S) → MvPowerSeries σ S) 1) : S)
⊢ (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S)
have h₁ : (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) 1
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
h :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial e : (a : S) → MvPowerSeries σ S) 1) : S)
h₁ :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) 1
⊢ (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S)
have h₂ : (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S) 1
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
h :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial e : (a : S) → MvPowerSeries σ S) 1) : S)
h₁ :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) 1
h₂ :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S) 1
⊢ (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S)
have h₃ : (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S)
    (1 : S)
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e : σ →₀ ℕ
h :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial e : (a : S) → MvPowerSeries σ S) 1) : S)
h₁ :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) 1
h₂ :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S) 1
h₃ :
  (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S)
      (1 : S)
⊢ (algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (e.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S)
have h₄ : Eq.{u_5 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S)
  ((algebraMap R S : (a : R) → S) ((coeff e : (a : MvPowerSeries σ R) → R) f : R) : S)
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e d : σ →₀ ℕ
hd : d ≠ e
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S) =
    0
have h : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial d : (a : S) → MvPowerSeries σ S) 1) : S) =
  0
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e d : σ →₀ ℕ
hd : d ≠ e
h :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial d : (a : S) → MvPowerSeries σ S) 1) : S) =
    0
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S) =
    0
have h₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) 0 = 0
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
f : MvPowerSeries σ R
e d : σ →₀ ℕ
hd : d ≠ e
h :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S) ((monomial d : (a : S) → MvPowerSeries σ S) 1) : S) =
    0
h₁ : HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) 0 = 0
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff e : (a : MvPowerSeries σ S) → S)
          (d.prod fun (s : σ) (e : ℕ) ↦ HPow.hPow (α := MvPowerSeries σ S) (X s) e) :
        S) =
    0
have h₂ : Eq.{u_5 + 1} (α := S) 0 0
Tactic: rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries τ S) ((map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (subst a f) : MvPowerSeries τ S)
    (subst (R := S) (fun (i : σ) ↦ (map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (a i))
        ((map h : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f) :
      MvPowerSeries τ S)
have h₁ : ∀ (n : τ →₀ ℕ),
  Eq.{u_5 + 1} (α := S)
    ((coeff n : (a : MvPowerSeries τ S) → S)
        ((map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (subst a f) : MvPowerSeries τ S) :
      S)
    ((coeff n : (a : MvPowerSeries τ S) → S)
        (subst (R := S) (fun (i : σ) ↦ (map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (a i))
          ((map h : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f)) :
      S)
Tactic: ext n