awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
⊢ f.order * MvPowerSeries.weightedOrder w a ≤
    ⨅ (d : Unit →₀ ℕ),
      ⨅ (_ : Ne (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)),
        (Finsupp.weight (MvPowerSeries.weightedOrder w ∘ Function.const Unit a) : (a : Unit →₀ ℕ) → ℕ∞) d
have simp : ∀ (i : Unit →₀ ℕ) (i_1 : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)),
  f.order * MvPowerSeries.weightedOrder w a ≤
    (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i
Tactic: simp only [ne_eq, Function.comp_const, le_iInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ f.order * MvPowerSeries.weightedOrder w a ≤
    (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i
have trans : f.order * MvPowerSeries.weightedOrder w a ≤ (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a
Tactic: trans i () * MvPowerSeries.weightedOrder w a
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
trans : f.order * MvPowerSeries.weightedOrder w a ≤ (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a
⊢ f.order * MvPowerSeries.weightedOrder w a ≤
    (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i
have trans₁ : (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a ≤
  (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i
Tactic: trans i () * MvPowerSeries.weightedOrder w a
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ Ne (α := R) ((coeff ((i : (a : Unit) → ℕ) ()) : (a : R⟦X⟧) → R) f : R) (0 : R)
have delta : Ne (α := R) ((MvPowerSeries.coeff (Finsupp.single () ((i : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) f : R) (0 : R)
Tactic: delta PowerSeries.coeff
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ Ne (α := R) ((MvPowerSeries.coeff (Finsupp.single () ((i : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) f : R) (0 : R)
have h : Finsupp.single () ((i : (a : Unit) → ℕ) ()) = i
Tactic: convert! hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
⊢ a.order * f.order ≤ (subst a f).order
have refine : a.order * f.order ≤ (⨅ (i : Unit), (Function.const Unit a i).order) * MvPowerSeries.order f
Tactic: refine .trans ?_ (MvPowerSeries.le_order_subst (PowerSeries.hasSubst_iff.mp ha) _)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
| order (subst f φ)
have rw : (subst f φ).order
Tactic: rw [order_eq_order]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ φ.order ≤ order (subst f φ)
have conv_rhs : φ.order ≤ (subst f φ).order
Tactic: conv_rhs => rw [order_eq_order]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
hφ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ f.order ≤ order (subst f φ)
have simp_rw : MvPowerSeries.order f ≤ (subst f φ).order
Tactic: simp_rw [order_eq_order]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
⊢ Eq (α := R⟦X⟧) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
    ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
      MvPowerSeries Unit R)
have h : ∀ (n : ℕ),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
have h : HMul.hMul (β := R) (r ^ n) ((MvPowerSeries.coeff (Finsupp.single () n) : (a : R⟦X⟧) → R) f : R) =
  HMul.hMul (α := R) (β := R) (Finsupp.prod (Finsupp.single () n) fun (s : Unit) (m : ℕ) ↦ r ^ m : R)
    ((MvPowerSeries.coeff (Finsupp.single () n) : (a : MvPowerSeries Unit R) → R) f : R)
Tactic: rw [coeff_rescale, coeff, MvPowerSeries.coeff_rescale]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
⊢ (rescale r : (a : R⟦X⟧) → R⟦X⟧) f = subst (HSMul.hSMul (β := R⟦X⟧) r X) f
have rw : (MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f =
  subst (HSMul.hSMul (β := R⟦X⟧) r X) f
Tactic: rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
rw :
  (MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
⊢ (rescale r : (a : R⟦X⟧) → R⟦X⟧) f = subst (HSMul.hSMul (β := R⟦X⟧) r X) f
have rw₁ : MvPowerSeries.subst
    (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
  subst (HSMul.hSMul (β := R⟦X⟧) r X) f
Tactic: rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
rw :
  (MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₁ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
⊢ (rescale r : (a : R⟦X⟧) → R⟦X⟧) f = subst (HSMul.hSMul (β := R⟦X⟧) r X) f
have rw₂ : MvPowerSeries.subst
    (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
  subst (HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
Tactic: rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
rw :
  (MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₁ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₂ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
⊢ (rescale r : (a : R⟦X⟧) → R⟦X⟧) f = subst (HSMul.hSMul (β := R⟦X⟧) r X) f
have rw₃ : MvPowerSeries.subst
    (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
  MvPowerSeries.subst (fun (x : Unit) ↦ HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
Tactic: rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
rw :
  (MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₁ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₂ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
rw₃ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    MvPowerSeries.subst (fun (x : Unit) ↦ HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
⊢ (rescale r : (a : R⟦X⟧) → R⟦X⟧) f = subst (HSMul.hSMul (β := R⟦X⟧) r X) f
have rw₄ : Eq (α := R⟦X⟧) (MvPowerSeries.subst (fun (i : Unit) ↦ HSMul.hSMul (β := MvPowerSeries Unit R) r (MvPowerSeries.X i)) f)
  (MvPowerSeries.subst (fun (x : Unit) ↦ HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f)
Tactic: rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
⊢ Eq (α := R⟦X⟧ →+* R⟦X⟧) (↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) (rescale r)
have a : ∀ (f : R⟦X⟧) (n : ℕ),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
Tactic: ext f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
have a : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
  ((coeff n : (a : R⟦X⟧) → R)
      ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
        MvPowerSeries Unit R) :
    R)
Tactic: rw [rescale_eq, RingHom.coe_coe, MvPowerSeries.rescaleAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
a :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
have a₁ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescaleAlgHom r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
  ((coeff n : (a : R⟦X⟧) → R)
      ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
        MvPowerSeries Unit R) :
    R)
Tactic: rw [rescale_eq, RingHom.coe_coe, MvPowerSeries.rescaleAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
a :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
a₁ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescaleAlgHom r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
have a₂ : Eq (α := R)
  ((coeff n : (a : R⟦X⟧) → R)
      ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
        MvPowerSeries Unit R) :
    R)
  ((coeff n : (a : R⟦X⟧) → R)
      ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
        MvPowerSeries Unit R) :
    R)
Tactic: rw [rescale_eq, RingHom.coe_coe, MvPowerSeries.rescaleAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
⊢ HasSubst p
have ha : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
Tactic: apply HasSubst.of_constantCoeff_zero
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
have ha : p 0 = 0
Tactic: rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
⊢ p 0 = 0
have this : p 0 ≠ 0 → Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ) (1 : ℕ)
Tactic: have : (p 0 ≠ 0) → (0 : σ →₀ ℕ).degree = 1 := hp_lin 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
⊢ subst (R := R) p ((rescale a : (a : R⟦X⟧) → R⟦X⟧) f) =
    (MvPowerSeries.rescale (Function.const σ a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (subst p f)
have hp : HasSubst p
Tactic: have hp : PowerSeries.HasSubst p := by
    apply HasSubst.of_constantCoeff_zero
    rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply]
    have : (p 0 ≠ 0) → (0 : σ →₀ ℕ).degree = 1 := hp_lin 0
    grind
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
⊢ subst (R := R) p ((rescale a : (a : R⟦X⟧) → R⟦X⟧) f) =
    (MvPowerSeries.rescale (Function.const σ a) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (subst p f)
have rw : subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f =
  MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) (subst p f)
Tactic: rw [rescale_eq_subst, MvPowerSeries.rescale_eq_subst,
    subst_comp_subst_apply (HasSubst.smul_X' a) hp]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
⊢ subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f =
    MvPowerSeries.subst (R := R) (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X)
      (MvPowerSeries.subst (fun (x : Unit) ↦ p) f)
have rw : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
Tactic: rw [MvPowerSeries.subst_comp_subst_apply hp.const (MvPowerSeries.HasSubst.smul_X _),
    MvPowerSeries.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
have rw : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (MvPowerSeries.subst
        (fun (s : Unit) ↦
          MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
        f) :
    R)
Tactic: rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
have rw₁ : Eq.{u_2 + 1} (α := R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p (↑Polynomial.X : R⟦X⟧)) f) : R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (MvPowerSeries.subst
        (fun (s : Unit) ↦
          MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
        f) :
    R)
Tactic: rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
hp : HasSubst p
n : σ →₀ ℕ
rw :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p X) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
rw₁ :
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (a • subst (R := R) p (↑Polynomial.X : R⟦X⟧)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (subst (subst p (HSMul.hSMul (β := R⟦X⟧) a X)) f) : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        (MvPowerSeries.subst
          (fun (s : Unit) ↦
            MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
          f) :
      R)
have rw₂ : Eq.{u_2 + 1} (α := R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (subst
        (HSMul.hSMul (β := MvPowerSeries σ R) a
          ((Polynomial.aeval p : (a : Polynomial R) → MvPowerSeries σ R) Polynomial.X : MvPowerSeries σ R))
        f) :
    R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      (MvPowerSeries.subst
        (fun (s : Unit) ↦
          MvPowerSeries.subst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) (Function.const σ a) MvPowerSeries.X) p)
        f) :
    R)
Tactic: rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]