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
υ : 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
f : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries υ T)
    ((substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T)
        ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f) :
      MvPowerSeries υ T)
    ((substAlgHom (a := fun (s : σ) ↦ (substAlgHom hb : (a : MvPowerSeries τ S) → MvPowerSeries υ T) (a s)) ⋯ :
          (a : MvPowerSeries σ R) → MvPowerSeries υ T)
        f :
      MvPowerSeries υ T)

Tactic:
DFunLike.congr_fun (substAlgHom_comp_substAlgHom ha hb) f

Premises used: DFunLike.congr_fun, Classical.epsilon, Set.Mem, Filter.lim, Filter.limUnder, IsDenseInducing.extend, MvPowerSeries.substAlgHom_comp_substAlgHom
-- 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
υ : 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
⊢ Eq (α := MvPowerSeries σ R → MvPowerSeries υ T) (subst b ∘ subst a) (subst fun (s : σ) ↦ subst b (a s))

Tactic:
simpa [funext_iff, DFunLike.ext_iff] using substAlgHom_comp_substAlgHom (R := R) ha hb

Premises used: funext_iff, DFunLike.ext_iff, MvPowerSeries.substAlgHom_comp_substAlgHom
-- 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
υ : 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
f : MvPowerSeries σ R
⊢ subst b (subst a f) = subst (fun (s : σ) ↦ subst b (a s)) f

Tactic:
congr_fun (subst_comp_subst (R := R) ha hb) f

Premises used: MvPowerSeries.subst_comp_subst, MvPowerSeries.subst, dite, congr_fun, MvPowerSeries.eval₂
-- 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
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)
⊢ ⨅ (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)

Tactic:
apply MvPowerSeries.le_weightedOrder

Premises used: MvPowerSeries.le_weightedOrder
-- 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
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)
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
⊢ Eq.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)

Tactic:
rw [coeff_subst ha, finsum_eq_zero_of_forall_eq_zero]

Premises used: MvPowerSeries.coeff_subst, finsum_eq_zero_of_forall_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
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
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
⊢ 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

Premises used: MvPowerSeries.coeff, DFunLike.coe
-- 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
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

Tactic:
simp [hfx]
-- 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
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)
neg :
  (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞) <
    weightedOrder.{u_4, u_5} (R := S) w (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e)
⊢ 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_eq_zero_of_lt_weightedOrder w, smul_zero]

Premises used: smul_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- 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
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)

Tactic:
hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))

Premises used: MvPowerSeries.le_weightedOrder_prod, LT.lt.trans_le, LE.le.trans, biInf_le
-- 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
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)
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)) :
      ℕ∞)
⊢ (↑((Finsupp.weight w : (a : τ →₀ ℕ) → ℕ) d) : ℕ∞) <
    weightedOrder.{u_4, u_5} (R := S) w (x.prod fun (s : σ) (e : ℕ) ↦ a s ^ e)

Tactic:
refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))

Premises used: MvPowerSeries.le_weightedOrder_prod, LT.lt.trans_le, LE.le.trans, biInf_le
-- 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
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)
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 : ℕ)))
⊢ 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:
simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]

Premises used: Finsupp.sum, Function.comp_apply, Finsupp.weight_apply
-- 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
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)
i : σ
hi : i ∈ x.support
⊢ HSMul.hSMul (α := ℕ) ((x : (a : σ) → ℕ) i : ℕ) (weightedOrder w (a i)) ≤
    HSMul.hSMul (α := ℕ) ((x : (a : σ) → ℕ) i : ℕ) (weightedOrder w (a i))

