awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
pos :
  ∀ (h : x = a + b),
    (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
            ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
        x =
      coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
⊢ (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
have neg : ∀ (h : ¬x = a + b),
  (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
Tactic: by_cases h : x = a + b
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
have pos : coeff ((single a : (a : R) → R⟦Γ⟧) r) a * s = coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) (a + b)
Tactic: rw [h, coeff_mul_single_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
have neg : ∀
  x_1 ∈
    addAntidiagonal (s := support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) (t :=
      support.{u_1, u_3} (R := R) ((single b : (a : R) → R⟦Γ⟧) s)) sorry sorry x,
  HMul.hMul (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) x_1.1) (coeff ((single b : (a : R) → R⟦Γ⟧) s) x_1.2) = 0
Tactic: rw [coeff_single_of_ne h, coeff_mul, sum_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀
    x_1 ∈
      addAntidiagonal (s := support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) (t :=
        support.{u_1, u_3} (R := R) ((single b : (a : R) → R⟦Γ⟧) s)) ⋯ ⋯ x,
    HMul.hMul (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) x_1.1) (coeff ((single b : (a : R) → R⟦Γ⟧) s) x_1.2) = 0
have neg : ∀ (x_1 : Γ × Γ),
  Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) x_1.1 ∧
      Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((single b : (a : R) → R⟦Γ⟧) s)) x_1.2 ∧
        x_1.1 + x_1.2 = x →
    HMul.hMul (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) x_1.1) (coeff ((single b : (a : R) → R⟦Γ⟧) s) x_1.2) = 0
Tactic: simp_rw [mem_addAntidiagonal]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) (y, z).1
hz : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((single b : (a : R) → R⟦Γ⟧) s)) (y, z).2
h : ¬(y, z).1 + (y, z).2 = a + b
⊢ HMul.hMul (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) (y, z).1) (coeff ((single b : (a : R) → R⟦Γ⟧) s) (y, z).2) =
    0
have h₁ : ¬a + b = a + b
Tactic: rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
⊢ HPow.hPow (α := R⟦Γ⟧) (β := ℕ) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) 0 =
    (single (HSMul.hSMul (α := ℕ) 0 a) : (a : R) → R⟦Γ⟧) (HPow.hPow (β := ℕ) r 0)
have zero : ∀ (x : Γ),
  (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) 0).coeff x =
    coeff ((single (HSMul.hSMul (α := ℕ) 0 a) : (a : R) → R⟦Γ⟧) (HPow.hPow (β := ℕ) r 0)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
n : ℕ
IH : HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
have succ : HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
    ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
  (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
Tactic: rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
n : ℕ
IH : HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
succ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
have succ₁ : HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
    ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
  (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
Tactic: rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
n : ℕ
IH : HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
succ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
succ₁ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
have succ₂ : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n) : R⟦Γ⟧)
    ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
  (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
Tactic: rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
n : ℕ
IH : HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
succ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
succ₁ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
succ₂ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n) : R⟦Γ⟧)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
have succ₃ : Eq (α := R⟦Γ⟧) ((single (n • a + a) : (a : R) → R⟦Γ⟧) (r ^ n * r) : R⟦Γ⟧)
  ((single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r) : R⟦Γ⟧)
Tactic: rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
n : ℕ
IH : HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
succ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
succ₁ :
  HMul.hMul (β := R⟦Γ⟧) (HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
succ₂ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n) : R⟦Γ⟧)
      ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r)
succ₃ :
  Eq (α := R⟦Γ⟧) ((single (n • a + a) : (a : R) → R⟦Γ⟧) (r ^ n * r) : R⟦Γ⟧)
    ((single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ n * r) : R⟦Γ⟧)
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
have succ₄ : Eq (α := R⟦Γ⟧) ((single (n • a + a) : (a : R) → R⟦Γ⟧) (r ^ n * r) : R⟦Γ⟧)
  ((single (n • a + a) : (a : R) → R⟦Γ⟧) (r ^ n * r) : R⟦Γ⟧)
Tactic: rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
n : ℕ
r : R
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
have zero : HPow.hPow (α := R⟦Γ⟧) (β := ℕ) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) 0 =
  (single (HSMul.hSMul (α := ℕ) 0 a) : (a : R) → R⟦Γ⟧) (HPow.hPow (β := ℕ) r 0)
Tactic: induction n with
  | zero => ext; simp only [pow_zero, coeff_one, zero_smul, coeff_single]
  | succ n IH => rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
n : ℕ
r : R
zero :
  HPow.hPow (α := R⟦Γ⟧) (β := ℕ) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) 0 =
    (single (HSMul.hSMul (α := ℕ) 0 a) : (a : R) → R⟦Γ⟧) (HPow.hPow (β := ℕ) r 0)
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)
have succ : ∀ (n : ℕ)
  (IH : HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)),
  HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))
Tactic: induction n with
  | zero => ext; simp only [pow_zero, coeff_one, zero_smul, coeff_single]
  | succ n IH => rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x y : R
⊢ (single 0 : (a : R) → R⟦Γ⟧) (x * y) =
    HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)
