awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
h : ¬i < c
⊢ coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y)) i =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      i

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
x y : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (x + y).coeff x_1 = (y + x).coeff x_1
⊢ x + y = y + x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
x y : R⟦Γ⟧
x_1 : Γ
⊢ (x + y).coeff x_1 = (y + x).coeff x_1

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s_1 : Finset α
x : α → R⟦Γ⟧
g : Γ
i : α
s : Finset α
his : i ∉ s
hsum : Eq.{u_3 + 1} (α := R) (coeff (∑ i ∈ s, x i) g) (∑ i ∈ s, (x i).coeff g)
rw : (x i + ∑ x_1 ∈ s, x x_1).coeff g = ∑ i ∈ cons i s his, (x i).coeff g
rw₁ : (x i + ∑ x_1 ∈ s, x x_1).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g
rw₂ : (x i).coeff g + coeff (∑ x_1 ∈ s, x x_1) g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g
rw₃ rw₄ : (x i).coeff g + ∑ i ∈ s, (x i).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g
⊢ Eq.{u_3 + 1} (α := R) (coeff (∑ i ∈ cons i s his, x i) g) (∑ i ∈ cons i s his, (x i).coeff g)

Tactic:
rw [sum_cons, sum_cons, coeff_add, hsum]

Premises used: Finset.sum_cons, HahnSeries.coeff_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : NegZeroClass R
x : R⟦Γ⟧
⊢ (-x).support ⊆ x.support

Tactic:
support_map_subset ..

Premises used: HahnSeries.support_map_subset
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : NegZeroClass R
x : R⟦Γ⟧
⊢ (-x).coeff = -x.coeff

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : NegZeroClass R
x : R⟦Γ⟧
a : Γ
⊢ (-x).coeff a = -x.coeff a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
⊢ (x - y).support ⊆ x.support ∪ y.support

Tactic:
Function.support_sub ..

Premises used: HahnSeries.support, Function.support_sub
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
⊢ (x - y).coeff = x.coeff - y.coeff

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
a : Γ
⊢ (x - y).coeff a = x.coeff a - y.coeff a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
a : Γ
r s : R
⊢ (single a : (a : R) → R⟦Γ⟧) (r - s) =
    HSub.hSub (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)

Tactic:
map_sub (single.addMonoidHom a) _ _

Premises used: map_sub, HahnSeries.single.addMonoidHom
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
a : Γ
r : R
⊢ Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) (-r) : R⟦Γ⟧) (-(single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)

Tactic:
map_neg (single.addMonoidHom a) _

Premises used: map_neg, HahnSeries.single.addMonoidHom
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
h : ∀ (x_1 : Γ), x_1 ∈ (-x).support ↔ x_1 ∈ x.support
⊢ (-x).support = x.support

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
x_1 : Γ
⊢ x_1 ∈ (-x).support ↔ x_1 ∈ x.support

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : AddGroup S
f : R →+ S
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), HahnSeries.coeff ((-x).map f) x_1 = HahnSeries.coeff (-x.map f) x_1
⊢ Eq (α := S⟦Γ⟧) ((-x).map f) (-x.map f)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : AddGroup S
f : R →+ S
x : R⟦Γ⟧
x_1 : Γ
⊢ coeff ((-x).map f) x_1 = coeff (-x.map f) x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
⊢ (-x).orderTop = x.orderTop

Tactic:
simp only [orderTop, support_neg, neg_eq_zero]

Premises used: HahnSeries.orderTop, neg_eq_zero, HahnSeries.support_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
⊢ (-x).orderTop = x.orderTop

Tactic:
classical simp only [orderTop, support_neg, neg_eq_zero]

Premises used: HahnSeries.orderTop, neg_eq_zero, HahnSeries.support_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : Zero Γ
f : R⟦Γ⟧
pos : ∀ (hf : f = 0), (-f).order = f.order
neg : ∀ (hf : ¬f = 0), (-f).order = f.order
⊢ (-f).order = f.order

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : Zero Γ
f : R⟦Γ⟧
hf : f = 0
⊢ (-f).order = f.order

Tactic:
simp only [hf, neg_zero]

Premises used: neg_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : Zero Γ
f : R⟦Γ⟧
hf : ¬f = 0
⊢ (-f).order = f.order

Tactic:
simp only [order, support_neg, neg_eq_zero]

Premises used: HahnSeries.order, neg_eq_zero, HahnSeries.support_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : Zero Γ
f : R⟦Γ⟧
pos : ∀ (hf : f = 0), (-f).order = f.order
neg neg₁ : ∀ (hf : ¬f = 0), (-f).order = f.order
⊢ (-f).order = f.order

Tactic:
classical
  by_cases hf : f = 0
  · simp only [hf, neg_zero]
  simp only [order, support_neg, neg_eq_zero]

Premises used: HahnSeries.order, neg_eq_zero, HahnSeries.support_neg, neg_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
inl : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) (-0)) (-leadingCoeff.{u_1, u_3} (Γ := Γ) 0)
inr : ∀ (hx : x ≠ 0), (-x).leadingCoeff = -x.leadingCoeff
⊢ (-x).leadingCoeff = -x.leadingCoeff

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
⊢ Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) (-0)) (-leadingCoeff.{u_1, u_3} (Γ := Γ) 0)

