awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : 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) (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)
have 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))
Tactic: rw [PowerSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n : ℕ
⊢ 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))
have 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)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n : ℕ
⊢ ∀ 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)
have 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)
Tactic: simp only [coeff_mk, Prod.forall, mem_antidiagonal]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
f g : R⟦X⟧
n b c : ℕ
H : b + c = n
⊢ 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)
have 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)
Tactic: rw [← H, pow_add, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← H, pow_add, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← H, pow_add, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (mk fun (n : ℕ) ↦ HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) 0 : R)) 0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a : R
x y : R⟦X⟧
⊢ (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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →+* R⟦X⟧) (rescale 0) (RingHom.comp C constantCoeff)
have 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)
Tactic: ext x n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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)
have 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' := sorry, map_mul' := sorry } :
            (a : R⟦X⟧) → R⟦X⟧)
          x :
        R⟦X⟧) :
    R)
  (if n = 0 then (constantCoeff : (a : R⟦X⟧) → R) x else 0 : R)
Tactic: simp only [Function.comp_apply, RingHom.coe_comp, rescale, RingHom.coe_mk,
    coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x : R⟦X⟧
n : ℕ
⊢ 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)
have 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' := sorry, map_mul' := sorry } :
              (a : R⟦X⟧) → R⟦X⟧)
            x :
          R⟦X⟧) :
      R)
    ((constantCoeff : (a : R⟦X⟧) → R) x : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have 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' := sorry, map_mul' := sorry } :
              (a : R⟦X⟧) → R⟦X⟧)
            x :
          R⟦X⟧) :
      R)
    (0 : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →+* R⟦X⟧) (rescale 1) (RingHom.id R⟦X⟧)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → R
a : R
⊢ Eq (α := R⟦X⟧) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) (mk f) : R⟦X⟧) (mk fun (n : ℕ) ↦ a ^ n * f n : R⟦X⟧)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → R
a : R
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)
have 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)
Tactic: rw [coeff_rescale, coeff_mk, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have h₁ : a ^ n * f n = (coeff n : (a : R⟦X⟧) → R) (mk fun (n : ℕ) ↦ a ^ n * f n)
Tactic: rw [coeff_rescale, coeff_mk, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ 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)
have h₂ : a ^ n * f n = a ^ n * f n
Tactic: rw [coeff_rescale, coeff_mk, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : R
⊢ Eq (α := R⟦X⟧ →+* R⟦X⟧) (rescale (a * b)) (RingHom.comp (rescale b) (rescale a))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
⊢ 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⟧)
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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 ((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⟧)
have 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)
Tactic: convert! rescale_map (φ : R →+* S) _ _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ 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)
have 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)
Tactic: simp only [coeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ 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)
have 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))
Tactic: rw [MvPowerSeries.coeff_prod, ← Finsupp.uniqueAddEquiv_symm_apply _ d,
    ← mapRange_finsuppAntidiag_eq, sum_map]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
k n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ ^ k) : R)
    (∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) φ : R)
have h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
Tactic: have h₁ (i : ℕ) : Function.const ℕ φ i = φ := rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ ^ k) : R)
    (∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) φ : R)
have h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
Tactic: have h₂ (i : ℕ) : ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i := by
    apply prod_range_induction (fun _ => φ) (fun i => φ ^ i) rfl i (fun _ => congrFun rfl)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ ^ k) : R)
    (∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) φ : R)
have rw : Eq.{u_2 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) : R)
  (∑ l ∈ (range k).finsuppAntidiag n,
      ∏ i ∈ range k, (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) (Function.const ℕ φ k) :
    R)
Tactic: rw [← h₂, ← h₁ k]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ * ψ) =
    HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) ψ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) ψ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
have this : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
Tactic: have : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
this : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ * ψ) =
    HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) ((constantCoeff : (a : R⟦X⟧) → R) ψ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) ψ : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
have rw : (0, 1) ∉ {(1, 0)}
Tactic: rw [coeff_mul, this, Finset.sum_insert, Finset.sum_singleton, coeff_zero_eq_constantCoeff,
    mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n) =
    HMul.hMul (α := R) (β := R) ((↑n : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n - 1)
have inl : (coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) =
  HMul.hMul (α := R) (β := R) ((↑0 : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (HSub.hSub (α := ℕ) 0 1)
Tactic: rcases Nat.eq_zero_or_pos n with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
φ : R⟦X⟧
inl :
  (coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) =
    HMul.hMul (α := R) (β := R) ((↑0 : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (HSub.hSub (α := ℕ) 0 1)
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n) =
    HMul.hMul (α := R) (β := R) ((↑n : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n - 1)
have inr : ∀ (hn : n > 0),
  (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n) =
    HMul.hMul (α := R) (β := R) ((↑n : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n - 1)
Tactic: rcases Nat.eq_zero_or_pos n with (rfl | hn)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ ^ (n' + 1)) =
    HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
have h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
Tactic: have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ ^ (n' + 1)) =
    HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
have h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
Tactic: have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih :
  ∀ (hn : n' > 0),
    (coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') =
      HMul.hMul (α := R) (β := R) ((↑n' : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
⊢ (coeff 1 : (a : R⟦X⟧) → R) (φ ^ (n' + 1)) =
    HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
have inr : HMul.hMul (α := R) (β := R) ((coeff (0, 1).1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((coeff (0, 1).2 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (α := R) (β := R) ((coeff (1, 0).1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
      ((coeff (1, 0).2 : (a : R⟦X⟧) → R) φ : R) =
  HMul.hMul (α := R) (β := R) ((↑(n' + 1) : R) : R) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
    HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (n' + 1 - 1)
Tactic: rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]