awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
hc : ∀ (i : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ False

Tactic:
hd <| Finsupp.ext hc

Premises used: Finsupp.ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
hc : ∀ (i : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ False

Tactic:
exact hd <| Finsupp.ext hc

Premises used: Finsupp.ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
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)
⊢ 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
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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 : σ
hi : Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ i ∈ d.support

Tactic:
simp [hi]
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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 : σ
hi : Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq.{u_5 + 1} (α := S) ((fun (a : σ) (b : ℕ) ↦ HPow.hPow (α := S) 0 b) i ((d : (a : σ) → ℕ) i)) 0

Tactic:
simp [zero_pow hi]

Premises used: zero_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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 : σ
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:
simpa [map_finsuppProd, ha'] using
        Finset.prod_eq_zero (i := i) (by simp [hi]) (by simp [zero_pow hi])

Premises used: map_finsuppProd, Finset.prod_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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)

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])
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
neg₁ neg₂ : Eq.{u_5 + 1} (α := S) 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

Tactic:
rw [this, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
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)
⊢ Eq (α := MvPowerSeries σ S)
    ((map (algebraMap R S) : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S)
    (subst X f : MvPowerSeries σ S)

Tactic:
ext e
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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)
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
⊢ 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:
rw [coeff_map, coeff_subst HasSubst.X f e, finsum_eq_single _ e]

Premises used: MvPowerSeries.coeff_subst, MvPowerSeries.coeff_map, MvPowerSeries.HasSubst.X, finsum_eq_single
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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)
h₄ 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)
⊢ (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 [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
      algebra_compatible_smul S, smul_eq_mul, mul_one]

Premises used: algebra_compatible_smul, MvPowerSeries.coeff_monomial_same, MvPowerSeries.monomial_one_eq, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
h₂ h₃ : Eq.{u_5 + 1} (α := S) 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

Tactic:
rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]

Premises used: smul_zero, Ne.symm, MvPowerSeries.monomial_one_eq, MvPowerSeries.coeff_monomial_ne
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
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)
⊢ 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)

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : τ →₀ ℕ
⊢ ∀ {r : R}, Eq.{u_5 + 1} (α := S) ((h : (a : R) → S) r : S) ((h.toAddMonoidHom : (a : R) → S) r : S)

Tactic:
have {r : R} : h r = h.toAddMonoidHom r := rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : τ →₀ ℕ
this : ∀ {r : R}, Eq.{u_5 + 1} (α := S) ((h : (a : R) → S) r : S) ((h.toAddMonoidHom : (a : R) → S) r : S)
h₁ :
  ∀ (x : σ →₀ ℕ),
    (h.toAddMonoidHom : (a : R) → S)
        (HSMul.hSMul (α := R) (β := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
          ((coeff n : (a : MvPowerSeries τ R) → R) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : R)) =
      HSMul.hSMul (α := S) (β := S)
        ((coeff x : (a : MvPowerSeries σ S) → S)
            ((map h : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S) :
          S)
        ((coeff n : (a : MvPowerSeries τ S) → S)
            (x.prod fun (s : σ) (e : ℕ) ↦
              HPow.hPow (α := MvPowerSeries τ S)
                ((map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (a s) : MvPowerSeries τ S) e) :
          S)
⊢ 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:
rw [coeff_subst (ha.map h), coeff_map, coeff_subst ha, this, AddMonoidHom.map_finsum _
    (coeff_subst_finite ha _ _), finsum_congr]

Premises used: MvPowerSeries.HasSubst.map, AddMonoidHom.map_finsum, MvPowerSeries.coeff_subst, MvPowerSeries.coeff_map, finsum_congr, MvPowerSeries.coeff_subst_finite
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
n : τ →₀ ℕ
this : ∀ {r : R}, Eq.{u_5 + 1} (α := S) ((h : (a : R) → S) r : S) ((h.toAddMonoidHom : (a : R) → S) r : S)
d : σ →₀ ℕ
⊢ (h.toAddMonoidHom : (a : R) → S)
      (HSMul.hSMul (α := R) (β := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff n : (a : MvPowerSeries τ R) → R) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : R)) =
    HSMul.hSMul (α := S) (β := S)
      ((coeff d : (a : MvPowerSeries σ S) → S)
          ((map h : (a : MvPowerSeries σ R) → MvPowerSeries σ S) f : MvPowerSeries σ S) :
        S)
      ((coeff n : (a : MvPowerSeries τ S) → S)
          (d.prod fun (s : σ) (e : ℕ) ↦
            HPow.hPow (α := MvPowerSeries τ S)
              ((map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (a s) : MvPowerSeries τ S) e) :
        S)

Tactic:
simp [smul_eq_mul, RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe, map_mul,
    ← coeff_map, Finsupp.prod]

Premises used: RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe, map_mul, MvPowerSeries.coeff_map, smul_eq_mul, Finsupp.prod
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) f : R) (0 : R)
s : Fin (Nat.succ 0).succ
0 :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![subst ![X i, X j] f, X k] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) :
      R)
    (0 : R)
