awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : k = m + n
⊢ a * b = a * b

Tactic:
try rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : ¬k = m + n
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : ¬k = m + n
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
try rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ ¬k = k

Tactic:
rw [← h₂, tsub_add_cancel_of_le h₁] at h₃

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k
⊢ a * b = 0

Tactic:
(h₃ rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k
⊢ a * b = 0

Tactic:
exact (h₃ rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
⊢ ¬m = m

Tactic:
rw [h₃, add_tsub_cancel_right] at h₂

Premises used: add_tsub_cancel_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
h₄ : ¬m = m
⊢ k = m + n

Tactic:
rw [h₃, add_tsub_cancel_right] at h₂

Premises used: add_tsub_cancel_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬m = m
h₃ : k = m + n
⊢ 0 * b = a * b

Tactic:
(h₂ rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬m = m
h₃ : k = m + n
⊢ 0 * b = a * b

Tactic:
exact (h₂ rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0

Tactic:
zero_mul b

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0

Tactic:
exact zero_mul b

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ ¬n ≤ m + n

Tactic:
rw [h₂] at h₁
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
h₃ : ¬n ≤ m + n
⊢ k = m + n

Tactic:
rw [h₂] at h₁
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ m + n
h₂ : k = m + n
⊢ 0 = a * b

Tactic:
(h₁ <| le_add_left le_rfl).elim

Premises used: le_rfl, False.elim, le_add_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ m + n
h₂ : k = m + n
⊢ 0 = a * b

Tactic:
exact (h₁ <| le_add_left le_rfl).elim

Premises used: le_rfl, False.elim, le_add_left
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
h :
  ∀ (k : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff k : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
            ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
            ((monomial n : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R)) :
        R)
      ((coeff k : (a : MvPowerSeries σ R) → R)
          ((monomial (m + n) : (a : R) → MvPowerSeries σ R) (a * b) : MvPowerSeries σ R) :
        R)
h₁ : ∀ (k : σ →₀ ℕ), (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
neg : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
pos : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = a * b
neg₁ : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
pos₁ : ∀ (k : σ →₀ ℕ) (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = a * b
pos₂ : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = a * b
neg₂ : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
pos₃ : ∀ (k : σ →₀ ℕ) (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = a * b
neg₃ : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
pos₄ pos₅ : ∀ (k : σ →₀ ℕ) (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = a * b
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
      ((monomial n : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R) =
    (monomial (m + n) : (a : R) → MvPowerSeries σ R) (a * b)

Tactic:
classical
  ext k
  simp only [coeff_mul_monomial, coeff_monomial]
  split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl
  · rw [← h₂, tsub_add_cancel_of_le h₁] at h₃
    exact (h₃ rfl).elim
  · rw [h₃, add_tsub_cancel_right] at h₂
    exact (h₂ rfl).elim
  · exact zero_mul b
  · rw [h₂] at h₁
    exact (h₁ <| le_add_left le_rfl).elim

Premises used: MvPowerSeries.coeff_mul_monomial, MulZeroClass.zero_mul, MvPowerSeries.coeff_monomial, add_tsub_cancel_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
a b : R
⊢ Eq (α := MvPowerSeries σ R) (AddHom.toFun (LinearMap.toAddHom (monomial 0)) (a * b))
    ((monomial (HAdd.hAdd (α := σ →₀ ℕ) 0 0) : (a : R) → MvPowerSeries σ R) (a * b))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq (α := (a : R) → MvPowerSeries σ R) (⇑(monomial 0) : (a : R) → MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R)

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
a : R
⊢ Eq (α := MvPowerSeries σ R) ((monomial 0 : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) =
    if n = 0 then a else 0

Tactic:
coeff_monomial _ _ _

Premises used: Function.update, Pi.single, dite, MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
a : R
⊢ (coeff 0 : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = a

Tactic:
coeff_monomial_same 0 a

Premises used: Function.update, MvPowerSeries.coeff_monomial_same, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, OfNat.ofNat, Multiset.attach
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
a b : R
h :
  Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
    ((C : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R)
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = b
rw₁ : Type u_1
rw₂ : (coeff 0 : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R) = b
rw₃ rw₄ : b = b
⊢ a = b

Tactic:
rw [← coeff_zero_C a, h, coeff_zero_C]

Premises used: MvPowerSeries.coeff_zero_C
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : IsEmpty σ
p : MvPowerSeries σ R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) (p 0) : MvPowerSeries σ R) : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ (C : (a : R) → MvPowerSeries σ R) (p 0) = p

Tactic:
ext n
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : IsEmpty σ
p : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff n : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) (p 0) : MvPowerSeries σ R) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) p : R)

Tactic:
simpa [coeff_C, Subsingleton.eq_zero n] using coeff_apply _ _

Premises used: MvPowerSeries.coeff_apply, MvPowerSeries.coeff_C, Subsingleton.eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
r s : R
⊢ Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R) ↔
    r = s

Tactic:
(C_injective).eq_iff

Premises used: Function.Injective.eq_iff, MvPowerSeries.C_injective
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (X s) : R) (if n = single s 1 then 1 else 0 : R)

Tactic:
coeff_monomial _ _ _

Premises used: MvPowerSeries.X, MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
s t : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff (single t 1) : (a : MvPowerSeries σ R) → R) (X s) : R) (if t = s then 1 else 0 : R)

Tactic:
simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

Premises used: MvPowerSeries.coeff_X, Finsupp.single_left_inj, one_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff (single s 1) : (a : MvPowerSeries σ R) → R) (X s) : R) (1 : R)

