awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x y : R⟦Γ⟧
a : Γ
⊢ (x * y).coeff a = ∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a, x.coeff ij.1 * y.coeff ij.2

Tactic:
rfl

Premises used: Multiset.sum, Set.addAntidiagonal, Multiset.foldr, Set.Mem, setOf, Finset.sum, rfl
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), HahnSeries.coeff ((x * y).map f) x_1 = (HMul.hMul (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1
⊢ (x * y).map f = HMul.hMul (α := S⟦Γ⟧) (x.map f) (y.map f)

Tactic:
ext
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
coeff :
  Eq.{u_4 + 1} (α := S)
    (∑ x_2 ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff x_2.1) : S) ((f : (a : R) → S) (y.coeff x_2.2) : S))
    (∑ x_2 ∈ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff x_2.1) : S) ((f : (a : R) → S) (y.coeff x_2.2) : S))
⊢ HahnSeries.coeff ((x * y).map f) x_1 = (HMul.hMul (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1

Tactic:
simp only [map_coeff, coeff_mul, map_sum, map_mul]

Premises used: HahnSeries.coeff_mul, map_sum, map_mul, HahnSeries.map_coeff
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
⊢ Eq.{u_4 + 1} (α := S)
    (∑ x_2 ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff x_2.1) : S) ((f : (a : R) → S) (y.coeff x_2.2) : S))
    (∑ x_2 ∈ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff x_2.1) : S) ((f : (a : R) → S) (y.coeff x_2.2) : S))

Tactic:
Eq.symm (sum_subset (fun gh hgh => ?_) (fun gh hgh hz => ?_))

Premises used: Finset.sum_subset, Eq.symm
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
coeff :
  ∀ (gh : Γ × Γ) (hgh : gh ∈ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1),
    gh ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1
coeff₁ :
  ∀ (gh : Γ × Γ) (hgh : gh ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1)
    (hz : gh ∉ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0
⊢ Eq.{u_4 + 1} (α := S)
    (∑ x_2 ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff x_2.1) : S) ((f : (a : R) → S) (y.coeff x_2.2) : S))
    (∑ x_2 ∈ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff x_2.1) : S) ((f : (a : R) → S) (y.coeff x_2.2) : S))

Tactic:
refine Eq.symm (sum_subset (fun gh hgh => ?_) (fun gh hgh hz => ?_))

Premises used: Finset.sum_subset, Eq.symm
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1
coeff :
  ∀
    (hgh :
      ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) ∧
        ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S) ∧ gh.1 + gh.2 = x_1),
    ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0
⊢ gh ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1

Tactic:
simp_all only [mem_addAntidiagonal, mem_support, map_coeff, ne_eq, and_true]

Premises used: and_true, ne_eq, HahnSeries.map_coeff, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) ∧
    ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S) ∧ gh.1 + gh.2 = x_1
⊢ ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0

Tactic:
⟨fun h => hgh.1 (map_zero f ▸ congrArg f h), fun h => hgh.2.1 (map_zero f ▸ congrArg f h)⟩

Premises used: congrArg, Eq.rec, map_zero, And.right, And.left, And.intro, DFunLike.coe
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) ∧
    ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S) ∧ gh.1 + gh.2 = x_1
⊢ ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0

Tactic:
exact ⟨fun h => hgh.1 (map_zero f ▸ congrArg f h), fun h => hgh.2.1 (map_zero f ▸ congrArg f 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1
hz : gh ∉ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1
⊢ ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1

Tactic:
simp_all only [mem_addAntidiagonal, mem_support, ne_eq, map_coeff, and_true,
      not_and, not_not]

Premises used: and_true, Classical.not_not, ne_eq, HahnSeries.map_coeff, not_and, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1
hz : gh ∉ addAntidiagonal (s := support (x.map f)) (t := support (y.map f)) ⋯ ⋯ x_1
hgh₁ : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1
⊢ ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) →
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S)

Tactic:
simp_all only [mem_addAntidiagonal, mem_support, ne_eq, map_coeff, and_true,
      not_and, not_not]

Premises used: and_true, Classical.not_not, ne_eq, HahnSeries.map_coeff, not_and, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1
hz :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) →
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S)
pos :
  ∀ (h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S)),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0
neg :
  ∀ (h : ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S)),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0

Tactic:
by_cases h : f (x.coeff gh.1) = 0

Premises used: Prod.fst, HahnSeries.coeff, DFunLike.coe
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1
hz :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) →
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S)
h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0

Tactic:
mul_eq_zero_of_left h (f (y.coeff gh.2))

Premises used: mul_eq_zero_of_left, HahnSeries.coeff, Prod.snd, DFunLike.coe
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1
hz :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) →
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S)
h : Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0

Tactic:
exact mul_eq_zero_of_left h (f (y.coeff gh.2))

Premises used: mul_eq_zero_of_left, HahnSeries.coeff, Prod.snd, DFunLike.coe
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1
hz :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) →
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S)
h : ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0

Tactic:
mul_eq_zero_of_right (f (x.coeff gh.1)) (hz h)

Premises used: mul_eq_zero_of_right, Prod.fst, HahnSeries.coeff, DFunLike.coe
-- 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 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x_1 : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x_1
hz :
  ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S) →
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (y.coeff gh.2) : S) (0 : S)
h : ¬Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (x.coeff gh.1) : S) (0 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (x.coeff gh.1) : S) ((f : (a : R) → S) (y.coeff gh.2) : S) = 0

