awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 + x.2 : (a : σ) → ℕ) x_1 : ℕ)) * f x.1 =
    HMul.hMul (α := R) (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 : (a : σ) → ℕ) x_1 : ℕ))
        (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.2 : (a : σ) → ℕ) x_1 : ℕ)) *
      f x.1
have h : ∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 + x.2 : (a : σ) → ℕ) x_1 : ℕ) =
  HMul.hMul (α := R) (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 : (a : σ) → ℕ) x_1 : ℕ))
    (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.2 : (a : σ) → ℕ) x_1 : ℕ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 + x.2 : (a : σ) → ℕ) x_1 : ℕ) =
    HMul.hMul (α := R) (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 : (a : σ) → ℕ) x_1 : ℕ))
      (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.2 : (a : σ) → ℕ) x_1 : ℕ))
have h : Eq.{u_9 + 1} (α := R)
  (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 + x.2 : (a : σ) → ℕ) x_1 : ℕ))
  (∏ x_1 ∈ x.1.support ∪ x.2.support,
    HPow.hPow (β := ℕ) (a x_1) ((x.1 : (a : σ) → ℕ) x_1 : ℕ) * HPow.hPow (β := ℕ) (a x_1) ((x.2 : (a : σ) → ℕ) x_1 : ℕ))
Tactic: rw [← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ Eq.{u_9 + 1} (α := R)
    (∏ x_1 ∈ x.1.support ∪ x.2.support, HPow.hPow (β := ℕ) (a x_1) ((x.1 + x.2 : (a : σ) → ℕ) x_1 : ℕ))
    (∏ x_1 ∈ x.1.support ∪ x.2.support,
      HPow.hPow (β := ℕ) (a x_1) ((x.1 : (a : σ) → ℕ) x_1 : ℕ) *
        HPow.hPow (β := ℕ) (a x_1) ((x.2 : (a : σ) → ℕ) x_1 : ℕ))
have h : ∀ x_1 ∈ x.1.support ∪ x.2.support,
  HPow.hPow (β := ℕ) (a x_1) ((x.1 + x.2 : (a : σ) → ℕ) x_1 : ℕ) =
    HPow.hPow (β := ℕ) (a x_1) ((x.1 : (a : σ) → ℕ) x_1 : ℕ) * HPow.hPow (β := ℕ) (a x_1) ((x.2 : (a : σ) → ℕ) x_1 : ℕ)
Tactic: apply Finset.prod_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) (f * g) : R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R)
          (fun (n : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
              ((coeff n : (a : MvPowerSeries σ R) → R) f : R))
          fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) g : R)) :
      R)
have h : HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) (f * g) : R) =
  (coeff n : (a : MvPowerSeries σ R) → R)
    (HMul.hMul (α := MvPowerSeries σ R)
      (fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) f : R))
      fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) g : R))
Tactic: classical
    rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro x hx
    simp only [Finset.mem_antidiagonal] at hx
    rw [← hx]
    simp only [coeff_apply]
    rw [Finsupp.prod_of_support_subset _ Finsupp.support_add,
      Finsupp.prod_of_support_subset x.1 Finset.subset_union_left,
      Finsupp.prod_of_support_subset x.2 Finset.subset_union_right]
    · simp only [← mul_assoc]
      congr 1
      rw [mul_assoc, mul_comm (f x.1), ← mul_assoc]
      congr 1
      rw [← Finset.prod_mul_distrib]
      apply Finset.prod_congr rfl
      simp [pow_add]
    all_goals {simp}
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
⊢ Eq (α := MvPowerSeries σ R)
    (fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R))
    0
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
x y : MvPowerSeries σ R
⊢ (fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) (x + y) : R)) =
    HAdd.hAdd (α := MvPowerSeries σ R)
      (fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R))
      fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) y : R)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) (x + y) : R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (HAdd.hAdd (α := MvPowerSeries σ R)
          (fun (n : σ →₀ ℕ) ↦
            HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
              ((coeff n : (a : MvPowerSeries σ R) → R) x : R))
          fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) y : R)) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 0) (RingHom.comp C constantCoeff)