Tactic:
coeff_monomial_same _ _

Premises used: MvPowerSeries.coeff_monomial_same, MvPowerSeries.X
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
hnc : ¬Eq (α := σ →₀ ℕ) 0 (single s 1)
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)

Tactic:
rw [coeff_X, if_neg]

Premises used: MvPowerSeries.coeff_X, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
h : Eq (α := σ →₀ ℕ) 0 (single s 1)
⊢ False

Tactic:
one_ne_zero (single_eq_zero.mp h.symm)

Premises used: Finsupp.single_eq_zero, Iff.mp, one_ne_zero, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
h : Eq (α := σ →₀ ℕ) 0 (single s 1)
⊢ False

Tactic:
exact one_ne_zero (single_eq_zero.mp h.symm)

Premises used: Finsupp.single_eq_zero, Iff.mp, one_ne_zero, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
rw : Eq.{u_2 + 1} (α := R) (if Eq (α := σ →₀ ℕ) 0 (single s 1) then 1 else 0) 0
rw₁ : Eq.{u_2 + 1} (α := R) 0 0
hnc : ¬Eq (α := σ →₀ ℕ) 0 (single s 1)
rw₂ : Eq.{u_2 + 1} (α := R) 0 0
hnc₁ hnc₂ : ¬Eq (α := σ →₀ ℕ) 0 (single s 1)
hnc₃ : ∀ (h : Eq (α := σ →₀ ℕ) 0 (single s 1)), False
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)

Tactic:
classical
  rw [coeff_X, if_neg]
  intro h
  exact one_ne_zero (single_eq_zero.mp h.symm)

Premises used: MvPowerSeries.coeff_X, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ Commute φ (X s)

Tactic:
φ.commute_monomial.mpr fun _m => Commute.one_right _

Premises used: Iff.mpr, MvPowerSeries.X, MvPowerSeries.coeff, DFunLike.coe, Commute.one_right, MvPowerSeries.commute_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ X s * φ = φ * X s

Tactic:
φ.commute_X s |>.symm.eq

Premises used: MvPowerSeries.commute_X, Commute.symm, Commute.eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
n : ℕ
⊢ Commute φ (HPow.hPow (α := MvPowerSeries σ R) (X s) n)

