awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
m : ℕ
hm : m < 1
mpr mpr₁ mpr₂ mpr₃ : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) (0 : R)

Tactic:
rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]

Premises used: Nat.le_of_succ_le_succ, Nat.eq_zero_of_le_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
n : ℕ
rw :
  (↑((coeff n : (a : (↥T)⟦X⟧) → ↥T)
          (mk fun (n : ℕ) ↦ Subtype.mk (p := fun (x : R) ↦ x ∈ T) ((coeff n : (a : R⟦X⟧) → R) p) ⋯)) :
      R) =
    (coeff n : (a : R⟦X⟧) → R) p
rw₁ rw₂ :
  Eq (α := R) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) ((coeff n : (a : R⟦X⟧) → R) p) ⋯) : R) : R)
    ((coeff n : (a : R⟦X⟧) → R) p : R)
⊢ Eq (α := R) ((↑((coeff n : (a : (↥T)⟦X⟧) → ↥T) (p.toSubring T hp)) : R) : R) ((coeff n : (a : R⟦X⟧) → R) p : R)

Tactic:
rw [toSubring, coeff_mk]

Premises used: PowerSeries.coeff_mk, PowerSeries.toSubring
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
⊢ Eq (α := R) ((↑((constantCoeff : (a : (↥T)⟦X⟧) → ↥T) (p.toSubring T hp)) : R) : R)
    ((constantCoeff : (a : R⟦X⟧) → R) p : R)

Tactic:
coeff_zero_eq_constantCoeff_apply p

Premises used: PowerSeries.coeff_zero_eq_constantCoeff_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), Membership.mem (α := R) T ((coeff n : (a : R⟦X⟧) → R) p : R)
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((map T.subtype : (a : (↥T)⟦X⟧) → R⟦X⟧) (p.toSubring T hp) : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) p : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
h :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
      ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 1 : R)) : R)
      ((coeff n : (a : R⟦X⟧) → R) 1 : R)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 1 : R)) 1

Tactic:
ext1
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
h : (if n = 0 then a ^ n else 0) = if n = 0 then 1 else 0
⊢ Eq.{u_1 + 1} (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 1 : R)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 1 : R)

Tactic:
simp only [mul_boole, PowerSeries.coeff_mk, PowerSeries.coeff_one]

Premises used: mul_boole, PowerSeries.coeff_mk, PowerSeries.coeff_one
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
pos : ∀ (h : n = 0), a ^ n = 1
neg : ∀ (h : ¬n = 0), Eq.{u_1 + 1} (α := R) 0 0
⊢ (if n = 0 then a ^ n else 0) = if n = 0 then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
h : n = 0
pos : HPow.hPow (β := ℕ) a 0 = 1
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ a ^ n = 1

Tactic:
rw [h, pow_zero a]

Premises used: pow_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R)
      ((coeff n : (a : R⟦X⟧) → R)
          (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)) :
        R)
      ((coeff n : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R))
            (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R))) :
        R)
⊢ (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)) =
    HMul.hMul (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R))
      (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R))

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n : ℕ
h :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      a ^ n * HMul.hMul (α := R) (β := R) ((coeff i.1 : (a : R⟦X⟧) → R) f : R) ((coeff i.2 : (a : R⟦X⟧) → R) g : R))
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := R) (β := R)
        ((coeff p.1 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R)) :
          R)
        ((coeff p.2 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R)) :
          R))
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R))
          (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R))) :
      R)

Tactic:
rw [PowerSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul, Finset.mul_sum]

Premises used: Finset.mul_sum, PowerSeries.coeff_mk, PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n : ℕ
h :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ n,
    a ^ n * HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R)) :
          R)
        ((coeff x.2 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R)) :
          R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      a ^ n * HMul.hMul (α := R) (β := R) ((coeff i.1 : (a : R⟦X⟧) → R) f : R) ((coeff i.2 : (a : R⟦X⟧) → R) g : R))
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := R) (β := R)
        ((coeff p.1 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R)) :
          R)
        ((coeff p.2 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R)) :
          R))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n : ℕ