have a : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
Tactic: ext x n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
have a : Eq.{u_9 + 1} (α := R)
  ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
    R)
  (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
Tactic: simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
have pos : ∀ (h : n = 0),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
pos :
  ∀ (h : n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
have neg : ∀ (h : ¬n = 0),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (0 : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (0 : R)
have neg : (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) * x n = 0
Tactic: simp only [coeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) * x n = 0
have h₁ : Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0
Tactic: convert! zero_mul _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (hypothesis)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ¬n = 0
⊢ Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0
have h₁ : ∃ (x : σ), ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
h : ∃ (x : σ), ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
⊢ Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0
have h₁ : ∀ (s : σ) (h : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) s : ℕ) (0 : ℕ)),
  Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m) 0
Tactic: obtain ⟨s, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
x : MvPowerSeries σ R
n : σ →₀ ℕ
s : σ
h : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ Eq.{u_9 + 1} (α := R) (∏ x ∈ n.support, HPow.hPow (α := R) (β := ℕ) 0 ((n : (a : σ) → ℕ) x : ℕ)) 0
have apply : s ∈ n.support
Tactic: apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 0) (RingHom.comp C constantCoeff)
have a : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
      R)
Tactic: classical
  ext x n
  simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]
  split_ifs with h
  · simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]
  · simp only [coeff_apply]
    convert! zero_mul _
    simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
    obtain ⟨s, h⟩ := h
    simp only [Finsupp.prod]
    apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
    simpa using h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 0) (RingHom.comp C constantCoeff)
have a₁ : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
Tactic: classical
  ext x n
  simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]
  split_ifs with h
  · simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]
  · simp only [coeff_apply]
    convert! zero_mul _
    simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
    obtain ⟨s, h⟩ := h
    simp only [Finsupp.prod]
    apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
    simpa using h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
a₁ :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 0) (RingHom.comp C constantCoeff)
have pos : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ) (h : n = 0),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)
Tactic: classical
  ext x n
  simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]
  split_ifs with h
  · simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]
  · simp only [coeff_apply]
    convert! zero_mul _
    simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
    obtain ⟨s, h⟩ := h
    simp only [Finsupp.prod]
    apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
    simpa using h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
a :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((rescale 0 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          ((RingHom.comp C constantCoeff : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R) :
        R)
a₁ :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      (if n = 0 then (constantCoeff : (a : MvPowerSeries σ R) → R) x else 0 : R)
pos :
  ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ) (h : n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
            ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
        R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) x : R)
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 0) (RingHom.comp C constantCoeff)
have neg : ∀ (x : MvPowerSeries σ R) (n : σ →₀ ℕ) (h : ¬n = 0),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ HPow.hPow (α := R) 0 m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    (0 : R)
Tactic: classical
  ext x n
  simp only [rescale, Pi.zero_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    RingHom.coe_comp, Function.comp_apply, coeff_C]
  split_ifs with h
  · simp [h, coeff_apply, ← @coeff_zero_eq_constantCoeff_apply, coeff_apply]
  · simp only [coeff_apply]
    convert! zero_mul _
    simp only [DFunLike.ext_iff, not_forall, Finsupp.coe_zero, Pi.zero_apply] at h
    obtain ⟨s, h⟩ := h
    simp only [Finsupp.prod]
    apply Finset.prod_eq_zero (i := s) _ (zero_pow h)
    simpa using h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_9
inst : CommSemiring R
⊢ Eq (α := MvPowerSeries σ R →+* MvPowerSeries σ R) (rescale 1) (RingHom.id (MvPowerSeries σ R))
have a : ∀ (f : MvPowerSeries σ R) (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((rescale 1 : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        ((RingHom.id (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R) :
      R)
Tactic: ext f n