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
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)
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))
    (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
⊢ ⨅ (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 pos : ∀ (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
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)
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))
    (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
pos :
  ∀ (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
⊢ ⨅ (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 neg : ∀ (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
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
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤ weightedOrder w (subst a f)
have refine : weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤
  ⨅ (d : σ →₀ ℕ),
    ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
      ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d
Tactic: refine .trans ?_ (le_weightedOrder_subst w ha 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
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤
    ⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d
have simp : ∀ (i : σ →₀ ℕ) (i_1 : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤
    ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
Tactic: simp only [ne_eq, le_iInf_iff]
-- 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
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ ∀ (i : σ →₀ ℕ) (i_1 : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤
      ((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
have refine : ∀ (i : σ →₀ ℕ) (hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  LE.le (α := ℕ∞) ((↑((Finsupp.weight (ENat.toNat ∘ weightedOrder w ∘ a) : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) : ℕ∞)
    (((Finsupp.weight (weightedOrder w ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i : ℕ∞)
Tactic: refine fun i hi ↦ (weightedOrder_le _ hi).trans ?_
-- 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
⊢ (⨅ (i : σ), (a i).order) * f.order ≤ (subst a f).order
have refine : (⨅ (i : σ), (a i).order) * f.order ≤
  ⨅ (d : σ →₀ ℕ),
    ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
      ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d
Tactic: refine .trans ?_ (MvPowerSeries.le_weightedOrder_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
⊢ (⨅ (i : σ), (a i).order) * f.order ≤
    ⨅ (d : σ →₀ ℕ),
      ⨅ (_ : Ne.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
        ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) d
have simp : ∀ (i : σ →₀ ℕ) (i_1 : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
  (⨅ (i : σ), (a i).order) * f.order ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
Tactic: simp only [ne_eq, le_iInf_iff]
-- 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
i : σ →₀ ℕ
hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (⨅ (i : σ), (a i).order) * f.order ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
have trans : (⨅ (i : σ), (a i).order) * f.order ≤
  HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
Tactic: trans (⨅ (i : σ), (order ∘ a) i) * ↑i.degree
-- 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
i : σ →₀ ℕ
hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
trans :
  (⨅ (i : σ), (a i).order) * f.order ≤
    HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
⊢ (⨅ (i : σ), (a i).order) * f.order ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
have trans₁ : HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) ≤
  ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
Tactic: trans (⨅ (i : σ), (order ∘ a) i) * ↑i.degree
-- 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
i : σ →₀ ℕ
hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
have simp : LE.le (α := ℕ∞)
  (∑ i_1 ∈ i.support,
    HMul.hMul (α := ℕ∞) (⨅ (i : σ), weightedOrder (fun (x : τ) ↦ 1) (a i)) (↑((i : (a : σ) → ℕ) i_1) : ℕ∞))
  (i.sum fun (i : σ) (c : ℕ) ↦ (↑c : ℕ∞) * weightedOrder (fun (x : τ) ↦ 1) (a i))
Tactic: simp only [Function.comp_apply, order, Finsupp.degree, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
      Nat.cast_sum, Finset.mul_sum, Finsupp.weight_apply, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
⊢ Eq (α := MvPowerSeries σ R)
    (fun (n : σ →₀ ℕ) ↦
      HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R))
    1
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_9 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) fun (n : σ →₀ ℕ) ↦
        HMul.hMul (α := R) (β := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m : R)
          ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R) :
      R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
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)
have 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)
Tactic: simp only [coeff_one, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
n : σ →₀ ℕ
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
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)
    (0 : R)
have neg : n = 0 → Eq.{u_9 + 1} (α := R) (n.prod fun (s : σ) (m : ℕ) ↦ a s ^ m) 0
Tactic: simp only [coeff_apply, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
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)
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
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)
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
A : Type u_2
inst : CommSemiring A
R_1 : Type u_3
inst_1 : CommRing R_1
inst_2 : Algebra A R_1
τ : Type u_4
S : Type u_5
inst_3 : CommRing S
inst_4 : Algebra A S
inst_5 : Algebra R_1 S
inst_6 : IsScalarTower A R_1 S
a_1 a_2 : σ → MvPowerSeries τ S
T_1 : Type u_6
inst_7 : CommRing T_1
inst_8 : UniformSpace T_1
inst_9 : T2Space T_1
inst_10 : CompleteSpace T_1
inst_11 : IsUniformAddGroup T_1
inst_12 : IsTopologicalRing T_1
inst_13 : IsLinearTopology T_1 T_1
inst_14 : Algebra R_1 T_1
ε : MvPowerSeries τ S →ₐ[R_1] T_1
inst_15 : Algebra S T_1
inst_16 : IsScalarTower R_1 S T_1
υ : Type u_7
T : Type u_8
inst_17 : CommRing T
inst_18 : Algebra R_1 T
inst_19 : Algebra S T
inst_20 : IsScalarTower R_1 S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst_21 : CommSemiring R
a : σ → R
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)
⊢ 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)
have 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)
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)