1 :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![subst ![X i, X j] f, X k] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) :
      R)
    (0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![subst ![X i, X j] f, X k] s) : R) (0 : R)

Tactic:
fin_cases s
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) f : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![subst ![X i, X j] f, X k] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) :
      R)
    (0 : R)

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

Premises used: MvPowerSeries.HasSubst.X_X, MvPowerSeries.constantCoeff_subst_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) f : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![subst ![X i, X j] f, X k] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) :
      R)
    (0 : R)

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

Premises used: MvPowerSeries.HasSubst.X_X, MvPowerSeries.constantCoeff_subst_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) f : R) (0 : R)
s : Fin (Nat.succ 0).succ
0 :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![X i, subst ![X j, X k] f] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) :
      R)
    (0 : R)
1 :
  Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![X i, subst ![X j, X k] f] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) :
      R)
    (0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![X i, subst ![X j, X k] f] s) : R) (0 : R)

Tactic:
fin_cases s
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) f : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![X i, subst ![X j, X k] f] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)) :
      R)
    (0 : R)

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

Premises used: MvPowerSeries.HasSubst.X_X, MvPowerSeries.constantCoeff_subst_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : Eq (α := R) ((constantCoeff : (a : MvPowerSeries (Fin 2) R) → R) f : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R)
        (![X i, subst ![X j, X k] f] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)) :
      R)
    (0 : R)

Tactic:
simp_all [constantCoeff_subst_eq_zero .X_X]

Premises used: MvPowerSeries.HasSubst.X_X, MvPowerSeries.constantCoeff_subst_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst_11 : UniformSpace R
inst_12 : DiscreteUniformity R
inst_13 : UniformSpace S
inst_14 : DiscreteUniformity S
ha : HasSubst a
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
H :
  ∀ (f : MvPowerSeries σ R),
    Eq.{u_6 + 1} (α := T) ((ε.comp (substAlgHom ha) : (a : MvPowerSeries σ R) → T) f : T)
      ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯ : (a : MvPowerSeries σ R) → T)
          f :
        T)
⊢ ε.comp (substAlgHom ha) = aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯

Tactic:
ext f
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst_11 : UniformSpace R
inst_12 : DiscreteUniformity R
inst_13 : UniformSpace S
inst_14 : DiscreteUniformity S
ha : HasSubst a
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
f : MvPowerSeries σ R
H :
  Eq.{u_6 + 1} (α := T)
    (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
        (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
          (a : MvPowerSeries σ R) → MvPowerSeries τ S)
        f :
      T)
    ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯ : (a : MvPowerSeries σ R) → T) f :
      T)
⊢ Eq.{u_6 + 1} (α := T) ((ε.comp (substAlgHom ha) : (a : MvPowerSeries σ R) → T) f : T)
    ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯ : (a : MvPowerSeries σ R) → T) f :
      T)

Tactic:
simp only [AlgHom.coe_comp, substAlgHom_eq_aeval ha]

Premises used: MvPowerSeries.substAlgHom_eq_aeval, AlgHom.coe_comp
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst_11 : UniformSpace R
inst_12 : DiscreteUniformity R
inst_13 : UniformSpace S
inst_14 : DiscreteUniformity S
ha : HasSubst a
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
f : MvPowerSeries σ R
⊢ Eq.{u_6 + 1} (α := T)
    (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
        (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
          (a : MvPowerSeries σ R) → MvPowerSeries τ S)
        f :
      T)
    ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯ : (a : MvPowerSeries σ R) → T) f :
      T)

Tactic:
DFunLike.congr_fun (comp_aeval ha.hasEval hε) f

Premises used: DFunLike.congr_fun, Classical.epsilon, Set.Mem, MvPowerSeries.comp_aeval, Filter.lim, MvPowerSeries.HasSubst.hasEval, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.RingTheory.MvPowerSeries.Substitution
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
T : Type u_6
inst_3 : CommRing T
inst_4 : UniformSpace T
inst_5 : T2Space T
inst_6 : CompleteSpace T
inst_7 : IsUniformAddGroup T
inst_8 : IsTopologicalRing T
inst_9 : IsLinearTopology T T
inst_10 : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst_11 : UniformSpace R
inst_12 : DiscreteUniformity R
inst_13 : UniformSpace S
inst_14 : DiscreteUniformity S
ha : HasSubst a
hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
f : MvPowerSeries σ R
⊢ Eq.{u_6 + 1} (α := T)
    (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
        (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
          (a : MvPowerSeries σ R) → MvPowerSeries τ S)
        f :
      T)
    ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯ : (a : MvPowerSeries σ R) → T) f :
      T)

Tactic:
exact DFunLike.congr_fun (comp_aeval ha.hasEval hε) f

Premises used: DFunLike.congr_fun, MvPowerSeries.comp_aeval, MvPowerSeries.HasSubst.hasEval