Tactic:
exact mul_eq_zero_of_right (f (x.coeff gh.1)) (hz h)

Premises used: mul_eq_zero_of_right, Prod.fst, HahnSeries.coeff, DFunLike.coe
-- 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
x y : R⟦Γ⟧
a : Γ
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
⊢ (x * y).coeff a = ∑ ij ∈ addAntidiagonal (s := s) (t := y.support) hs ⋯ a, x.coeff ij.1 * y.coeff ij.2

Tactic:
HahnModule.coeff_smul_left hs hxs

Premises used: Set.addAntidiagonal, Set.Mem, setOf, Finset.addAntidiagonal, HahnModule.coeff_smul_left
-- 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
x y : R⟦Γ⟧
a : Γ
s : Set Γ
hs : s.IsPWO
hys : y.support ⊆ s
⊢ (x * y).coeff a = ∑ ij ∈ addAntidiagonal (s := x.support) (t := s) ⋯ hs a, x.coeff ij.1 * y.coeff ij.2

Tactic:
HahnModule.coeff_smul_right hs hys

Premises used: Set.addAntidiagonal, setOf, Finset.addAntidiagonal, HahnModule.coeff_smul_right
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
simp :
  (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) x
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) (y + z) : HahnModule Γ R R)) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)) :
        R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)
⊢ x * (y + z) = x * y + x * z

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Premises used: HahnSeries.of_symm_smul_of_eq_mul
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) x
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) (y + z) : HahnModule Γ R R)) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)) :
        R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)

Tactic:
HahnModule.smul_add x y z

Premises used: HahnModule.smul_add, HahnModule
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) x
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) (y + z) : HahnModule Γ R R)) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)) :
        R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)

Tactic:
exact HahnModule.smul_add x y z

Premises used: HahnModule.smul_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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
simp :
  (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) (x + y)
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) y
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)
⊢ (x + y) * z = x * z + y * z

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Premises used: HahnSeries.of_symm_smul_of_eq_mul
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) (x + y)
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) y
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)

Tactic:
HahnModule.add_smul ?_

Premises used: HahnModule.add_smul, HahnModule
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
refine : ∀ (r s u : R), (r + s) • u = r • u + s • u
⊢ (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) (x + y)
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) x
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
          (HSMul.hSMul (β := HahnModule Γ R R) y
            ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) z : HahnModule Γ R R)) :
        R⟦Γ⟧)

Tactic:
refine HahnModule.add_smul ?_

Premises used: HahnModule.add_smul
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
simp : ∀ (r s u : R), (r + s) * u = r * u + s * u
⊢ ∀ (r s u : R), (r + s) • u = r • u + s • u

Tactic:
simp only [smul_eq_mul]

Premises used: smul_eq_mul
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ ∀ (r s u : R), (r + s) * u = r * u + s * u

Tactic:
add_mul

Premises used: add_mul
-- 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 : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ ∀ (r s u : R), (r + s) * u = r * u + s * u

Tactic:
exact add_mul

Premises used: add_mul
-- 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
r : R
x : R⟦Γ⟧
a b : Γ
rw :
  coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ R R) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) x : HahnModule Γ R R)))
      (b +ᵥ a) =
    r * x.coeff a
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).coeff (a + b) = r * x.coeff a

Tactic:
rw [← of_symm_smul_of_eq_mul, add_comm, ← vadd_eq_add]

Premises used: HahnSeries.of_symm_smul_of_eq_mul, add_comm, vadd_eq_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
r : R
x : R⟦Γ⟧
a b : Γ
⊢ coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ R R) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) x : HahnModule Γ R R)))
      (b +ᵥ a) =
    r * x.coeff a

Tactic:
HahnModule.coeff_single_smul_vadd

Premises used: HahnModule.coeff_single_smul_vadd
-- 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
r : R
x : R⟦Γ⟧
a b : Γ
⊢ coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ R R) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) x : HahnModule Γ R R)))
      (b +ᵥ a) =
    r * x.coeff a

Tactic:
exact HahnModule.coeff_single_smul_vadd

Premises used: HahnModule.coeff_single_smul_vadd
-- 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
r : R
x : R⟦Γ⟧
a b : Γ
pos : ∀ (hr : r = 0), (HMul.hMul (β := R⟦Γ⟧) x ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff (a + b) = x.coeff a * r
neg : ∀ (hr : ¬r = 0), (HMul.hMul (β := R⟦Γ⟧) x ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff (a + b) = x.coeff a * r
⊢ (HMul.hMul (β := R⟦Γ⟧) x ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff (a + b) = x.coeff a * r

Tactic:
by_cases hr : 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 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : r = 0
⊢ (HMul.hMul (β := R⟦Γ⟧) x ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff (a + b) = x.coeff a * r

Tactic:
simp [hr, coeff_mul]

Premises used: HahnSeries.coeff_mul
-- 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
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
neg :
  ∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2 =
    x.coeff a * r
⊢ (HMul.hMul (β := R⟦Γ⟧) x ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff (a + b) = x.coeff a * r

Tactic:
simp only [hr, coeff_mul, support_single_of_ne, Ne, not_false_iff]

Premises used: HahnSeries.coeff_mul, Ne, HahnSeries.support_single_of_ne, not_false_iff