h :
  ∀ (a_1 b : ℕ),
    a_1 + b = n →
      a ^ n * HMul.hMul (α := R) (β := R) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) ((coeff b : (a : R⟦X⟧) → R) g : R) =
        HMul.hMul (β := R) (a ^ a_1) ((coeff a_1 : (a : R⟦X⟧) → R) f : R) *
          HMul.hMul (β := R) (a ^ b) ((coeff b : (a : R⟦X⟧) → R) g : R)
⊢ ∀ x ∈ @antidiagonal _ instAddMonoid _ n,
    a ^ n * HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
      HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R)) :
          R)
        ((coeff x.2 : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) g : R)) :
          R)

Tactic:
simp only [coeff_mk, Prod.forall, mem_antidiagonal]

Premises used: PowerSeries.coeff_mk, Finset.HasAntidiagonal.mem_antidiagonal, Prod.forall
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n b c : ℕ
H : b + c = n
h :
  a ^ (b + c) * HMul.hMul (α := R) (β := R) ((coeff b : (a : R⟦X⟧) → R) f : R) ((coeff c : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (β := R) (a ^ b) ((coeff b : (a : R⟦X⟧) → R) f : R) *
      HMul.hMul (β := R) (a ^ c) ((coeff c : (a : R⟦X⟧) → R) g : R)
h₁ :
  a ^ b * a ^ c * HMul.hMul (α := R) (β := R) ((coeff b : (a : R⟦X⟧) → R) f : R) ((coeff c : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (β := R) (a ^ b) ((coeff b : (a : R⟦X⟧) → R) f : R) *
      HMul.hMul (β := R) (a ^ c) ((coeff c : (a : R⟦X⟧) → R) g : R)
h₂ h₃ :
  HMul.hMul (β := R) (a ^ b) ((coeff b : (a : R⟦X⟧) → R) f : R) *
      HMul.hMul (β := R) (a ^ c) ((coeff c : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (β := R) (a ^ b) ((coeff b : (a : R⟦X⟧) → R) f : R) *
      HMul.hMul (β := R) (a ^ c) ((coeff c : (a : R⟦X⟧) → R) g : R)
⊢ a ^ n * HMul.hMul (α := R) (β := R) ((coeff b : (a : R⟦X⟧) → R) f : R) ((coeff c : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (β := R) (a ^ b) ((coeff b : (a : R⟦X⟧) → R) f : R) *
      HMul.hMul (β := R) (a ^ c) ((coeff c : (a : R⟦X⟧) → R) g : R)

Tactic:
rw [← H, pow_add, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, pow_add
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
h :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R)
      ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 0 : R)) : R)
      ((coeff n : (a : R⟦X⟧) → R) 0 : R)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 0 : R)) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 0 : R)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)

Tactic:
simp only [map_zero, PowerSeries.coeff_mk, mul_zero]

Premises used: map_zero, PowerSeries.coeff_mk, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
x y : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R)
      ((coeff n : (a : R⟦X⟧) → R)
          (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (x + y) : R)) :
        R)
      ((coeff n : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) x : R))
            (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) y : R))) :
        R)
⊢ (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (x + y) : R)) =
    HAdd.hAdd (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) x : R))
      (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) y : R))

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
x y : R⟦X⟧
n : ℕ
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (x + y) : R)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) x : R))
          (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) y : R))) :
      R)

Tactic:
mul_add _ _ _

Premises used: mul_add, PowerSeries.mk
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a : R
x y : R⟦X⟧
n : ℕ
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (x + y) : R)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) x : R))
          (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) y : R))) :
      R)

Tactic:
exact mul_add _ _ _

Premises used: mul_add
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
a : R
n : ℕ
⊢ (coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) =
    HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) f : R)

Tactic:
coeff_mk n (fun n ↦ a ^ n * coeff n f)

