awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : Eq (α := ℚ) (↑n ! : ℚ) 0
h₁ : n ! = 0
⊢ False

Tactic:
apply factorial_ne_zero n

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : Eq (α := ℚ) (↑n ! : ℚ) 0
h₁ h₂ : Eq (α := ℕ) 0 0
⊢ n ! = 0

Tactic:
rw [cast_eq_zero.1 h]

Premises used: Nat.cast_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((rescale 1 : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)
      ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) =
    (rescale (HAdd.hAdd (α := A) 1 (-1)) : (a : A⟦X⟧) → A⟦X⟧) (exp A)

Tactic:
exp_mul_exp_eq_exp_add (1 : A) (-1)

Premises used: PowerSeries.exp_mul_exp_eq_exp_add, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
h : exp A = (rescale 1 : (a : A⟦X⟧) → A⟦X⟧) (exp A)
h₁ : Eq (α := A⟦X⟧) (1 : A⟦X⟧) ((rescale (HAdd.hAdd (α := A) 1 (-1)) : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)
⊢ HMul.hMul (β := A⟦X⟧) (exp A) ((evalNegHom : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧) = 1

Tactic:
convert! exp_mul_exp_eq_exp_add (1 : A) (-1)

Premises used: PowerSeries.exp_mul_exp_eq_exp_add, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ exp A = (rescale 1 : (a : A⟦X⟧) → A⟦X⟧) (exp A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ Eq (α := A⟦X⟧) (1 : A⟦X⟧) ((rescale (HAdd.hAdd (α := A) 1 (-1)) : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ HPow.hPow (β := ℕ) (exp A) 0 = (rescale (↑0 : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)

Tactic:
simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero,
      pow_zero (exp A), coe_comp]

Premises used: PowerSeries.rescale_zero, pow_zero, map_one, RingHom.coe_comp, PowerSeries.constantCoeff_exp, Function.comp_apply, Nat.cast_zero, PowerSeries.exp
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
k : ℕ
h : exp A ^ k = (rescale (↑k : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
⊢ exp A ^ (k + 1) = (rescale (↑(k + 1) : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)

Tactic:
simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
      id_apply, rescale_one] using pow_succ (exp A) k

Premises used: Nat.succ_eq_add_one, RingHom.id_apply, pow_succ, PowerSeries.exp_mul_exp_eq_exp_add, Nat.cast, Nat.cast_add, PowerSeries.exp, PowerSeries.rescale_one, Nat.cast_one
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
k : ℕ
zero : HPow.hPow (β := ℕ) (exp A) 0 = (rescale (↑0 : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
succ :
  ∀ (k : ℕ) (h : exp A ^ k = (rescale (↑k : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)),
    exp A ^ (k + 1) = (rescale (↑(k + 1) : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)
⊢ exp A ^ k = (rescale (↑k : A) : (a : A⟦X⟧) → A⟦X⟧) (exp A)

Tactic:
induction k with
  | zero =>
    simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero,
      pow_zero (exp A), coe_comp]
  | succ k h =>
    simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
      id_apply, rescale_one] using pow_succ (exp A) k

Premises used: Nat.succ_eq_add_one, RingHom.id_apply, pow_succ, PowerSeries.rescale_zero, PowerSeries.exp_mul_exp_eq_exp_add, Nat.cast, pow_zero, Nat.cast_add, map_one, RingHom.coe_comp, PowerSeries.constantCoeff_exp, Nat.zero, Function.comp_apply, Nat.cast_zero, PowerSeries.exp, PowerSeries.rescale_one, Nat.succ, Nat.cast_one
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
simp :
  Eq.{u_4 + 1} (α := A⟦X⟧)
    (∑ x ∈ Finset.range n,
      ({
            toFun := fun (f : A⟦X⟧) ↦
              mk fun (n : ℕ) ↦ HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
          (a : A⟦X⟧) → A⟦X⟧)
        (exp A))
    (mk fun (p : ℕ) ↦
      ∑ k ∈ Finset.range n,
        HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A))
⊢ Eq.{u_4 + 1} (α := A⟦X⟧) (∑ k ∈ Finset.range n, exp A ^ k)
    (mk fun (p : ℕ) ↦
      ∑ k ∈ Finset.range n,
        HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A))

Tactic:
simp only [exp_pow_eq_rescale_exp, rescale]

Premises used: PowerSeries.exp_pow_eq_rescale_exp, PowerSeries.rescale
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  ∀ (n_1 : ℕ),
    Eq.{u_4 + 1} (α := A)
      ((coeff n_1 : (a : A⟦X⟧) → A)
          (∑ x ∈ Finset.range n,
            ({
                  toFun := fun (f : A⟦X⟧) ↦
                    mk fun (n : ℕ) ↦
                      HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
                  map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
                (a : A⟦X⟧) → A⟦X⟧)
              (exp A)) :
        A)
      ((coeff n_1 : (a : A⟦X⟧) → A)
          (mk fun (p : ℕ) ↦
            ∑ k ∈ Finset.range n,
              HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A)) :
        A)
⊢ Eq.{u_4 + 1} (α := A⟦X⟧)
    (∑ x ∈ Finset.range n,
      ({
            toFun := fun (f : A⟦X⟧) ↦
              mk fun (n : ℕ) ↦ HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
          (a : A⟦X⟧) → A⟦X⟧)
        (exp A))
    (mk fun (p : ℕ) ↦
      ∑ k ∈ Finset.range n,
        HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A))

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Exp
Goal:
A : Type u_4
inst : CommRing A
inst_1 : Algebra ℚ A
n n_1 : ℕ
⊢ Eq.{u_4 + 1} (α := A)
    ((coeff n_1 : (a : A⟦X⟧) → A)
        (∑ x ∈ Finset.range n,
          ({
                toFun := fun (f : A⟦X⟧) ↦
                  mk fun (n : ℕ) ↦
                    HMul.hMul (β := A) (HPow.hPow (α := A) (↑x : A) n) ((coeff n : (a : A⟦X⟧) → A) f : A),
                map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
              (a : A⟦X⟧) → A⟦X⟧)
            (exp A)) :
      A)
    ((coeff n_1 : (a : A⟦X⟧) → A)
        (mk fun (p : ℕ) ↦
          ∑ k ∈ Finset.range n,
            HMul.hMul (β := A) (HPow.hPow (α := A) (↑k : A) p) ((algebraMap ℚ A : (a : ℚ) → A) (↑p ! : ℚ)⁻¹ : A)) :
      A)

Tactic:
simp only [one_div, coeff_mk, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    coeff_exp, map_sum]

Premises used: OneHom.coe_mk, PowerSeries.coeff_mk, PowerSeries.coeff_exp, map_sum, MonoidHom.coe_mk, one_div, RingHom.coe_mk
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
f : R⟦X⟧
⊢ (expand p hp : (a : R⟦X⟧) → R⟦X⟧) f = subst (HPow.hPow (α := R⟦X⟧) X p) f

Tactic:
simp [expand, MvPowerSeries.expand, subst, X]

Premises used: MvPowerSeries.expand, PowerSeries.subst, PowerSeries.X, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
rw : ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
| ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)

Tactic:
rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]

Premises used: PowerSeries.C, AlgHom.map_smul_of_tower, map_one, mul_one, PowerSeries.expand, PowerSeries.smul_eq_C_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
r : R
conv_lhs :
  Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
    ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
conv_lhs₁ : Eq (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)
⊢ Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
    ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)

Tactic:
conv_lhs => rw [← mul_one (C r), ← smul_eq_C_mul, expand, AlgHom.map_smul_of_tower,
    map_one, smul_eq_C_mul, mul_one]

Premises used: PowerSeries.C, AlgHom.map_smul_of_tower, map_one, mul_one, PowerSeries.expand, PowerSeries.smul_eq_C_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
H :
  ∀ (i : R⟦X⟧),
    Eq (α := R⟦X⟧) ((expand (p * q) ⋯ : (a : R⟦X⟧) → R⟦X⟧) i : R⟦X⟧)
      ((AlgHom.comp (expand p hp) (expand q hq) : (a : R⟦X⟧) → R⟦X⟧) i : R⟦X⟧)
⊢ Eq.{u_2 + 1} (α := R⟦X⟧ →ₐ[R] R⟦X⟧) (expand (p * q) ⋯) (AlgHom.comp (expand p hp) (expand q hq))

Tactic:
ext1 i
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
i : R⟦X⟧
⊢ Eq (α := R⟦X⟧) ((expand (p * q) ⋯ : (a : R⟦X⟧) → R⟦X⟧) i : R⟦X⟧)
    ((AlgHom.comp (expand p hp) (expand q hq) : (a : R⟦X⟧) → R⟦X⟧) i : R⟦X⟧)

Tactic:
simp [expand, MvPowerSeries.expand_mul_eq_comp p hp q hq]

Premises used: PowerSeries.expand, MvPowerSeries.expand_mul_eq_comp
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
q : ℕ
hq : q ≠ 0
φ : R⟦X⟧
⊢ Eq (α := R⟦X⟧) ((expand (p * q) ⋯ : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧)
    ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((expand q hq : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R⟦X⟧)

Tactic:
DFunLike.congr_fun (expand_mul_eq_comp p hp q hq) φ

Premises used: DFunLike.congr_fun, Classical.epsilon, Set.Mem, PowerSeries.expand_mul_eq_comp, Filter.lim, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
a : R
φ : R⟦X⟧
⊢ (expand p hp : (a : R⟦X⟧) → R⟦X⟧) (a • φ) = HSMul.hSMul (β := R⟦X⟧) a ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧)

Tactic:
AlgHom.map_smul_of_tower _ _ _

Premises used: AlgHom.map_smul_of_tower
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
⊢ (expand p hp : (a : R⟦X⟧) → R⟦X⟧) X = HPow.hPow (α := R⟦X⟧) X p

Tactic:
substAlgHom_X (HasSubst.X_pow hp)

Premises used: PowerSeries.substAlgHom_X, PowerSeries.HasSubst.X_pow, PowerSeries.X
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
d : ℕ
r : R
⊢ Eq (α := R⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) ((monomial d : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧)
    ((monomial (p * d) : (a : R) → R⟦X⟧) r : R⟦X⟧)

Tactic:
simp [expand, monomial, MvPowerSeries.expand_monomial]

Premises used: MvPowerSeries.expand_monomial, PowerSeries.monomial, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
⊢ Eq (α := R⟦X⟧ →ₐ[R] R⟦X⟧) (expand 1 ⋯) (AlgHom.id R R⟦X⟧)

Tactic:
simp [expand]

Premises used: PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
⊢ (expand 1 ⋯ : (a : R⟦X⟧) → R⟦X⟧) f = f

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
p : ℕ
hp : p ≠ 0
f : R →+* S
φ : R⟦X⟧
⊢ Eq (α := S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) : S⟦X⟧)
    ((expand p hp : (a : S⟦X⟧) → S⟦X⟧) ((map f : (a : R⟦X⟧) → S⟦X⟧) φ : S⟦X⟧) : S⟦X⟧)

Tactic:
simp [map, expand, MvPowerSeries.map_expand]

Premises used: PowerSeries.map, MvPowerSeries.map_expand, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
τ : Type u_1
S : Type u_3
inst : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
rw :
  Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S)
        (MvPowerSeries.subst (fun (x : Unit) ↦ f) φ) :
      MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)
rw₁ :
  Eq (α := MvPowerSeries τ S)
    (MvPowerSeries.subst (fun (i : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f)
      φ)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ)
rw₂ rw₃ :
  Eq (α := MvPowerSeries τ S)
    (MvPowerSeries.subst (fun (i : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f)
      φ)
    (MvPowerSeries.subst (fun (x : Unit) ↦ (MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f)
      φ)
⊢ Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) (subst f φ) : MvPowerSeries τ S)
    (subst ((MvPowerSeries.expand p hp : (a : MvPowerSeries τ S) → MvPowerSeries τ S) f) φ : MvPowerSeries τ S)

Tactic:
rw [PowerSeries.subst, MvPowerSeries.expand_subst _ hp (HasSubst.const hf) (φ := φ),
    PowerSeries.subst]

Premises used: PowerSeries.subst, MvPowerSeries.expand_subst, PowerSeries.HasSubst.const
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
rw :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)
rw₁ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₂ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p * m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₃ :
  Eq (α := R)
    ((MvPowerSeries.coeff (Finsupp.single () (p • m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₄ :
  Eq (α := R)
    ((MvPowerSeries.coeff (HSMul.hSMul (β := Unit →₀ ℕ) p (Finsupp.single () m)) : (a : R⟦X⟧) → R)
        ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) :
      R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
rw₅ rw₆ :
  Eq (α := R) ((MvPowerSeries.coeff (Finsupp.single () m) : (a : MvPowerSeries Unit R) → R) φ : R)
    ((MvPowerSeries.coeff (Finsupp.single () m) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff (p * m) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) φ : R)

Tactic:
rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]

Premises used: PowerSeries.coeff, MvPowerSeries.coeff_expand_smul, smul_eq_mul, PowerSeries.expand, Finsupp.smul_single
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
rw : ((coeff 0 : (a : R⟦X⟧) → R) φ : R)
| ((constantCoeff : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)

Tactic:
rw [← coeff_zero_eq_constantCoeff, ← mul_zero p, coeff_expand_mul]

Premises used: PowerSeries.coeff_expand_mul, MulZeroClass.mul_zero, PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
conv_lhs : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((constantCoeff : (a : R⟦X⟧) → R) φ : R)

Tactic:
conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← mul_zero p, coeff_expand_mul]

Premises used: PowerSeries.coeff_expand_mul, MulZeroClass.mul_zero, PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
h₁ : ¬p ∣ (Finsupp.single () m : (a : Unit) → ℕ) ()
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R) (0 : R)

Tactic:
rw [coeff, expand, MvPowerSeries.coeff_expand_of_not_dvd (i := ())]

Premises used: PowerSeries.coeff, MvPowerSeries.coeff_expand_of_not_dvd, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ ¬p ∣ (Finsupp.single () m : (a : Unit) → ℕ) ()

Tactic:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
rw :
  Subset (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
rw₁ rw₂ :
  Subset (α := Set (Unit →₀ ℕ)) ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
⊢ Subset (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)

Tactic:
rw [expand, MvPowerSeries.support_expand]

Premises used: MvPowerSeries.support_expand, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
rw :
  Eq (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
rw₁ rw₂ :
  Eq (α := Set (Unit →₀ ℕ)) ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)
⊢ Eq (α := Set (Unit →₀ ℕ)) (Function.support.{0, u_2} (M := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ))
    ((fun (x : Unit →₀ ℕ) ↦ p • x) '' Function.support φ)

Tactic:
rw [expand, MvPowerSeries.support_expand]

Premises used: MvPowerSeries.support_expand, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
pos :
  ∀ (h : p ∣ n),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
      ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
neg : ∀ (h : ¬p ∣ n), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R) (0 : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    (if p ∣ n then (coeff (n / p) : (a : R⟦X⟧) → R) φ else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : p ∣ n
pos :
  ∀ (q : ℕ) (hq : n = p * q),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
      ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)

Tactic:
obtain ⟨q, hq⟩ := h
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
pos :
  Eq (α := R) ((coeff (p * q) : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
pos₁ : Eq (α := R) ((coeff q : (a : R⟦X⟧) → R) φ : R) ((coeff (p * q / p) : (a : R⟦X⟧) → R) φ : R)
pos₂ pos₃ : Eq (α := R) ((coeff q : (a : R⟦X⟧) → R) φ : R) ((coeff q : (a : R⟦X⟧) → R) φ : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R)
    ((coeff (n / p) : (a : R⟦X⟧) → R) φ : R)

Tactic:
rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]

Premises used: PowerSeries.coeff_expand_mul, Nat.mul_div_cancel_left, Nat.pos_of_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : ¬p ∣ n
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R) (0 : R)

Tactic:
coeff_expand_of_not_dvd p hp _ h

Premises used: PowerSeries.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : ¬p ∣ n
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ : R⟦X⟧) : R) (0 : R)

Tactic:
exact coeff_expand_of_not_dvd p hp _ h

Premises used: PowerSeries.coeff_expand_of_not_dvd
-- Module: Mathlib.RingTheory.PowerSeries.Expand
Goal:
R : Type u_2
inst : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
simp_rw : order.{u_2} (R := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) = p • φ.order
simp_rw₁ :
  MvPowerSeries.order.{0, u_2} (σ := Unit) (R := R) ((MvPowerSeries.expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) =
    p • MvPowerSeries.order φ
⊢ order.{u_2} (R := R) ((expand p hp : (a : R⟦X⟧) → R⟦X⟧) φ) = p • φ.order

Tactic:
simp_rw [expand, order_eq_order, MvPowerSeries.order_expand p hp φ]

Premises used: PowerSeries.order_eq_order, MvPowerSeries.order_expand, PowerSeries.expand
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
⊢ gaussNorm v c f = ⨆ (i : ℕ), v ((coeff i : (a : R⟦X⟧) → R) f) * c ^ i

Tactic:
Equiv.iSup_congr (Finsupp.uniqueEquiv ()) ?_

Premises used: Unit.unit, Finsupp.uniqueEquiv, MvPowerSeries.gaussNorm, Equiv.iSup_congr
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
refine :
  ∀ (x : Unit →₀ ℕ),
    v ((coeff ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) x) : (a : R⟦X⟧) → R) f) *
        HPow.hPow (β := ℕ) c ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) x : ℕ) =
      v ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f) *
        x.prod fun (x1 : Unit) (x2 : ℕ) ↦ HPow.hPow (α := ℝ) ((fun (x : Unit) ↦ c) x1) x2
⊢ gaussNorm v c f = ⨆ (i : ℕ), v ((coeff i : (a : R⟦X⟧) → R) f) * c ^ i

Tactic:
refine Equiv.iSup_congr (Finsupp.uniqueEquiv ()) ?_

Premises used: Unit.unit, Finsupp.uniqueEquiv, Equiv.iSup_congr
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ Finsupp.single () ((x : (a : Unit) → ℕ) PUnit.unit) = x

Tactic:
grind
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
x : Unit →₀ ℕ
⊢ v ((coeff ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) x) : (a : R⟦X⟧) → R) f) *
      HPow.hPow (β := ℕ) c ((Finsupp.uniqueEquiv () : (a : Unit →₀ ℕ) → ℕ) x : ℕ) =
    v ((MvPowerSeries.coeff x : (a : MvPowerSeries Unit R) → R) f) *
      x.prod fun (x1 : Unit) (x2 : ℕ) ↦ HPow.hPow (α := ℝ) ((fun (x : Unit) ↦ c) x1) x2

Tactic:
simp only [coeff, Finsupp.uniqueEquiv_apply, PUnit.default_eq_unit, Finsupp.prod_pow,
    Finset.univ_unique, Finset.prod_singleton, show (Finsupp.single () (x PUnit.unit)) = x by grind]

Premises used: Finset.prod_singleton, Finset.univ_unique, PowerSeries.coeff, Finsupp.prod_pow, PUnit.default_eq_unit, Finsupp.uniqueEquiv_apply
-- Module: Mathlib.RingTheory.PowerSeries.GaussNorm
Goal:
R : Type u_1
inst : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
this :
  Eq (α := Set ℝ) (Set.range fun (t : ℕ) ↦ v ((coeff t : (a : R⟦X⟧) → R) f) * c ^ t)
    (Set.range fun (t : Unit →₀ ℕ) ↦
      v ((MvPowerSeries.coeff t : (a : MvPowerSeries Unit R) → R) f) * t.prod fun (x : Unit) (x2 : ℕ) ↦ c ^ x2)
⊢ MvPowerSeries.HasGaussNorm v (fun (x : Unit) ↦ c) f

Tactic:
simpa only [MvPowerSeries.HasGaussNorm, ← this]

Premises used: MvPowerSeries.HasGaussNorm