Tactic:
φ.commute_X s |>.pow_right _

Premises used: Commute.pow_right, MvPowerSeries.commute_X
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
n : ℕ
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n * φ = φ * HPow.hPow (α := MvPowerSeries σ R) (X s) n

Tactic:
φ.commute_X_pow s n |>.symm.eq

Premises used: MvPowerSeries.commute_X_pow, Commute.symm, Commute.eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
⊢ Eq (α := MvPowerSeries σ R) (X s) ((monomial (single s 1) : (a : R) → MvPowerSeries σ R) 1)

Tactic:
rfl

Premises used: MvPowerSeries.X, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
⊢ HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X s) 0 = (monomial (single s 0) : (a : R) → MvPowerSeries σ R) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
ih : HPow.hPow (α := MvPowerSeries σ R) (X s) n = (monomial (single s n) : (a : R) → MvPowerSeries σ R) 1
succ : HPow.hPow (α := MvPowerSeries σ R) (X s) n * X s = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
succ₁ :
  HMul.hMul (α := MvPowerSeries σ R) ((monomial (single s n) : (a : R) → MvPowerSeries σ R) 1) (X s) =
    (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
succ₂ :
  HMul.hMul (α := MvPowerSeries σ R) ((monomial (single s n) : (a : R) → MvPowerSeries σ R) 1) (X s) =
    (monomial (HAdd.hAdd (α := σ →₀ ℕ) (single s n) (single s 1)) : (a : R) → MvPowerSeries σ R) 1
succ₃ :
  HMul.hMul (α := MvPowerSeries σ R) ((monomial (single s n) : (a : R) → MvPowerSeries σ R) 1)
      ((monomial (single s 1) : (a : R) → MvPowerSeries σ R) 1) =
    (monomial (HAdd.hAdd (α := σ →₀ ℕ) (single s n) (single s 1)) : (a : R) → MvPowerSeries σ R) 1
succ₄ :
  Eq (α := MvPowerSeries σ R)
    ((monomial (HAdd.hAdd (α := σ →₀ ℕ) (single s n) (single s 1)) : (a : R) → MvPowerSeries σ R)
        (HMul.hMul (α := R) 1 1) :
      MvPowerSeries σ R)
    ((monomial (HAdd.hAdd (α := σ →₀ ℕ) (single s n) (single s 1)) : (a : R) → MvPowerSeries σ R) 1 : MvPowerSeries σ R)
succ₅ succ₆ :
  Eq (α := MvPowerSeries σ R)
    ((monomial (HAdd.hAdd (α := σ →₀ ℕ) (single s n) (single s 1)) : (a : R) → MvPowerSeries σ R) 1)
    ((monomial (HAdd.hAdd (α := σ →₀ ℕ) (single s n) (single s 1)) : (a : R) → MvPowerSeries σ R) 1)
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1

Tactic:
rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

Premises used: pow_succ, MvPowerSeries.X, Finsupp.single_add, MvPowerSeries.monomial_mul_monomial, one_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
zero : HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X s) 0 = (monomial (single s 0) : (a : R) → MvPowerSeries σ R) 1
succ :
  ∀ (n : ℕ) (ih : HPow.hPow (α := MvPowerSeries σ R) (X s) n = (monomial (single s n) : (a : R) → MvPowerSeries σ R) 1),
    HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n = (monomial (single s n) : (a : R) → MvPowerSeries σ R) 1

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

Premises used: pow_succ, MvPowerSeries.X, Finsupp.single_add, MvPowerSeries.monomial_mul_monomial, one_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
n : ℕ
rw :
  Eq.{u_2 + 1} (α := R)
    ((coeff m : (a : MvPowerSeries σ R) → R) ((monomial (single s n) : (a : R) → MvPowerSeries σ R) 1) : R)
    (if m = single s n then 1 else 0 : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) (if m = single s n then 1 else 0) (if m = single s n then 1 else 0)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
    (if m = single s n then 1 else 0 : R)