Premises used: HMul.hMul, PowerSeries.coeff, PowerSeries.coeff_mk, HPow.hPow, PowerSeries.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a :
  ∀ (x : R⟦X⟧) (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale 0 : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) ((RingHom.comp C constantCoeff : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →+* R⟦X⟧) (rescale 0) (RingHom.comp C constantCoeff)

Tactic:
ext x n
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R⟦X⟧
n : ℕ
a :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (({
                toFun := fun (f : R⟦X⟧) ↦
                  mk fun (n : ℕ) ↦ HMul.hMul (β := R) (HPow.hPow (α := R) 0 n) ((coeff n : (a : R⟦X⟧) → R) f : R),
                map_one' := ⋯, map_mul' := ⋯ } :
              (a : R⟦X⟧) → R⟦X⟧)
            x :
          R⟦X⟧) :
      R)
    (if n = 0 then (constantCoeff : (a : R⟦X⟧) → R) x else 0 : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale 0 : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((RingHom.comp C constantCoeff : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk,
    coeff_C]

Premises used: PowerSeries.coeff_C, RingHom.coe_mk, RingHom.coe_comp, Function.comp_apply, PowerSeries.rescale
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R⟦X⟧
n : ℕ
pos :
  ∀ (h : n = 0),
    Eq (α := R)
      ((coeff n : (a : R⟦X⟧) → R)
          (({
                  toFun := fun (f : R⟦X⟧) ↦
                    mk fun (n : ℕ) ↦ HMul.hMul (β := R) (HPow.hPow (α := R) 0 n) ((coeff n : (a : R⟦X⟧) → R) f : R),
                  map_one' := ⋯, map_mul' := ⋯ } :
                (a : R⟦X⟧) → R⟦X⟧)
              x :
            R⟦X⟧) :
        R)
      ((constantCoeff : (a : R⟦X⟧) → R) x : R)
neg :
  ∀ (h : ¬n = 0),
    Eq (α := R)
      ((coeff n : (a : R⟦X⟧) → R)
          (({
                  toFun := fun (f : R⟦X⟧) ↦
                    mk fun (n : ℕ) ↦ HMul.hMul (β := R) (HPow.hPow (α := R) 0 n) ((coeff n : (a : R⟦X⟧) → R) f : R),
                  map_one' := ⋯, map_mul' := ⋯ } :
                (a : R⟦X⟧) → R⟦X⟧)
              x :
            R⟦X⟧) :
        R)
      (0 : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (({
                toFun := fun (f : R⟦X⟧) ↦
                  mk fun (n : ℕ) ↦ HMul.hMul (β := R) (HPow.hPow (α := R) 0 n) ((coeff n : (a : R⟦X⟧) → R) f : R),
                map_one' := ⋯, map_mul' := ⋯ } :
              (a : R⟦X⟧) → R⟦X⟧)
            x :
          R⟦X⟧) :
      R)
    (if n = 0 then (constantCoeff : (a : R⟦X⟧) → R) x else 0 : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R⟦X⟧
n : ℕ
h : n = 0
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (({
                toFun := fun (f : R⟦X⟧) ↦
                  mk fun (n : ℕ) ↦ HMul.hMul (β := R) (HPow.hPow (α := R) 0 n) ((coeff n : (a : R⟦X⟧) → R) f : R),
                map_one' := ⋯, map_mul' := ⋯ } :
              (a : R⟦X⟧) → R⟦X⟧)
            x :
          R⟦X⟧) :
      R)
    ((constantCoeff : (a : R⟦X⟧) → R) x : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R⟦X⟧
n : ℕ
h : ¬n = 0
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (({
                toFun := fun (f : R⟦X⟧) ↦
                  mk fun (n : ℕ) ↦ HMul.hMul (β := R) (HPow.hPow (α := R) 0 n) ((coeff n : (a : R⟦X⟧) → R) f : R),
                map_one' := ⋯, map_mul' := ⋯ } :
              (a : R⟦X⟧) → R⟦X⟧)
            x :
          R⟦X⟧) :
      R)
    (0 : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
⊢ Eq (α := R⟦X⟧) ((rescale 0 : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
    ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : R⟦X⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a :
  ∀ (x : R⟦X⟧) (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale 1 : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) ((RingHom.id R⟦X⟧ : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →+* R⟦X⟧) (rescale 1) (RingHom.id R⟦X⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale 1 : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((RingHom.id R⟦X⟧ : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)

Tactic:
simp [coeff_rescale]

Premises used: PowerSeries.coeff_rescale
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → R
a : R
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) (mk f) : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ a ^ n * f n) : R)
⊢ Eq (α := R⟦X⟧) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) (mk f) : R⟦X⟧) (mk fun (n : ℕ) ↦ a ^ n * f n : R⟦X⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → R
a : R
n : ℕ
h :
  HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) (mk f) : R) =
    (coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ a ^ n * f n)
h₁ : a ^ n * f n = (coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ a ^ n * f n)
h₂ h₃ : a ^ n * f n = a ^ n * f n
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) (mk f) : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ a ^ n * f n) : R)

