awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
ι : Type u_3
f : ι → ℕ
g : ι → R
s : Finset ι
⊢ Eq.{u_2 + 1} (α := R⟦X⟧) (∏ i ∈ s, (monomial (f i) : (a : R) → R⟦X⟧) (g i) : R⟦X⟧)
    ((monomial (∑ i ∈ s, f i) : (a : R) → R⟦X⟧) (∏ i ∈ s, g i) : R⟦X⟧)

Tactic:
simpa [monomial, Finsupp.single_finsetSum] using
    MvPowerSeries.prod_monomial (fun i ↦ Finsupp.single () (f i)) g s

Premises used: Unit.unit, PowerSeries.monomial, Finsupp.single_finsetSum, MvPowerSeries.prod_monomial, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
m : ℕ
a : R
n : ℕ
⊢ HPow.hPow (α := R⟦X⟧) ((monomial m : (a : R) → R⟦X⟧) a : R⟦X⟧) n = (monomial (n * m) : (a : R) → R⟦X⟧) (a ^ n)

Tactic:
simpa [monomial] using MvPowerSeries.monomial_pow (Finsupp.single () m) a n

Premises used: Unit.unit, MvPowerSeries.monomial_pow, PowerSeries.monomial, Finsupp.single
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
k n : ℕ
φ : R⟦X⟧
⊢ ∀ (i : ℕ), Function.const ℕ φ i = φ

Tactic:
have h₁ (i : ℕ) : Function.const ℕ φ i = φ := rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
i : ℕ
⊢ ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i

Tactic:
apply prod_range_induction (fun _ => φ) (fun i => φ ^ i) rfl i (fun _ => congrFun rfl)

Premises used: Finset.prod_range_induction, HPow.hPow, congrFun, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
⊢ ∀ (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)
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
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)
⊢ 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)

Tactic:
rw [← h₂, ← h₁ k]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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.{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:
apply coeff_prod (f := Function.const ℕ φ) (d := n) (s := range k)

Premises used: Finset.range, PowerSeries.coeff_prod, Nat, Function.const
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}

Tactic:
rfl

Premises used: List.map, Multiset.Nat.antidiagonal, Multiset.ndinsert, rfl, List.Nat.antidiagonal, ite
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}

Tactic:
have : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
this : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
rw : (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)

Tactic:
rw [coeff_mul, this, Finset.sum_insert, Finset.sum_singleton, coeff_zero_eq_constantCoeff,
    mul_comm, add_comm]

Premises used: add_comm, Finset.sum_singleton, PowerSeries.coeff_mul, PowerSeries.coeff_zero_eq_constantCoeff, mul_comm, Finset.sum_insert
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ ψ : R⟦X⟧
this : Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
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)
⊢ (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)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
⊢ (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:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_2
inst : CommSemiring R
φ : R⟦X⟧
hn : GT.gt (α := ℕ) 0 0
⊢ (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:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
m : ℕ
⊢ φ ^ (m + 1) = φ ^ m * φ

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, npowRec, Finset.sum, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
m : ℕ
⊢ φ ^ (m + 1) = φ ^ m * φ

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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
⊢ ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ

Tactic:
have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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 * φ
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}

Tactic:
rfl

Premises used: List.map, Multiset.Nat.antidiagonal, Multiset.ndinsert, rfl, List.Nat.antidiagonal, ite
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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 * φ
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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 * φ
⊢ Eq (α := Finset (ℕ × ℕ)) (@antidiagonal _ Nat.instAddMonoid _ 1) {(0, 1), (1, 0)}

Tactic:
have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
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)
inr₁ : (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)

Tactic:
rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]

Premises used: Finset.sum_singleton, PowerSeries.coeff_mul, Finset.sum_insert
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
inr :
  HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
⊢ 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:
simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one,
          add_tsub_cancel_right]

Premises used: map_pow, Nat.cast_add, PowerSeries.coeff_zero_eq_constantCoeff, add_tsub_cancel_right, Nat.cast_one
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
⊢ n' = 0 ∨ 1 ≤ n'

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
⊢ n' = 0 ∨ 1 ≤ n'

Tactic:
have h₀ : n' = 0 ∨ 1 ≤ n' := by lia
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h₀ : n' = 0 ∨ 1 ≤ n'
inr :
  ∀ (h' : n' = 0),
    HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
inr₁ :
  ∀ (h' : 1 ≤ n'),
    HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'

Tactic:
rcases h₀ with h' | h'
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h' : n' = 0
inr :
  ∀
    (h'' :
      ¬HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
              ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
            HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R)
              ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
          HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
            HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'),
    False
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'

Tactic:
by_contra h''
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h' : n' = 0
h'' :
  ¬HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
⊢ ¬HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0)
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) : R)
          ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0

Tactic:
rw [h'] at h''
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h' : n' = 0
h'' :
  ¬HMul.hMul (β := R) (HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0)
          ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
        HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (HPow.hPow (β := ℕ) φ 0) : R)
          ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
      HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
        HPow.hPow (α := R) (β := ℕ) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) 0
⊢ ¬(coeff 1 : (a : R⟦X⟧) → R) φ = HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)

Tactic:
simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''

Premises used: MulZeroClass.zero_mul, pow_zero, PowerSeries.coeff_one, reduceIte, mul_one, add_zero, one_ne_zero, one_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h' : n' = 0
h'' :
  ¬(coeff 1 : (a : R⟦X⟧) → R) φ = HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑0 : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R)
⊢ False

Tactic:
norm_num at h''
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h' : 1 ≤ n'
inr :
  HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (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))
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'
inr₁ : n' > 0
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (α := R) (β := R) ((coeff 1 : (a : R⟦X⟧) → R) (φ ^ n') : R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'

Tactic:
rw [ih]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)}
h' : 1 ≤ n'
lhs :
  HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
      ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
    HMul.hMul (β := R)
      (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))
      ((constantCoeff : (a : R⟦X⟧) → R) φ : R)
| HMul.hMul (β := R) (HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n')
        ((coeff 1 : (a : R⟦X⟧) → R) φ : R) +
      HMul.hMul (β := R)
        (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))
        ((constantCoeff : (a : R⟦X⟧) → R) φ : R) =
    HMul.hMul (β := R) (HAdd.hAdd (α := R) (↑n' : R) 1) ((coeff 1 : (a : R⟦X⟧) → R) φ : R) *
      HPow.hPow (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) n'

Tactic:
lhs