awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
pos : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : k = m + n), a * b = a * b
neg : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
pos₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = a * b
neg₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
have pos₂ : ∀ (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = a * b
Tactic: split_ifs with h₁ h₂ h₃ h₃ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
pos : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : k = m + n), a * b = a * b
neg : ∀ (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
pos₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = a * b
neg₁ : ∀ (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
pos₂ : ∀ (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = a * b
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
have neg₂ : ∀ (h₁ : ¬n ≤ k) (h₂ : ¬k = m + n), Eq.{u_2 + 1} (α := R) 0 0
Tactic: split_ifs with h₁ h₂ h₃ h₃ h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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 = 0
have h₄ : ¬k = k
Tactic: rw [← h₂, tsub_add_cancel_of_le h₁] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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 = a * b
have h₄ : ¬m = m
Tactic: rw [h₃, add_tsub_cancel_right] at h₂
Cleared hypotheses: h₂, h₃
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b
have h₃ : ¬n ≤ m + n
Tactic: rw [h₂] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
m n : σ →₀ ℕ
a b : 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) =
    (monomial (m + n) : (a : R) → MvPowerSeries σ R) (a * b)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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)
⊢ 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)
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ 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)
have neg : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : k - n = m) (h₃ : ¬k = m + n), a * b = 0
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ 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)
have pos : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : k = m + n), 0 * b = 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ 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)
have neg₁ : ∀ (k : σ →₀ ℕ) (h₁ : n ≤ k) (h₂ : ¬k - n = m) (h₃ : ¬k = m + n), 0 * b = 0
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ 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)
have pos₁ : ∀ (k : σ →₀ ℕ) (h₁ : ¬n ≤ k) (h₂ : k = m + n), 0 = 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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)
⊢ a = b
have rw : (coeff 0 : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) = b
Tactic: rw [← coeff_zero_C a, h, coeff_zero_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ a = b
have rw₂ : (coeff 0 : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) b : MvPowerSeries σ R) = b
Tactic: rw [← coeff_zero_C a, h, coeff_zero_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ a = b
have rw₃ : b = b
Tactic: rw [← coeff_zero_C a, h, coeff_zero_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : IsEmpty σ
p : MvPowerSeries σ R
⊢ (C : (a : R) → MvPowerSeries σ R) (p 0) = p
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)
have hnc : ¬Eq (α := σ →₀ ℕ) 0 (single s 1)
Tactic: rw [coeff_X, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)
have rw : Eq.{u_2 + 1} (α := R) (if Eq (α := σ →₀ ℕ) 0 (single s 1) then 1 else 0) 0
Tactic: classical
  rw [coeff_X, if_neg]
  intro h
  exact one_ne_zero (single_eq_zero.mp h.symm)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: classical
  rw [coeff_X, if_neg]
  intro h
  exact one_ne_zero (single_eq_zero.mp h.symm)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (X s) : R) (0 : R)
have hnc : ¬Eq (α := σ →₀ ℕ) 0 (single s 1)
Tactic: classical
  rw [coeff_X, if_neg]
  intro h
  exact one_ne_zero (single_eq_zero.mp h.symm)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
have succ : HPow.hPow (α := MvPowerSeries σ R) (X s) n * X s = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
Tactic: rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
have 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
Tactic: rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
have 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
Tactic: rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
have 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
Tactic: rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
have 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)
Tactic: rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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)
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) (n + 1) = (monomial (single s (n + 1)) : (a : R) → MvPowerSeries σ R) 1
have 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)
Tactic: rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n = (monomial (single s n) : (a : R) → MvPowerSeries σ R) 1
have zero : HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (X s) 0 = (monomial (single s 0) : (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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n = (monomial (single s n) : (a : R) → MvPowerSeries σ R) 1
have 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
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : DecidableEq σ
m : σ →₀ ℕ
s : σ
n : ℕ
⊢ 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)
have 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)
Tactic: rw [X_pow_eq s n, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_2 + 1} (α := R) (if m = single s n then 1 else 0) (if m = single s n then 1 else 0)
Tactic: rw [X_pow_eq s n, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * X s) : R) (0 : R)
have this : ¬LE.le (α := σ →₀ ℕ) (single s 1) 0
Tactic: have : ¬single s 1 ≤ 0 := fun h => by simpa using h s