awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
pos : ∀ (hx : x = 0), min x.order y.order ≤ (x + y).order
⊢ min x.order y.order ≤ (x + y).order
have neg : ∀ (hx : ¬x = 0), min x.order y.order ≤ (x + y).order
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.order y.order ≤ (x + y).order
have pos : ∀ (hy : y = 0), min x.order y.order ≤ (x + y).order
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
pos : ∀ (hy : y = 0), min x.order y.order ≤ (x + y).order
⊢ min x.order y.order ≤ (x + y).order
have neg : ∀ (hy : ¬y = 0), min x.order y.order ≤ (x + y).order
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.order y.order ≤ (x + y).order
have neg : min (sorry.min (s := x.support) sorry) (sorry.min (s := y.support) sorry) ≤ sorry.min (s := (x + y).support) sorry
Tactic: rw [order_of_ne hx, order_of_ne hy, order_of_ne hxy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + y).orderTop = x.orderTop
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := orderTop_ne_top.1 hxy.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
⊢ (x + y).coeff g ≠ 0
have rw : x.coeff g ≠ 0
Tactic: rw [coeff_add, coeff_eq_zero_of_lt_orderTop (lt_of_eq_of_lt (orderTop_of_ne_zero hx).symm hxy),
      add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
⊢ (x + y).orderTop = x.orderTop
have hcxyne : (x + y).coeff g ≠ 0
Tactic: have hcxyne : (x + y).coeff g ≠ 0 := by
    rw [coeff_add, coeff_eq_zero_of_lt_orderTop (lt_of_eq_of_lt (orderTop_of_ne_zero hx).symm hxy),
      add_zero]
    exact coeff_orderTop_ne (orderTop_of_ne_zero hx)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ x.orderTop
have rw : (x + y).orderTop ≤ (↑(sorry.min (s := x.support) sorry) : WithTop Γ)
Tactic: rw [orderTop_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop = x.orderTop
have hxyx : (x + y).orderTop ≤ x.orderTop
Tactic: have hxyx : (x + y).orderTop ≤ x.orderTop := by
    rw [orderTop_of_ne_zero hx]
    exact orderTop_le_of_coeff_ne_zero hcxyne
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + y).leadingCoeff = x.leadingCoeff
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := orderTop_ne_top.1 hxy.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
have ho : (x + y).orderTop = x.orderTop
Tactic: have ho : (x + y).orderTop = x.orderTop := orderTop_add_eq_left hxy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
⊢ (x + y).leadingCoeff = x.leadingCoeff
have pos : ∀ (h : x + y = 0), (x + y).leadingCoeff = x.leadingCoeff
Tactic: by_cases h : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
pos : ∀ (h : x + y = 0), (x + y).leadingCoeff = x.leadingCoeff
⊢ (x + y).leadingCoeff = x.leadingCoeff
have neg : ∀ (h : ¬x + y = 0), (x + y).leadingCoeff = x.leadingCoeff
Tactic: by_cases h : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
have ho₁ : ⊤ = x.orderTop
Tactic: rw [h, orderTop_zero] at ho
Cleared hypotheses: ho, h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : ⊤ = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
have pos : leadingCoeff.{u_8, u_3} (Γ := Γ) 0 = x.leadingCoeff
Tactic: rw [h, orderTop_eq_top.mp ho.symm]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : ⊤ = x.orderTop
h : x + y = 0
pos : leadingCoeff.{u_8, u_3} (Γ := Γ) 0 = x.leadingCoeff
⊢ (x + y).leadingCoeff = x.leadingCoeff
have pos₁ : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_8, u_3} (Γ := Γ) 0) (leadingCoeff.{u_8, u_3} (Γ := Γ) 0)
Tactic: rw [h, orderTop_eq_top.mp ho.symm]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
have neg : x.coeff (x.orderTop.untop sorry) + y.coeff (x.orderTop.untop sorry) = x.coeff (x.orderTop.untop sorry)
Tactic: simp_rw [leadingCoeff_of_ne_zero h, leadingCoeff_of_ne_zero hx, ho, coeff_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ x.coeff (x.orderTop.untop ⋯) + y.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
have neg : x.coeff (x.orderTop.untop sorry) + 0 = x.coeff (x.orderTop.untop sorry)
Tactic: rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
neg : x.coeff (x.orderTop.untop ⋯) + 0 = x.coeff (x.orderTop.untop ⋯)
⊢ x.coeff (x.orderTop.untop ⋯) + y.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
have neg₁ : x.coeff (x.orderTop.untop sorry) = x.coeff (x.orderTop.untop sorry)
Tactic: rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : Zero Γ
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x = 0
⊢ False
have hxy₁ : 0 = y
Tactic: simp only [h, order_zero, leadingCoeff_zero, map_zero, add_zero] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x.order = y.order
⊢ False
have hyne : Ne (α := R⟦Γ⟧) ((single y.order : (a : R) → R⟦Γ⟧) y.leadingCoeff : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: have hyne : single y.order y.leadingCoeff ≠ 0 := single_ne_zero <| leadingCoeff_ne_zero.mpr hy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x.order = y.order
hyne : Ne (α := R⟦Γ⟧) ((single y.order : (a : R) → R⟦Γ⟧) y.leadingCoeff : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ False
have hyne₁ : Ne (α := R⟦Γ⟧) 0 0
Tactic: rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy, single_eq_zero] at hyne
Cleared hypotheses: hyne
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
⊢ x.order < y.order
have this : x.order ≠ y.order
Tactic: have : x.order ≠ y.order := by
    intro h
    have hyne : single y.order y.leadingCoeff ≠ 0 := single_ne_zero <| leadingCoeff_ne_zero.mpr hy
    rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy, single_eq_zero] at hyne
    exact hyne rfl
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order < y.order
have refine : x.order ≤ y.order
Tactic: refine lt_of_le_of_ne ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order ≤ y.order
have simp : sorry.min (s := x.support) sorry ≤ sorry.min (s := y.support) sorry
Tactic: simp only [order, ne_zero_of_eq_add_single hxy hy, ↓reduceDIte, hy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
⊢ ⋯.min (s := x.support) ⋯ ≤ ⋯.min (s := y.support) ⋯
have refine : ∀ (g : Γ) (hg : g ∈ y.support), g ∈ x.support
Tactic: refine Set.IsWF.min_le_min_of_subset fun g hg ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
⊢ g ∈ x.support
have inl : ∀ (hg : x.order ∈ y.support), x.order ∈ x.support
Tactic: obtain rfl | hgx := eq_or_ne g x.order
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
inl : ∀ (hg : x.order ∈ y.support), x.order ∈ x.support
⊢ g ∈ x.support
have inr : ∀ (hgx : g ≠ x.order), g ∈ x.support
Tactic: obtain rfl | hgx := eq_or_ne g x.order
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ x.coeff g = (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)).coeff g
have rw : x.coeff g = x.coeff g
Tactic: rw [← hxy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ g ∈ x.support
have this₁ : x.coeff g = (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)).coeff g
Tactic: have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this_1 : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)).coeff g
⊢ g ∈ x.support
have this₁ : x.coeff g = y.coeff g
Tactic: rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
⊢ embDomain f (x + y) = embDomain f x + embDomain f y
have coeff : ∀ (g : Γ'), (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
have pos : ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
  (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
Tactic: by_cases hg : g ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
pos :
  ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
    (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
have neg : ∀ (hg : g ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
  (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
Tactic: by_cases hg : g ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
have pos : ∀ (a : Γ),
  (embDomain f (x + y)).coeff ((f : (a : Γ) → Γ') a) = (embDomain f x + embDomain f y).coeff ((f : (a : Γ) → Γ') a)
Tactic: obtain ⟨a, rfl⟩ := hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
⊢ (truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
      ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)
have coeff : ∀ (i : Γ),
  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: ext i
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
⊢ 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
have pos : ∀ (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: by_cases h : i < c
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
pos :
  ∀ (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
⊢ 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
have neg : ∀ (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: by_cases h : i < c
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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 + y = y + x
have coeff : ∀ (x_1 : Γ), (x + y).coeff x_1 = (y + x).coeff x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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)
⊢ Eq.{u_3 + 1} (α := R) (coeff (∑ i ∈ cons i s his, x i) g) (∑ i ∈ cons i s his, (x i).coeff g)
have rw : (x i + ∑ x_1 ∈ s, x x_1).coeff g = ∑ i ∈ cons i s his, (x i).coeff g
Tactic: rw [sum_cons, sum_cons, coeff_add, hsum]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ Eq.{u_3 + 1} (α := R) (coeff (∑ i ∈ cons i s his, x i) g) (∑ i ∈ cons i s his, (x i).coeff g)
have rw₁ : (x i + ∑ x_1 ∈ s, x x_1).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g
Tactic: rw [sum_cons, sum_cons, coeff_add, hsum]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ Eq.{u_3 + 1} (α := R) (coeff (∑ i ∈ cons i s his, x i) g) (∑ i ∈ cons i s his, (x i).coeff g)
have 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
Tactic: rw [sum_cons, sum_cons, coeff_add, hsum]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ Eq.{u_3 + 1} (α := R) (coeff (∑ i ∈ cons i s his, x i) g) (∑ i ∈ cons i s his, (x i).coeff g)
have rw₃ : (x i).coeff g + ∑ i ∈ s, (x i).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g
Tactic: rw [sum_cons, sum_cons, coeff_add, hsum]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
⊢ (-x).support = x.support
have h : ∀ (x_1 : Γ), x_1 ∈ (-x).support ↔ x_1 ∈ x.support
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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⟦Γ⟧
⊢ Eq (α := S⟦Γ⟧) ((-x).map f) (-x.map f)
have coeff : ∀ (x_1 : Γ), coeff ((-x).map f) x_1 = coeff (-x.map f) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : Zero Γ
f : R⟦Γ⟧
⊢ (-f).order = f.order
have pos : ∀ (hf : f = 0), (-f).order = f.order
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ (-f).order = f.order
have neg : ∀ (hf : ¬f = 0), (-f).order = f.order
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
inst_2 : Zero Γ
f : R⟦Γ⟧
⊢ (-f).order = f.order
have pos : ∀ (hf : f = 0), (-f).order = f.order
Tactic: classical
  by_cases hf : f = 0
  · simp only [hf, neg_zero]
  simp only [order, support_neg, neg_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ (-f).order = f.order
have neg : ∀ (hf : ¬f = 0), (-f).order = f.order
Tactic: classical
  by_cases hf : f = 0
  · simp only [hf, neg_zero]
  simp only [order, support_neg, neg_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
⊢ (-x).leadingCoeff = -x.leadingCoeff
have inl : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) (-0)) (-leadingCoeff.{u_1, u_3} (Γ := Γ) 0)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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)
⊢ (-x).leadingCoeff = -x.leadingCoeff
have inr : ∀ (hx : x ≠ 0), (-x).leadingCoeff = -x.leadingCoeff
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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 - y).map f = HSub.hSub (α := S⟦Γ⟧) (x.map f) (y.map f)
have coeff : ∀ (x_1 : Γ), coeff ((x - y).map f) x_1 = (HSub.hSub (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1
Tactic: ext