have rw : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧)
  ((single (HAdd.hAdd (α := Γ) 0 0) : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧)
Tactic: rw [single_mul_single, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x y : R
rw :
  Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧)
    ((single (HAdd.hAdd (α := Γ) 0 0) : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧)
⊢ (single 0 : (a : R) → R⟦Γ⟧) (x * y) =
    HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)
have rw₁ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧)
Tactic: rw [single_mul_single, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x y : R
⊢ (single 0 : (a : R) → R⟦Γ⟧) (x + y) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)
have coeff : ∀ (a : Γ),
  coeff ((single 0 : (a : R) → R⟦Γ⟧) (x + y)) a =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      a
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x y : R
a : Γ
⊢ coeff ((single 0 : (a : R) → R⟦Γ⟧) (x + y)) a =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      a
have pos : ∀ (h : a = 0),
  coeff ((single 0 : (a : R) → R⟦Γ⟧) (x + y)) a =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x y : R
a : Γ
pos :
  ∀ (h : a = 0),
    coeff ((single 0 : (a : R) → R⟦Γ⟧) (x + y)) a =
      (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧)
            ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
        a
⊢ coeff ((single 0 : (a : R) → R⟦Γ⟧) (x + y)) a =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      a
have neg : ∀ (h : ¬a = 0),
  coeff ((single 0 : (a : R) → R⟦Γ⟧) (x + y)) a =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((single 0 : (a : R) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
a : R
f : R →+* S
⊢ Eq (α := S⟦Γ⟧) (map ((C : (a : R) → R⟦Γ⟧) a) f) ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a))
have coeff : ∀ (g : Γ), coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
⊢ coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
have pos : ∀ (h : g = 0), coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
Tactic: by_cases h : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
inst_4 : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
pos : ∀ (h : g = 0), coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
⊢ coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
have neg : ∀ (h : ¬g = 0), coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
Tactic: by_cases h : g = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r s : R
rs : Eq (α := R⟦Γ⟧) ((C : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((C : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
⊢ r = s
have rs₁ : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (coeff ((C : (a : R) → R⟦Γ⟧) r) x) (coeff ((C : (a : R) → R⟦Γ⟧) s) x)
Tactic: rw [HahnSeries.ext_iff, funext_iff] at rs
Cleared hypotheses: rs
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (coeff ((C : (a : R) → R⟦Γ⟧) r) x) (coeff ((C : (a : R) → R⟦Γ⟧) s) x)
⊢ r = s
have h : Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) r) 0)
  (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)
Tactic: have h := rs 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (coeff ((C : (a : R) → R⟦Γ⟧) r) x) (coeff ((C : (a : R) → R⟦Γ⟧) s) x)
h :
  Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) r) 0)
    (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)
⊢ r = s
have rwa : ∀
  (h :
    Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((single 0 : (a : R) → R⟦Γ⟧) r) 0)
      (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)),
  r = s
Tactic: rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (coeff ((C : (a : R) → R⟦Γ⟧) r) x) (coeff ((C : (a : R) → R⟦Γ⟧) s) x)
h :
  Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) r) 0)
    (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)
rwa :
  ∀
    (h :
      Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((single 0 : (a : R) → R⟦Γ⟧) r) 0)
        (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)),
    r = s
⊢ r = s
have rwa₁ : ∀ (h : r = coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0), r = s
Tactic: rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (coeff ((C : (a : R) → R⟦Γ⟧) r) x) (coeff ((C : (a : R) → R⟦Γ⟧) s) x)
h :
  Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) r) 0)
    (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)
rwa :
  ∀
    (h :
      Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((single 0 : (a : R) → R⟦Γ⟧) r) 0)
        (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)),
    r = s
rwa₁ : ∀ (h : r = coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0), r = s
⊢ r = s
have rwa₂ : ∀ (h : r = coeff.{u_1, u_3} (Γ := Γ) ((single 0 : (a : R) → R⟦Γ⟧) s) 0), r = s
Tactic: rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (coeff ((C : (a : R) → R⟦Γ⟧) r) x) (coeff ((C : (a : R) → R⟦Γ⟧) s) x)
h :
  Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) r) 0)
    (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)
rwa :
  ∀
    (h :
      Eq.{u_3 + 1} (α := R) (coeff.{u_1, u_3} (Γ := Γ) ((single 0 : (a : R) → R⟦Γ⟧) r) 0)
        (coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0)),
    r = s
rwa₁ : ∀ (h : r = coeff.{u_1, u_3} (Γ := Γ) ((C : (a : R) → R⟦Γ⟧) s) 0), r = s
rwa₂ : ∀ (h : r = coeff.{u_1, u_3} (Γ := Γ) ((single 0 : (a : R) → R⟦Γ⟧) s) 0), r = s
⊢ r = s
have rwa₃ : ∀ (h : r = s), r = s
Tactic: rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r : R
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
have pos : ∀ (h : r = 0), Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r : R
pos : ∀ (h : r = 0), Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
have neg : ∀ (h : ¬r = 0), Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r : R
h : r = 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
have pos : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) 0)) 0
Tactic: rw [h, C_zero, order_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r : R
h : r = 0
pos : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) 0)) 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
have pos₁ : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 0) 0
Tactic: rw [h, C_zero, order_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
r : R
h : r = 0
pos : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) 0)) 0
pos₁ : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 0) 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0
have pos₂ : Eq.{u_1 + 1} (α := Γ) 0 0
Tactic: rw [h, C_zero, order_zero]