Tactic:
rw [X_pow_eq s n, coeff_monomial]

Premises used: MvPowerSeries.X_pow_eq, MvPowerSeries.coeff_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) φ ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)) =
    HMul.hMul (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) a

Tactic:
simpa using coeff_add_mul_monomial n 0 φ a

Premises used: MvPowerSeries.coeff_add_mul_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) φ) =
    HMul.hMul (β := R) a ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
simpa using coeff_add_monomial_mul 0 n φ a

Premises used: OfNat.ofNat, MvPowerSeries.coeff_add_monomial_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
h : LE.le (α := σ →₀ ℕ) (single s 1) 0
⊢ False

Tactic:
simpa using h s
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ ¬LE.le (α := σ →₀ ℕ) (single s 1) 0

Tactic:
have : ¬single s 1 ≤ 0 := fun h => by simpa using h s
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
this : ¬LE.le (α := σ →₀ ℕ) (single s 1) 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * X s) : R) (0 : R)

Tactic:
simp only [X, coeff_mul_monomial, if_neg this]

Premises used: MvPowerSeries.coeff_mul_monomial, MvPowerSeries.X, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
rw : Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * X s) : R) (0 : R)
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s * φ) : R) (0 : R)

Tactic:
rw [← (φ.commute_X s).eq, coeff_zero_mul_X]

Premises used: MvPowerSeries.commute_X, MvPowerSeries.coeff_zero_mul_X, Commute.eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ ψ : MvPowerSeries σ R
⊢ (coeff 0 : (a : MvPowerSeries σ R) → R) (φ * ψ) =
    HMul.hMul (α := R) (β := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff 0 : (a : MvPowerSeries σ R) → R) ψ : R)

Tactic:
simp [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ ψ : MvPowerSeries σ R
⊢ (coeff 0 : (a : MvPowerSeries σ R) → R) (φ * ψ) =
    HMul.hMul (α := R) (β := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff 0 : (a : MvPowerSeries σ R) → R) ψ : R)

Tactic:
classical simp [coeff_mul]

Premises used: MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq (α := (a : MvPowerSeries σ R) → R) (⇑(coeff 0) : (a : MvPowerSeries σ R) → R)
    (⇑constantCoeff : (a : MvPowerSeries σ R) → R)

Tactic:
rfl

Premises used: MvPowerSeries, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) φ : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
a : R
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = a

Tactic:
rfl

Premises used: Function.update, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq (α := R →+* R) (RingHom.comp (β := MvPowerSeries σ R) constantCoeff C) (RingHom.id R)

Tactic:
rfl

Premises used: Function.update, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) 0 : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) 1 : R) (1 : R)

Tactic:
rfl

Premises used: Function.update, Multiset.zero, Pi.single, dite, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)

Tactic:
coeff_zero_X s

Premises used: Function.update, Multiset.zero, Pi.single, dite, MvPowerSeries.X, Multiset.ofList, MvPowerSeries.coeff_zero_X
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
S : Type u_3
inst_1 : Semiring S
inst_2 : Module R S
φ : MvPowerSeries σ S
a : R
⊢ (constantCoeff : (a : MvPowerSeries σ S) → S) (a • φ) =
    HSMul.hSMul (β := S) a ((constantCoeff : (a : MvPowerSeries σ S) → S) φ : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
h : IsUnit φ
⊢ IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
h.map _

Premises used: IsUnit.map
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : σ →₀ ℕ
a : R
⊢ (coeff n : (a : MvPowerSeries σ R) → R) (a • f) = HMul.hMul (β := R) a ((coeff n : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
a : R
h :
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (a • f) : R)
      ((coeff n : (a : MvPowerSeries σ R) → R)
          (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) f) :
        R)
⊢ a • f = HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) f

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (a • f) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) f) :
      R)

Tactic:
simp