Tactic:
rw [coeff_rescale, coeff_mk, coeff_mk]

Premises used: PowerSeries.coeff_rescale, PowerSeries.coeff_mk
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a b : R
a₁ :
  ∀ (x : R⟦X⟧) (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale (a * b) : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) ((RingHom.comp (rescale b) (rescale a) : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
⊢ Eq (α := R⟦X⟧ →+* R⟦X⟧) (rescale (a * b)) (RingHom.comp (rescale b) (rescale a))

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
a b : R
x : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale (a * b) : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((RingHom.comp (rescale b) (rescale a) : (a : R⟦X⟧) → R⟦X⟧) x : R⟦X⟧) : R)

Tactic:
simp [← rescale_rescale]

Premises used: PowerSeries.rescale_rescale
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := S)
      ((coeff n : (a : S⟦X⟧) → S)
          (((rescale ((φ : (a : R) → S) r) : S⟦X⟧ →+* S⟦X⟧) : (a : S⟦X⟧) → S⟦X⟧)
              ((map φ : (a : R⟦X⟧) → S⟦X⟧) f : S⟦X⟧) :
            S⟦X⟧) :
        S)
      ((coeff n : (a : S⟦X⟧) → S) ((map φ : (a : R⟦X⟧) → S⟦X⟧) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f) : S⟦X⟧) : S)
⊢ Eq (α := S⟦X⟧)
    (((rescale ((φ : (a : R) → S) r) : S⟦X⟧ →+* S⟦X⟧) : (a : S⟦X⟧) → S⟦X⟧) ((map φ : (a : R⟦X⟧) → S⟦X⟧) f : S⟦X⟧) :
      S⟦X⟧)
    ((map φ : (a : R⟦X⟧) → S⟦X⟧) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f) : S⟦X⟧)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := S)
    ((coeff n : (a : S⟦X⟧) → S)
        (((rescale ((φ : (a : R) → S) r) : S⟦X⟧ →+* S⟦X⟧) : (a : S⟦X⟧) → S⟦X⟧) ((map φ : (a : R⟦X⟧) → S⟦X⟧) f : S⟦X⟧) :
          S⟦X⟧) :
      S)
    ((coeff n : (a : S⟦X⟧) → S) ((map φ : (a : R⟦X⟧) → S⟦X⟧) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f) : S⟦X⟧) : S)

Tactic:
simp [coeff_rescale, coeff_map, map_mul, map_pow]

