awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V_1 : Type u_5
inst : AddCommMonoid Γ_1
inst_1 : PartialOrder Γ_1
inst_2 : IsOrderedCancelAddMonoid Γ_1
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ_1 Γ'
inst_5 : IsOrderedCancelVAdd Γ_1 Γ'
inst_6 : AddCommMonoid V_1
Γ : Type u_6
V : Type u_7
inst_7 : Ring R
inst_8 : IsDomain R
inst_9 : AddCommGroup V
inst_10 : AddCommMonoid Γ
inst_11 : LinearOrder Γ
inst_12 : IsOrderedCancelAddMonoid Γ
inst_13 : Module R V
inst_14 : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ¬Eq.{u_7 + 1} (α := V)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
        (x.order + order.{u_6, u_7} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)))
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) 0)
        (x.order + order.{u_6, u_7} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)))

Tactic:
simpa [coeff_smul_order_add_order]

Premises used: HahnModule.coeff_smul_order_add_order
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V_1 : Type u_5
inst : AddCommMonoid Γ_1
inst_1 : PartialOrder Γ_1
inst_2 : IsOrderedCancelAddMonoid Γ_1
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ_1 Γ'
inst_5 : IsOrderedCancelVAdd Γ_1 Γ'
inst_6 : AddCommMonoid V_1
Γ : Type u_6
V : Type u_7
inst_7 : Ring R
inst_8 : IsDomain R
inst_9 : AddCommGroup V
inst_10 : AddCommMonoid Γ
inst_11 : LinearOrder Γ
inst_12 : IsOrderedCancelAddMonoid Γ
inst_13 : Module R V
inst_14 : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ∃ (x_1 : Γ),
    ¬Eq.{u_7 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y)) x_1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) 0) x_1)

Tactic:
exact ⟨x.order + ((of R).symm y).order, by simpa [coeff_smul_order_add_order]⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
coeff :
  ∀ (x : Γ),
    (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
            ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
        x =
      HahnSeries.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⟦Γ⟧) =
    (single (a + b) : (a : R) → R⟦Γ⟧) (r * s)

Tactic:
ext x
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
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
⊢ (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
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
pos : coeff ((single a : (a : R) → R⟦Γ⟧) r) a * s = coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) (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:
rw [h, coeff_mul_single_add]

Premises used: HahnSeries.coeff_mul_single_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) a * s = coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) (a + b)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
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)) ⋯ ⋯ 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
⊢ (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:
rw [coeff_single_of_ne h, coeff_mul, sum_eq_zero]

Premises used: HahnSeries.coeff_mul, Finset.sum_eq_zero, HahnSeries.coeff_single_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
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
⊢ ∀
    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

Tactic:
simp_rw [mem_addAntidiagonal]

Premises used: Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ ¬a + b = a + b

Tactic:
rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h

Premises used: HahnSeries.eq_of_mem_support_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : ¬a + b = 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

Tactic:
(h rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : ¬a + b = 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

Tactic:
exact (h rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
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
⊢ HPow.hPow (α := R⟦Γ⟧) (β := ℕ) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) 0 =
    (single (HSMul.hSMul (α := ℕ) 0 a) : (a : R) → R⟦Γ⟧) (HPow.hPow (β := ℕ) r 0)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
a : Γ
r : R
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:
simp only [pow_zero, coeff_one, zero_smul, coeff_single]

Premises used: pow_zero, zero_smul, HahnSeries.coeff_one, HahnSeries.coeff_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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⟦Γ⟧)
succ₄ 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⟦Γ⟧)
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (n + 1) =
    (single ((n + 1) • a) : (a : R) → R⟦Γ⟧) (r ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, IH, single_mul_single, succ_nsmul]

Premises used: HahnSeries.single_mul_single, pow_succ, succ_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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)
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))
⊢ HPow.hPow (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) n = (single (n • a) : (a : R) → R⟦Γ⟧) (r ^ n)

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]

Premises used: HahnSeries.single_mul_single, pow_succ, pow_zero, zero_smul, HahnSeries.coeff_one, HahnSeries.coeff_single, succ_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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⟦Γ⟧)
rw₁ rw₂ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (x * y) : R⟦Γ⟧) ((single 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⟦Γ⟧)

Tactic:
rw [single_mul_single, zero_add]

Premises used: HahnSeries.single_mul_single, zero_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
coeff :
  ∀ (a : Γ),
    HahnSeries.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
⊢ (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⟦Γ⟧)

Tactic:
ext a
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
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
⊢ 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
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
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:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
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:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
⊢ Eq (α := R⟦Γ⟧) ((C : (a : R) → R⟦Γ⟧) 0) 0

Tactic:
C.map_zero

Premises used: RingHom.map_zero, HahnSeries.C
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
⊢ Eq (α := R⟦Γ⟧) ((C : (a : R) → R⟦Γ⟧) 1) 1

Tactic:
C.map_one

Premises used: RingHom.map_one, HahnSeries.C
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
coeff :
  ∀ (g : Γ),
    HahnSeries.coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g =
      HahnSeries.coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g
⊢ Eq (α := S⟦Γ⟧) (map ((C : (a : R) → R⟦Γ⟧) a) f) ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a))

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : ∀ (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

Tactic:
by_cases h : g = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
h : g = 0
⊢ coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
h : ¬g = 0
⊢ coeff (map ((C : (a : R) → R⟦Γ⟧) a) f) g = coeff ((C : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) a)) g

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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⟦Γ⟧)
⊢ ∀ (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

Premises used: funext_iff, HahnSeries.ext_iff
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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)
⊢ 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
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : r = s), r = s
⊢ r = s

Tactic:
rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h

Premises used: HahnSeries.coeff_single_same, HahnSeries.C_apply
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ Ne (α := R⟦Γ⟧) ((C : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
C_injective.ne_iff' C_zero |>.mpr h

Premises used: Iff.mpr, HahnSeries.C_injective, HahnSeries.C_zero, Function.Injective.ne_iff'
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : ∀ (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

Tactic:
by_cases h : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
pos₂ pos₃ : Eq.{u_1 + 1} (α := Γ) 0 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) ((C : (a : R) → R⟦Γ⟧) r)) 0

Tactic:
rw [h, C_zero, order_zero]

Premises used: HahnSeries.C_zero, HahnSeries.order_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

Tactic:
order_single h

Premises used: HahnSeries.order_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

Tactic:
exact order_single h

Premises used: HahnSeries.order_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
r : R
x : R⟦Γ⟧
⊢ HMul.hMul (α := R⟦Γ⟧) ((C : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = r • x

Tactic:
single_zero_mul_eq_smul

Premises used: HahnSeries.single_zero_mul_eq_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
coeff : ∀ (g : Γ'), (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
⊢ embDomain f (x * y) = embDomain f x * embDomain f y

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ'
pos :
  ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
    (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
neg :
  ∀ (hg : g ∉ Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
    (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g

Tactic:
by_cases hg : g ∈ Set.range f

Premises used: Set.range, DFunLike.coe