awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
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) 1 : R) :
        R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 1 : 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) 1 : R))
    1

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
h :
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
      R)
    (if n = 0 then 1 else 0 : R)
⊢ 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) 1 : R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)

Tactic:
simp only [coeff_one, mul_ite, mul_one, mul_zero]

Premises used: mul_ite, MvPowerSeries.coeff_one, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
pos :
  ∀ (h : n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
        R)
      (1 : R)
neg :
  ∀ (h : ¬n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
        R)
      (0 : R)
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
      R)
    (if n = 0 then 1 else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
h : n = 0
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
      R)
    (1 : R)

Tactic:
simp [h, coeff_apply]

Premises used: MvPowerSeries.coeff_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
h : ¬n = 0
neg : n = 0 → Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) 0
⊢ Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
      R)
    (0 : R)

Tactic:
simp only [coeff_apply, ite_eq_right_iff]

Premises used: MvPowerSeries.coeff_apply, ite_eq_right_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
h : ¬n = 0
⊢ n = 0 → Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) 0

Tactic:
fun a_1 ↦ False.elim (h a_1)

Premises used: False.elim
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
h : ¬n = 0
⊢ n = 0 → Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) 0

Tactic:
exact fun a_1 ↦ False.elim (h a_1)

Premises used: False.elim
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : σ →₀ ℕ
h :
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
      R)
    (if n = 0 then 1 else 0 : R)
pos :
  ∀ (h : n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
        R)
      (1 : R)
neg neg₁ :
  ∀ (h : ¬n = 0),
    Eq.{u_9 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
          if n = 0 then n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m else 0 :
        R)
      (0 : R)
⊢ 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) 1 : R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)

Tactic:
classical
    simp only [coeff_one, mul_ite, mul_one, mul_zero]
    split_ifs with h
    · simp [h, coeff_apply]
    · simp only [coeff_apply, ite_eq_right_iff]
      exact fun a_1 ↦ False.elim (h a_1)

Premises used: mul_ite, MvPowerSeries.coeff_one, MvPowerSeries.coeff_apply, MulZeroClass.mul_zero, ite_eq_right_iff, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
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) (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)
⊢ (fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) (f * g) : 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:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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 : σ →₀ ℕ
h :
  Eq.{u_9 + 1} (α := R)
    (∑ i ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) *
        HMul.hMul (α := R) (β := R) ((coeff i.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff i.2 : (a : MvPowerSeries σ R) → R) g : R))
    (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R)
        ((coeff p.1 : (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 : R) :
          R)
        ((coeff p.2 : (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) g : R) :
          R))
⊢ 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)

Tactic:
rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]

Premises used: Finset.mul_sum, MvPowerSeries.coeff_apply, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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 : σ →₀ ℕ
h :
  ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
    (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) *
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (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 : R) :
          R)
        ((coeff x.2 : (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) g : R) :
          R)
⊢ Eq.{u_9 + 1} (α := R)
    (∑ i ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) *
        HMul.hMul (α := R) (β := R) ((coeff i.1 : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff i.2 : (a : MvPowerSeries σ R) → R) g : R))
    (∑ p ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R)
        ((coeff p.1 : (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 : R) :
          R)
        ((coeff p.2 : (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) g : R) :
          R))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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 ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n
⊢ x.1 + x.2 = n

Tactic:
simp only [Finset.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
h :
  ((x.1 + x.2).prod fun (s : σ) (m : ℕ) ↦ a s ^ m) *
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      ((coeff x.1 : (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 : R) :
        R)
      ((coeff x.2 : (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) g : R) :
        R)
⊢ (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) *
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      ((coeff x.1 : (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 : R) :
        R)
      ((coeff x.2 : (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) g : R) :
        R)

Tactic:
rw [← hx]
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
h :
  ((x.1 + x.2).prod fun (s : σ) (m : ℕ) ↦ a s ^ m) * (f x.1 * g x.2) =
    (x.1.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) * f x.1 * ((x.2.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) * g x.2)
⊢ ((x.1 + x.2).prod fun (s : σ) (m : ℕ) ↦ a s ^ m) *
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    HMul.hMul (α := R) (β := R)
      ((coeff x.1 : (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 : R) :
        R)
      ((coeff x.2 : (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) g : R) :
        R)

Tactic:
simp only [coeff_apply]

Premises used: MvPowerSeries.coeff_apply