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
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
pos :
  ∀ (hi : (i, j).1 = single s n),
    HMul.hMul (α := R) (β := R) (1 : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
⊢ HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have neg : ∀ (hi : ¬(i, j).1 = single s n),
  HMul.hMul (α := R) (β := R) (0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ HMul.hMul (α := R) (β := R) (1 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ False
have pos : (i, j) = (single s n, m - single s n)
Tactic: apply hne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (i, j) = (single s n, m - single s n)
have pos : i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1
Tactic: rw [← hij, ← hi, Prod.mk_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1
have pos : j = (i, j).1 + (i, j).2 - (i, j).1
Tactic: refine ⟨rfl, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ j = (i, j).1 + (i, j).2 - (i, j).1
have pos : ∀ (t : σ), Eq (α := ℕ) ((j : (a : σ) → ℕ) t : ℕ) (((i, j).1 + (i, j).2 - (i, j).1 : (a : σ) → ℕ) t : ℕ)
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ False
have pos : (single s n, m - single s n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
Tactic: apply hni
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ (single s n, m - single s n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
have pos : (single s n, m - single s n).1 + (single s n, m - single s n).2 = m
Tactic: rwa [mem_antidiagonal, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
pos : (single s n, m - single s n).1 + (single s n, m - single s n).2 = m
⊢ (single s n, m - single s n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
have pos₁ : (single s n, m - single s n).2 + (single s n, m - single s n).1 = m
Tactic: rwa [mem_antidiagonal, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have neg : ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
  HMul.hMul (α := R) (β := R)
      ((coeff x.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
Tactic: rw [h, coeff_mul, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
neg :
  ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have neg₁ : (m : (a : σ) → ℕ) s < n
Tactic: rw [h, coeff_mul, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have hij₁ : (i, j).1 + (i, j).2 = m
Tactic: rw [mem_antidiagonal] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have neg : HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
    ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
        (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
      R) =
  0
Tactic: rw [coeff_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
⊢ HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have pos : ∀ (hi : (i, j).1 = single s n),
  HMul.hMul (α := R) (β := R) (1 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
pos :
  ∀ (hi : (i, j).1 = single s n),
    HMul.hMul (α := R) (β := R) (1 : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
⊢ HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have neg : ∀ (hi : ¬(i, j).1 = single s n),
  HMul.hMul (α := R) (β := R) (0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ HMul.hMul (α := R) (β := R) (1 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ False
have pos : m - single s n + single s n = m
Tactic: apply H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ m - single s n + single s n = m
have pos : single s n + (i, j).2 - single s n + single s n = single s n + (i, j).2
Tactic: rw [← hij, hi]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
⊢ single s n + (i, j).2 - single s n + single s n = single s n + (i, j).2
have pos : ∀ (a : σ),
  Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
have pos : HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
    (⇑(single s n) : (a : σ) → ℕ) a =
  (single s n + (i, j).2 : (a : σ) → ℕ) a
Tactic: rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
pos :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    (single s n + (i, j).2 : (a : σ) → ℕ) a
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
have pos₁ : HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
    (⇑(single s n) : (a : σ) → ℕ) a =
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
Tactic: rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
pos :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    (single s n + (i, j).2 : (a : σ) → ℕ) a
pos₁ :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
have pos₂ : HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n : (a : σ) → ℕ) a : ℕ) =
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
Tactic: rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
pos :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    (single s n + (i, j).2 : (a : σ) → ℕ) a
pos₁ :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
have pos₃ : HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n : (a : σ) → ℕ) a : ℕ) =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
Tactic: rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
pos :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    (single s n + (i, j).2 : (a : σ) → ℕ) a
pos₁ :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
have pos₄ : HAdd.hAdd (α := ℕ) (β := ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
Tactic: rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
pos :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    (single s n + (i, j).2 : (a : σ) → ℕ) a
pos₁ :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
pos₄ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
have pos₅ : HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ) =
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
Tactic: rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
⊢ (m : (a : σ) → ℕ) s < n
have neg : ∀ (H : n ≤ (m : (a : σ) → ℕ) s), m - single s n + single s n = m
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : n ≤ (m : (a : σ) → ℕ) s
⊢ m - single s n + single s n = m
have neg : ∀ (t : σ), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
Tactic: ext t