Tactic:
simp
-- 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
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 (α := ℕ∞) (∑ 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:
exact Finset.sum_le_sum fun i hi ↦ .trans (by simp) (le_weightedOrder_pow ..)

Premises used: MvPowerSeries.le_weightedOrder_pow, Finset.sum_le_sum, LE.le.trans
-- 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
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
⊢ weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤ weightedOrder w (subst a f)

Tactic:
.trans ?_ (le_weightedOrder_subst w ha f)

Premises used: MvPowerSeries.le_weightedOrder_subst, LE.le.trans
-- 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
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
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
⊢ weightedOrder (ENat.toNat ∘ weightedOrder w ∘ a) f ≤ weightedOrder w (subst a f)

Tactic:
refine .trans ?_ (le_weightedOrder_subst w ha 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
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
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
⊢ 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:
simp only [ne_eq, le_iInf_iff]

Premises used: le_iInf_iff, ne_eq
-- 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
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

Tactic:
fun i hi ↦ (weightedOrder_le _ hi).trans ?_

Premises used: Function.comp, MvPowerSeries.weightedOrder, MvPowerSeries.weightedOrder_le, ENat.toNat, LE.le.trans
-- 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
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
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 : ℕ∞)
⊢ ∀ (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:
refine fun i hi ↦ (weightedOrder_le _ hi).trans ?_

Premises used: MvPowerSeries.weightedOrder_le, LE.le.trans
-- 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
w : τ → ℕ
ha : HasSubst a
ha0 : ∀ (i : σ), a i ≠ 0
f : MvPowerSeries σ R
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:
simp [Finsupp.weight_apply, Finsupp.sum, (ne_zero_iff_weightedOrder_finite _).mp (ha0 _)]

Premises used: Finsupp.sum, MvPowerSeries.ne_zero_iff_weightedOrder_finite, Iff.mp, Finsupp.weight_apply
-- 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
f : MvPowerSeries σ R
⊢ (⨅ (i : σ), (a i).order) * f.order ≤ (subst a f).order

Tactic:
.trans ?_ (MvPowerSeries.le_weightedOrder_subst _ ha _)

Premises used: MvPowerSeries.le_weightedOrder_subst, LE.le.trans
-- 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
f : MvPowerSeries σ R
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
⊢ (⨅ (i : σ), (a i).order) * f.order ≤ (subst a f).order

Tactic:
refine .trans ?_ (MvPowerSeries.le_weightedOrder_subst _ ha _)
-- 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
f : MvPowerSeries σ R
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
⊢ (⨅ (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:
simp only [ne_eq, le_iInf_iff]

Premises used: le_iInf_iff, ne_eq
-- 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
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) : ℕ∞)
trans₁ :
  HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i
⊢ (⨅ (i : σ), (a i).order) * f.order ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (a : σ →₀ ℕ) → ℕ∞) i

Tactic:
trans (⨅ (i : σ), (order ∘ a) i) * ↑i.degree

Premises used: iInf, Function.comp, Finsupp.degree, DFunLike.coe, MvPowerSeries.order
-- 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
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 ≤
    HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)

Tactic:
mul_le_mul_right (order_le hi) _

Premises used: mul_le_mul_right, MvPowerSeries.order_le, dite, MvPowerSeries.weightedOrder, MvPowerSeries.order
-- 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
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 ≤
    HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)

Tactic:
refine mul_le_mul_right (order_le hi) _

Premises used: mul_le_mul_right, MvPowerSeries.order_le
-- 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
f : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
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))
⊢ HMul.hMul (α := ℕ∞) (⨅ (i : σ), (order ∘ a) i) (↑((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) ≤
    ((Finsupp.weight ((weightedOrder fun (x : τ) ↦ 1) ∘ a) : (σ →₀ ℕ) →+ ℕ∞) : (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]

Premises used: Finset.mul_sum, AddMonoidHom.coe_mk, Finsupp.degree, ZeroHom.coe_mk, Nat.cast_sum, nsmul_eq_mul, Function.comp_apply, MvPowerSeries.order, Finsupp.weight_apply
-- 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
f : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
j : σ
hj : j ∈ i.support
⊢ HMul.hMul (α := ℕ∞) (⨅ (i : σ), weightedOrder (fun (x : τ) ↦ 1) (a i)) (↑((i : (a : σ) → ℕ) j) : ℕ∞) ≤
    (fun (i : σ) (c : ℕ) ↦ (↑c : ℕ∞) * weightedOrder (fun (x : τ) ↦ 1) (a i)) j ((i : (a : σ) → ℕ) j)

Tactic:
simp [mul_comm, mul_le_mul_right (iInf_le_iff.mpr fun _ a ↦ a j)]

Premises used: Iff.mpr, mul_le_mul_right, iInf_le_iff, mul_comm
-- 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
f : MvPowerSeries σ R
i : σ →₀ ℕ
hi : ¬Eq.{u_3 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 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:
exact Finset.sum_le_sum fun j hj => by
      simp [mul_comm, mul_le_mul_right (iInf_le_iff.mpr fun _ a ↦ a j)]

Premises used: Finset.sum_le_sum