Premises used: PowerSeries.coeff_rescale, map_pow, map_mul, PowerSeries.coeff_map
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
S : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra A R
inst_3 : CommSemiring S
inst_4 : Algebra A S
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
⊢ Eq (α := S⟦X⟧)
    (((rescale (((↑φ : R →+* S) : (a : R) → S) ((algebraMap A R : (a : A) → R) a : R)) : S⟦X⟧ →+* S⟦X⟧) :
          (a : S⟦X⟧) → S⟦X⟧)
        (((map (↑φ : R →+* S) : RingHom.{u_1, u_3} R⟦X⟧ S⟦X⟧) : (a : R⟦X⟧) → S⟦X⟧) f : S⟦X⟧) :
      S⟦X⟧)
    (((map (↑φ : R →+* S) : RingHom.{u_1, u_3} R⟦X⟧ S⟦X⟧) : (a : R⟦X⟧) → S⟦X⟧)
        (((rescale ((algebraMap A R : (a : A) → R) a) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f) :
      S⟦X⟧)

Tactic:
rescale_map (φ : R →+* S) _ _

Premises used: PowerSeries.rescale_map, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
S : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra A R
inst_3 : CommSemiring S
inst_4 : Algebra A S
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
h :
  Eq.{u_3 + 1} (α := S) ((algebraMap A S : (a : A) → S) a : S)
    (((↑φ : R →+* S) : (a : R) → S) ((algebraMap A R : (a : A) → R) a : R) : S)
⊢ Eq (α := S⟦X⟧)
    (((rescale ((algebraMap A S : (a : A) → S) a) : S⟦X⟧ →+* S⟦X⟧) : (a : S⟦X⟧) → S⟦X⟧)
        (((map (↑φ : R →+* S) : RingHom.{u_1, u_3} R⟦X⟧ S⟦X⟧) : (a : R⟦X⟧) → S⟦X⟧) f : S⟦X⟧) :
      S⟦X⟧)
    (((map (↑φ : R →+* S) : RingHom.{u_1, u_3} R⟦X⟧ S⟦X⟧) : (a : R⟦X⟧) → S⟦X⟧)
        (((rescale ((algebraMap A R : (a : A) → R) a) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f) :
      S⟦X⟧)

Tactic:
convert! rescale_map (φ : R →+* S) _ _

Premises used: PowerSeries.rescale_map, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
S : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra A R
inst_3 : CommSemiring S
inst_4 : Algebra A S
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap A S : (a : A) → S) a : S)
    (((↑φ : R →+* S) : (a : R) → S) ((algebraMap A R : (a : A) → R) a : R) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
simp :
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff (single () d) : (a : R⟦X⟧) → R) (∏ j ∈ s, f j) : R)
    (∑ x ∈ s.finsuppAntidiag d,
        ∏ x_1 ∈ s, (MvPowerSeries.coeff (single () ((x : (a : ι) → ℕ) x_1)) : (a : R⟦X⟧) → R) (f x_1) :
      R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : R⟦X⟧) → R) (∏ j ∈ s, f j) : R)
    (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → ℕ) i) : (a : R⟦X⟧) → R) (f i) : R)

Tactic:
simp only [coeff]

Premises used: PowerSeries.coeff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ s.finsuppAntidiag d,
      ∏ i ∈ s,
        (MvPowerSeries.coeff
              ((((Equiv.toEmbedding
                          (AddEquiv.toEquiv (Finsupp.mapRange.addEquiv (AddEquiv.symm (Finsupp.uniqueAddEquiv ())))) :
                        (a : ι →₀ ℕ) → ι →₀ Unit →₀ ℕ)
                      x :
                    ι →₀ Unit →₀ ℕ) :
                  (a : ι) → Unit →₀ ℕ)
                i) :
            (a : MvPowerSeries Unit R) → R)
          (f i))
    (∑ x ∈ s.finsuppAntidiag d,
      ∏ x_1 ∈ s, (MvPowerSeries.coeff (single () ((x : (a : ι) → ℕ) x_1)) : (a : R⟦X⟧) → R) (f x_1))
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff (single () d) : (a : R⟦X⟧) → R) (∏ j ∈ s, f j) : R)
    (∑ x ∈ s.finsuppAntidiag d,
        ∏ x_1 ∈ s, (MvPowerSeries.coeff (single () ((x : (a : ι) → ℕ) x_1)) : (a : R⟦X⟧) → R) (f x_1) :
      R)

Tactic:
rw [MvPowerSeries.coeff_prod, ← Finsupp.uniqueAddEquiv_symm_apply _ d,
    ← mapRange_finsuppAntidiag_eq, sum_map]

Premises used: Finset.sum_map, Finset.mapRange_finsuppAntidiag_eq, MvPowerSeries.coeff_prod, Finsupp.uniqueAddEquiv_symm_apply