Tactic:
simp [leadingCoeff_of_ne_zero, *]

Premises used: HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (-x).leadingCoeff = -x.leadingCoeff

Tactic:
simp [leadingCoeff_of_ne_zero, *]

Premises used: HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), HahnSeries.coeff ((x - y).map f) x_1 = (HSub.hSub (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1
⊢ (x - y).map f = HSub.hSub (α := S⟦Γ⟧) (x.map f) (y.map f)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
x_1 : Γ
⊢ coeff ((x - y).map f) x_1 = (HSub.hSub (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
rw : min x.orderTop (-y).orderTop ≤ (x + -y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x - y).orderTop

Tactic:
rw [sub_eq_add_neg, ← orderTop_neg (x := y)]

Premises used: sub_eq_add_neg, HahnSeries.orderTop_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop (-y).orderTop ≤ (x + -y).orderTop

Tactic:
min_orderTop_le_orderTop_add

Premises used: HahnSeries.min_orderTop_le_orderTop_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop (-y).orderTop ≤ (x + -y).orderTop

Tactic:
exact min_orderTop_le_orderTop_add

Premises used: HahnSeries.min_orderTop_le_orderTop_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
rw : (x + -y).orderTop = x.orderTop
⊢ (x - y).orderTop = x.orderTop

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ x.orderTop < (-y).orderTop

Tactic:
rw [← orderTop_neg (x := y)] at hxy

Premises used: HahnSeries.orderTop_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).orderTop = x.orderTop

Tactic:
orderTop_add_eq_left hxy

Premises used: HahnSeries.orderTop_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).orderTop = x.orderTop

Tactic:
exact orderTop_add_eq_left hxy

Premises used: HahnSeries.orderTop_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
rw : (x + -y).leadingCoeff = x.leadingCoeff
⊢ (x - y).leadingCoeff = x.leadingCoeff

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Tactic:
leadingCoeff_add_eq_left hxy

Premises used: HahnSeries.leadingCoeff_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Tactic:
exact leadingCoeff_add_eq_left hxy

Premises used: HahnSeries.leadingCoeff_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ (x - y).orderTop ≠ (↑g : WithTop Γ)

Tactic:
orderTop_ne_of_coeff_eq_zero ?_

Premises used: HahnSeries.orderTop_ne_of_coeff_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
refine : (x - y).coeff g = 0
⊢ (x - y).orderTop ≠ (↑g : WithTop Γ)

Tactic:
refine orderTop_ne_of_coeff_eq_zero ?_

Premises used: HahnSeries.orderTop_ne_of_coeff_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
h : x = 0
⊢ False

Tactic:
simp_all [orderTop_zero, WithTop.top_ne_coe]

Premises used: WithTop.top_ne_coe, HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := fun h ↦ by simp_all [orderTop_zero, WithTop.top_ne_coe]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
⊢ ⋯.min (s := x.support) ⋯ = g

Tactic:
rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hxg

Premises used: WithTop.coe_eq_coe, HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min (s := x.support) ⋯ = g
h : y = 0
⊢ False

Tactic:
simp_all [orderTop_zero, WithTop.top_ne_coe]

Premises used: WithTop.top_ne_coe, HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min (s := x.support) ⋯ = g
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := fun h ↦ by simp_all [orderTop_zero, WithTop.top_ne_coe]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min (s := x.support) ⋯ = g
hy : y ≠ 0
⊢ ⋯.min (s := y.support) ⋯ = g

Tactic:
rw [orderTop_of_ne_zero hy, WithTop.coe_eq_coe] at hyg

Premises used: WithTop.coe_eq_coe, HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hxyc : x.leadingCoeff = y.leadingCoeff
hx : x ≠ 0
hxg : ⋯.min (s := x.support) ⋯ = g
hy : y ≠ 0
hyg : ⋯.min (s := y.support) ⋯ = g
⊢ x.coeff g = y.coeff g

Tactic:
simp only [leadingCoeff_of_ne_zero hx, leadingCoeff_of_ne_zero hy, untop_orderTop_of_ne_zero hx,
    untop_orderTop_of_ne_zero hy, hxg, hyg] at hxyc

Premises used: HahnSeries.untop_orderTop_of_ne_zero, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
g : Γ
hx : x ≠ 0
hxg : ⋯.min (s := x.support) ⋯ = g
hy : y ≠ 0
hyg : ⋯.min (s := y.support) ⋯ = g
hxyc : x.coeff g = y.coeff g
rwa : x.coeff g - y.coeff g = 0
rwa₁ rwa₂ rwa₃ rwa₄ : x.coeff g = y.coeff g
⊢ (x - y).coeff g = 0

Tactic:
rwa [coeff_sub, sub_eq_zero]

Premises used: sub_eq_zero, HahnSeries.coeff_sub
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddGroup R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
rw : (↑g : WithTop Γ) = min (↑g : WithTop Γ) y.orderTop
rw₁ : (↑g : WithTop Γ) = min (↑g : WithTop Γ) (↑g : WithTop Γ)
rw₂ rw₃ : (↑g : WithTop Γ) = (↑g : WithTop Γ)
⊢ (↑g : WithTop Γ) = min x.orderTop y.orderTop

Tactic:
rw [hxg, hyg, inf_idem]

Premises used: inf_idem
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x x_1 : R
x_2 : V⟦Γ⟧
coeff : ∀ (x_3 : Γ), ((x * x_1) • x_2).coeff x_3 = (x • x_1 • x_2).coeff x_3
⊢ (x * x_1) • x_2 = x • x_1 • x_2

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x x_1 : R
x_2 : V⟦Γ⟧
x_3 : Γ
⊢ ((x * x_1) • x_2).coeff x_3 = (x • x_1 • x_2).coeff x_3

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x : V⟦Γ⟧
coeff : ∀ (x_1 : Γ), (HSMul.hSMul (α := R) 1 x).coeff x_1 = x.coeff x_1
⊢ HSMul.hSMul (α := R) 1 x = x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x : V⟦Γ⟧
x_1 : Γ
⊢ (HSMul.hSMul (α := R) 1 x).coeff x_1 = x.coeff x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x : R
coeff : ∀ (x_1 : Γ), (HSMul.hSMul (β := V⟦Γ⟧) x 0).coeff x_1 = HahnSeries.coeff 0 x_1
⊢ HSMul.hSMul (β := V⟦Γ⟧) x 0 = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x : R
x_1 : Γ
⊢ (HSMul.hSMul (β := V⟦Γ⟧) x 0).coeff x_1 = coeff 0 x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x : R
x_1 x_2 : V⟦Γ⟧
coeff : ∀ (x_3 : Γ), (x • (x_1 + x_2)).coeff x_3 = (x • x_1 + x • x_2).coeff x_3
⊢ x • (x_1 + x_2) = x • x_1 + x • x_2

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
x : R
x_1 x_2 : V⟦Γ⟧
x_3 : Γ
⊢ (x • (x_1 + x_2)).coeff x_3 = (x • x_1 + x • x_2).coeff x_3

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S_1 : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
S : Type u_9
inst_4 : Monoid S
inst_5 : DistribMulAction S V
inst_6 : SMul R S
inst_7 : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
coeff : ∀ (x : Γ), ((r • s) • a).coeff x = (r • s • a).coeff x
⊢ (r • s) • a = r • s • a

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S_1 : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
S : Type u_9
inst_4 : Monoid S
inst_5 : DistribMulAction S V
inst_6 : SMul R S
inst_7 : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
x : Γ
⊢ ((r • s) • a).coeff x = (r • s • a).coeff x

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S_1 : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
S : Type u_9
inst_4 : Monoid S
inst_5 : DistribMulAction S V
inst_6 : SMulCommClass R S V
r : R
s : S
a : V⟦Γ⟧
coeff : ∀ (x : Γ), (r • s • a).coeff x = (s • r • a).coeff x
⊢ r • s • a = s • r • a

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S_1 : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Monoid R
inst_2 : AddMonoid V
inst_3 : DistribMulAction R V
S : Type u_9
inst_4 : Monoid S
inst_5 : DistribMulAction S V
inst_6 : SMulCommClass R S V
r : R
s : S
a : V⟦Γ⟧
x : Γ
⊢ (r • s • a).coeff x = (s • r • a).coeff x

Tactic:
simp [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x x_1 : R
x_2 : V⟦Γ⟧
coeff : ∀ (x_3 : Γ), ((x + x_1) • x_2).coeff x_3 = (x • x_2 + x_1 • x_2).coeff x_3
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x x_1 : R
x_2 : V⟦Γ⟧
x_3 : Γ
⊢ ((x + x_1) • x_2).coeff x_3 = (x • x_2 + x_1 • x_2).coeff x_3

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x : V⟦Γ⟧
coeff : ∀ (x_1 : Γ), (HSMul.hSMul (α := R) 0 x).coeff x_1 = HahnSeries.coeff 0 x_1
⊢ HSMul.hSMul (α := R) 0 x = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x : V⟦Γ⟧
x_1 : Γ
⊢ (HSMul.hSMul (α := R) 0 x).coeff x_1 = coeff 0 x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
a : Γ
r : R
s : V
coeff :
  ∀ (b : Γ),
    HahnSeries.coeff (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s)) b =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
            (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)).coeff
        b
⊢ ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s) =
    HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)

Tactic:
ext b
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
a : Γ
r : R
s : V
b : Γ
pos :
  ∀ (h : b = a),
    coeff (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s)) b =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
            (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)).coeff
        b
neg :
  ∀ (h : ¬b = a),
    coeff (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s)) b =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
            (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)).coeff
        b
⊢ coeff (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) (r • s)) b =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) r : R)
          (ZeroHom.toFun (↑(addMonoidHom a) : ZeroHom V V⟦Γ⟧) s)).coeff
      b

Tactic:
by_cases h : b = a