awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
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)
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
⊢ 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₂ : Eq (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ) (0 : ℕ) → HPow.hPow (β := ℕ) (a t) 0 = 1
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 : ℕ)
h : Eq (α := ℕ) ((Finsupp.filter (fun (i : σ) ↦ i = t) d : (a : σ) → ℕ) t : ℕ) (0 : ℕ)
⊢ HPow.hPow (β := ℕ) (a t) 0 = 1
have rw : Eq (α := MvPowerSeries τ S) 1 1
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
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) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
Tactic: classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw : IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
⊢ 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: classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw : IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
rw₁ rw₂ 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))
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S) :
      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: classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw : IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
rw₁ rw₂ 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))
hf₁ hf₂ :
  ∀ (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))
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S) :
      S)
have pos : ∀ (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))
Tactic: classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
hf : IsNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw : IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
rw₁ rw₂ 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))
hf₁ hf₂ :
  ∀ (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))
pos :
  ∀ (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))
⊢ IsNilpotent.{u_5} (R := S)
    ((constantCoeff : (a : MvPowerSeries τ S) → S)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S) :
      S)
have neg : ∀ (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))
Tactic: classical
  rw [coe_substAlgHom, constantCoeff_subst ha]
  apply isNilpotent_finsum
  intro d
  by_cases hd : d = 0
  · rw [← algebraMap_smul S, smul_eq_mul, mul_comm, ← smul_eq_mul, hd]
    apply IsNilpotent.smul
    simpa using IsNilpotent.map hf (algebraMap R S)
  · apply IsNilpotent.smul
    rw [← ne_eq, Finsupp.ne_iff] at hd
    obtain ⟨t, hs⟩ := hd
    rw [← Finsupp.prod_filter_mul_prod_filter_not (fun i ↦ i = t), map_mul,
      mul_comm, ← smul_eq_mul]
    apply IsNilpotent.smul
    rw [Finsupp.prod_eq_single t]
    · simpa using IsNilpotent.pow_of_pos (ha.const_coeff t) hs
    · intro t' htt' ht'
      simp [ht'] at htt'
    · exact fun _ ↦ by rw [pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst_1 : CommRing T
inst_2 : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
⊢ ∀ (d : υ →₀ ℕ),
    Set.Finite.{u_1} (α := σ)
      {s : σ |
        Ne.{u_8 + 1} (α := T)
          ((coeff d : (a : MvPowerSeries υ T) → T)
              ((substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s) : MvPowerSeries υ T) :
            T)
          (0 : T)}
have rw : Filter.Tendsto (β := MvPowerSeries υ T)
  (fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) Filter.cofinite (nhds 0)
Tactic: rw [← coeff_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst_1 : CommRing T
inst_2 : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
⊢ Filter.Tendsto (β := MvPowerSeries υ T)
    (fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) Filter.cofinite (nhds 0)
have apply : Filter.Tendsto (α := MvPowerSeries τ S) (β := MvPowerSeries υ T)
  (⇑(substAlgHom hb) : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (nhds 0) (nhds 0)
Tactic: apply Filter.Tendsto.comp _ (ha.hasEval.tendsto_zero)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
υ : Type u_7
T : Type u_8
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this_1 : UniformSpace R := ⊥
this_2 : UniformSpace S := ⊥
this : UniformSpace T := ⊥
⊢ Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries υ T)
    (AlgHom.comp (AlgHom.restrictScalars R (substAlgHom hb)) (substAlgHom ha))
    (substAlgHom (a := fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) ⋯)
have apply : Continuous (X := MvPowerSeries τ S) (Y := MvPowerSeries υ T)
  (⇑(AlgHom.restrictScalars R (substAlgHom hb)) : (a : MvPowerSeries τ S) → MvPowerSeries υ T)
Tactic: apply comp_aeval (R := R) (ε := (substAlgHom hb).restrictScalars R) ha.hasEval
-- 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d ≤
    weightedOrder w (subst a f)
have h : ∀ (d : τ →₀ ℕ),
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
      (⨅ (d : σ →₀ ℕ),
        ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
          ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d) →
    Eq.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)
Tactic: apply MvPowerSeries.le_weightedOrder
-- 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd :
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
    (⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)
⊢ Eq.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)
have h : ∀ (x : σ →₀ ℕ),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: rw [coeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd :
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
    (⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)
x : σ →₀ ℕ
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have pos : ∀ (hfx : Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: by_cases hfx : f.coeff x = 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd :
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
    (⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)
x : σ →₀ ℕ
pos :
  ∀ (hfx : Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
      0
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have neg : ∀ (hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: by_cases hfx : f.coeff x = 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd :
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
    (⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)
x : σ →₀ ℕ
hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
have neg : (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞) <
  weightedOrder.{u_4, u_5} (R := S) w (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e)
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd :
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
    (⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)
x : σ →₀ ℕ
hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞) <
    weightedOrder.{u_4, u_5} (R := S) w (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e)
have neg : LE.le (α := ℕ∞) (((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) x : ℕ∞)
  (∑ i ∈ x.support, weightedOrder.{u_4, u_5} (R := S) w ((fun (s : σ) (e : ℕ) ↦ a s ^ e) i ((x : (a : σ) → ℕ) i)) : ℕ∞)
Tactic: refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))
-- 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd :
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
    (⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)
x : σ →₀ ℕ
hfx : ¬Eq.{u_3 + 1} (α := R) ((coeff x : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ LE.le (α := ℕ∞) (((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) x : ℕ∞)
    (∑ i ∈ x.support, weightedOrder.{u_4, u_5} (R := S) w ((fun (s : σ) (e : ℕ) ↦ a s ^ e) i ((x : (a : σ) → ℕ) i)) :
      ℕ∞)
have neg : LE.le (α := ℕ∞) (∑ x_1 ∈ x.support, HSMul.hSMul (α := ℕ) ((x : (a : σ) → ℕ) x_1 : ℕ) (weightedOrder w (a x_1)))
  (∑ x_1 ∈ x.support, weightedOrder w (HPow.hPow (β := ℕ) (a x_1) ((x : (a : σ) → ℕ) x_1 : ℕ)))
Tactic: simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]
-- 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d ≤
    weightedOrder w (subst a f)
have h : ∀ (d : τ →₀ ℕ),
  LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
      (⨅ (d : σ →₀ ℕ),
        ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
          ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d) →
    Eq.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)
Tactic: classical
  apply MvPowerSeries.le_weightedOrder
  intro d hd
  rw [coeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
  intro x
  by_cases hfx : f.coeff x = 0
  · simp [hfx]
  rw [coeff_eq_zero_of_lt_weightedOrder w, smul_zero]
  refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))
  simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]
  exact Finset.sum_le_sum fun i hi ↦ .trans (by simp) (le_weightedOrder_pow ..)
-- 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
h h₁ :
  ∀ (d : τ →₀ ℕ)
    (hd :
      LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
        (⨅ (d : σ →₀ ℕ),
          ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
            ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d)),
    Eq.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)
⊢ ⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d ≤
    weightedOrder w (subst a f)
have h₂ : ∀ (d : τ →₀ ℕ)
  (hd :
    LT.lt (α := ℕ∞) (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞)
      (⨅ (d : σ →₀ ℕ),
        ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
          ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d))
  (x : σ →₀ ℕ),
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := S) ((coeff x : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries τ S) → S) (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e) : S) =
    0
Tactic: classical
  apply MvPowerSeries.le_weightedOrder
  intro d hd
  rw [coeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
  intro x
  by_cases hfx : f.coeff x = 0
  · simp [hfx]
  rw [coeff_eq_zero_of_lt_weightedOrder w, smul_zero]
  refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))
  simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]
  exact Finset.sum_le_sum fun i hi ↦ .trans (by simp) (le_weightedOrder_pow ..)