awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
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)
have this : ∀ {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
-- 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
n : τ →₀ ℕ
this : ∀ {r : R}, Eq.{u_5 + 1} (α := S) ((h : (a : R) → S) r : S) ((h.toAddMonoidHom : (a : R) → S) r : 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)
have 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)
Tactic: rw [coeff_subst (ha.map h), coeff_map, coeff_subst ha, this, AddMonoidHom.map_finsum _
    (coeff_subst_finite ha _ _), finsum_congr]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![subst ![X i, X j] f, X k] s) : R) (0 : R)
have 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, sorry⟩)) :
    R)
  (0 : R)
Tactic: fin_cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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)
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![subst ![X i, X j] f, X k] s) : R) (0 : R)
have 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, sorry⟩)) :
    R)
  (0 : R)
Tactic: fin_cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![X i, subst ![X j, X k] f] s) : R) (0 : R)
have 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, sorry⟩)) :
    R)
  (0 : R)
Tactic: fin_cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
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)
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (![X i, subst ![X j, X k] f] s) : R) (0 : R)
have 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, sorry⟩)) :
    R)
  (0 : R)
Tactic: fin_cases s
Cleared hypotheses: s
-- 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
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)
⊢ ε.comp (substAlgHom ha) = aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯
have 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)) sorry : (a : MvPowerSeries σ R) → T) f :
      T)
Tactic: ext f
-- 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
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) ((ε.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)
have H : Eq.{u_6 + 1} (α := T)
  (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
      (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) sorry : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPowerSeries σ R) → MvPowerSeries τ S)
      f :
    T)
  ((aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) sorry : (a : MvPowerSeries σ R) → T) f : T)
Tactic: simp only [AlgHom.coe_comp, substAlgHom_eq_aeval ha]
-- 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
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)
⊢ Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯) : (a : MvPowerSeries σ R) → T)
have rw : Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
  (⇑(ε.comp (substAlgHom ha)) : (a : MvPowerSeries σ R) → T)
Tactic: rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]
-- 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
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)
rw :
  Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(ε.comp (substAlgHom ha)) : (a : MvPowerSeries σ R) → T)
⊢ Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯) : (a : MvPowerSeries σ R) → T)
have rw₁ : Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
  (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S))
Tactic: rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]
-- 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
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)
rw :
  Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(ε.comp (substAlgHom ha)) : (a : MvPowerSeries σ R) → T)
rw₁ :
  Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (Function.comp (β := MvPowerSeries τ S) (⇑ε : (a : MvPowerSeries τ S) → T)
      (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S))
⊢ Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
    (⇑(aeval (a := fun (s : σ) ↦ (ε.toRingHom : (a : MvPowerSeries τ S) → T) (a s)) ⋯) : (a : MvPowerSeries σ R) → T)
have rw₂ : Eq (α := MvPowerSeries σ R → T) ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
  ((⇑ε : (a : MvPowerSeries τ S) → T) ∘ subst a)
Tactic: rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]
-- 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
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
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : UniformSpace R
inst_14 : DiscreteUniformity R
inst_15 : UniformSpace S
inst_16 : DiscreteUniformity S
ha : HasSubst a
b : τ → T
hb : HasEval b
f : MvPowerSeries σ R
ε : MvPowerSeries τ S →ₐ[R] T := AlgHom.restrictScalars R (aeval hb)
⊢ eval₂ (algebraMap S T) b (subst a f) = eval₂ (algebraMap R T) (fun (s : σ) ↦ eval₂ (algebraMap S T) b (a s)) f
have hε : Continuous (X := MvPowerSeries τ S) (Y := T) (⇑ε : (a : MvPowerSeries τ S) → T)
Tactic: have hε : Continuous ε := continuous_aeval hb
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S) :
      S)
have rw : IsNilpotent.{u_5} (R := S)
  (∑ᶠ (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))
Tactic: rw [coe_substAlgHom, constantCoeff_subst ha]
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ IsNilpotent.{u_5} (R := S)
    (∑ᶠ (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))
have hf₁ : ∀ (b : σ →₀ ℕ),
  IsNilpotent
    (HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (b.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S))
Tactic: apply isNilpotent_finsum
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
⊢ IsNilpotent
    (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))
have pos : ∀ (hd : d = 0),
  IsNilpotent
    (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))
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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
pos :
  ∀ (hd : d = 0),
    IsNilpotent
      (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))
⊢ IsNilpotent
    (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))
have neg : ∀ (hd : ¬d = 0),
  IsNilpotent
    (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))
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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent
    (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))
have pos : IsNilpotent
  (HSMul.hSMul (α := S) (β := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S) (Finsupp.prod 0 fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
    ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S))
Tactic: rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent
    (HSMul.hSMul (α := S) (β := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S) (Finsupp.prod 0 fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
      ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S))
have pos : IsNilpotent.{u_5} (R := S) ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R) : S)
Tactic: apply IsNilpotent.smul
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ IsNilpotent
    (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))
have neg : IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
Tactic: apply IsNilpotent.smul
-- 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
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
have hd₁ : ∃ (a : σ), Ne (α := ℕ) ((d : (a : σ) → ℕ) a : ℕ) ((0 : (a : σ) → ℕ) a : ℕ)
Tactic: rw [← ne_eq, Finsupp.ne_iff] at hd
Cleared hypotheses: hd
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
hd : ∃ (a : σ), Ne (α := ℕ) ((d : (a : σ) → ℕ) a : ℕ) ((0 : (a : σ) → ℕ) a : ℕ)
⊢ IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
have neg : ∀ (t : σ) (hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)),
  IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
Tactic: obtain ⟨t, hs⟩ := hd
Cleared hypotheses: hd
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
⊢ IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (d.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S)
have neg : IsNilpotent
  (HSMul.hSMul (α := S) (β := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((Finsupp.filter (fun (a : σ) ↦ ¬a = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S))
Tactic: rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
⊢ IsNilpotent
    (HSMul.hSMul (α := S) (β := S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S)
          ((Finsupp.filter (fun (a : σ) ↦ ¬a = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
        S)
      ((constantCoeff : (a : MvPowerSeries τ S) → S)
          ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
        S))
have neg : IsNilpotent.{u_5} (R := S)
  ((constantCoeff : (a : MvPowerSeries τ S) → S)
      ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
    S)
Tactic: apply IsNilpotent.smul
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S)
have neg : IsNilpotent.{u_5} (R := S)
  ((constantCoeff : (a : MvPowerSeries τ S) → S)
      (HPow.hPow (β := ℕ) (a t) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ)) :
    S)
Tactic: rw [Finsupp.prod_eq_single t]
-- 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
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
d : σ →₀ ℕ
t : σ
hs : Ne (α := ℕ) ((d : (a : σ) → ℕ) t : ℕ) ((0 : (a : σ) → ℕ) t : ℕ)
neg :
  IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        (HPow.hPow (β := ℕ) (a t) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ)) :
      S)
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((Finsupp.filter (fun (i : σ) ↦ i = t) d).prod fun (s : σ) (e : ℕ) ↦ a s ^ e) :
      S)
have neg₁ : ∀ (b : σ),
  Ne (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) b : ℕ) (0 : ℕ) →
    b ≠ t → HPow.hPow (β := ℕ) (a b) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) b : ℕ) = 1
Tactic: rw [Finsupp.prod_eq_single t]