awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
have rw : min x.orderTop (-y).orderTop ≤ (x + -y).orderTop
Tactic: rw [sub_eq_add_neg, ← orderTop_neg (x := y)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
have rw : (x + -y).orderTop = x.orderTop
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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
have hxy₁ : x.orderTop < (-y).orderTop
Tactic: rw [← orderTop_neg (x := y)] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
have rw : (x + -y).leadingCoeff = x.leadingCoeff
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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
have hxy₁ : x.orderTop < (-y).orderTop
Tactic: rw [← orderTop_neg (x := y)] at hxy
Cleared hypotheses: hxy
-- 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 y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = (↑g : WithTop Γ)
hyg : y.orderTop = (↑g : WithTop Γ)
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ (x - y).orderTop ≠ (↑g : WithTop Γ)
have refine : (x - y).coeff g = 0
Tactic: refine orderTop_ne_of_coeff_eq_zero ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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).coeff g = 0
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := fun h ↦ by simp_all [orderTop_zero, WithTop.top_ne_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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
⊢ (x - y).coeff g = 0
have hxg₁ : sorry.min (s := x.support) sorry = g
Tactic: rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hxg
Cleared hypotheses: hxg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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
⊢ (x - y).coeff g = 0
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := fun h ↦ by simp_all [orderTop_zero, WithTop.top_ne_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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
⊢ (x - y).coeff g = 0
have hyg₁ : sorry.min (s := y.support) sorry = g
Tactic: rw [orderTop_of_ne_zero hy, WithTop.coe_eq_coe] at hyg
Cleared hypotheses: hyg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
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 - y).coeff g = 0
have hxyc₁ : 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
Cleared hypotheses: hxyc
-- 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 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
⊢ (x - y).coeff g = 0
have rwa : x.coeff g - y.coeff g = 0
Tactic: rwa [coeff_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ (↑g : WithTop Γ) = min x.orderTop y.orderTop
have rw : (↑g : WithTop Γ) = min (↑g : WithTop Γ) y.orderTop
Tactic: rw [hxg, hyg, inf_idem]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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
⊢ (↑g : WithTop Γ) = min x.orderTop y.orderTop
have rw₁ : (↑g : WithTop Γ) = min (↑g : WithTop Γ) (↑g : WithTop Γ)
Tactic: rw [hxg, hyg, inf_idem]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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 Γ)
⊢ (↑g : WithTop Γ) = min x.orderTop y.orderTop
have rw₂ : (↑g : WithTop Γ) = (↑g : WithTop Γ)
Tactic: rw [hxg, hyg, inf_idem]
-- 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_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 * x_1) • x_2 = x • x_1 • x_2
have coeff : ∀ (x_3 : Γ), ((x * x_1) • x_2).coeff x_3 = (x • x_1 • x_2).coeff x_3
Tactic: ext
-- 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_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⟦Γ⟧
⊢ HSMul.hSMul (α := R) 1 x = x
have coeff : ∀ (x_1 : Γ), (HSMul.hSMul (α := R) 1 x).coeff x_1 = x.coeff x_1
Tactic: ext
-- 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_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
⊢ HSMul.hSMul (β := V⟦Γ⟧) x 0 = 0
have coeff : ∀ (x_1 : Γ), (HSMul.hSMul (β := V⟦Γ⟧) x 0).coeff x_1 = coeff 0 x_1
Tactic: ext
-- 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_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 • (x_1 + x_2) = x • x_1 + x • x_2
have coeff : ∀ (x_3 : Γ), (x • (x_1 + x_2)).coeff x_3 = (x • x_1 + x • x_2).coeff x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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⟦Γ⟧
⊢ (r • s) • a = r • s • a
have coeff : ∀ (x : Γ), ((r • s) • a).coeff x = (r • s • a).coeff x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
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⟦Γ⟧
⊢ r • s • a = s • r • a
have coeff : ∀ (x : Γ), (r • s • a).coeff x = (s • r • a).coeff x
Tactic: ext
-- 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 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x x_1 : R
x_2 : V⟦Γ⟧
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2
have coeff : ∀ (x_3 : Γ), ((x + x_1) • x_2).coeff x_3 = (x • x_2 + x_1 • x_2).coeff x_3
Tactic: ext
-- 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 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x : V⟦Γ⟧
⊢ HSMul.hSMul (α := R) 0 x = 0
have coeff : ∀ (x_1 : Γ), (HSMul.hSMul (α := R) 0 x).coeff x_1 = coeff 0 x_1
Tactic: ext
-- 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 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
a : Γ
r : R
s : V
⊢ 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)
have 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: ext b
-- 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 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
a : Γ
r : R
s : V
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
have 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
Tactic: by_cases h : b = a
-- 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 : 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
⊢ 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
have 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
Tactic: by_cases h : b = a
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst : PartialOrder Γ
inst_1 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : AddCommMonoid U
inst_5 : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
⊢ (r • x).map f = HSMul.hSMul (β := V⟦Γ⟧) r (x.map f)
have coeff : ∀ (x_1 : Γ), coeff ((r • x).map f) x_1 = (HSMul.hSMul (β := V⟦Γ⟧) r (x.map f)).coeff x_1
Tactic: ext
-- 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 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x x_1 : Γ →₀ V
⊢ (ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x + x_1) =
    HAdd.hAdd (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x : V⟦Γ⟧)
      ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)
have coeff : ∀ (x_2 : Γ),
  coeff ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x + x_1)) x_2 =
    (HAdd.hAdd (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x : V⟦Γ⟧)
          ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)).coeff
      x_2
Tactic: ext
-- 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 : Semiring R
inst_2 : AddCommMonoid V
inst_3 : Module R V
x : R
x_1 : Γ →₀ V
⊢ (ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x • x_1) =
    HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) x : R) ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)
have coeff : ∀ (x_2 : Γ),
  coeff ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) (x • x_1)) x_2 =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((RingHom.id R : (a : R) → R) x : R)
          ((ofFinsupp : (a : Γ →₀ V) → V⟦Γ⟧) x_1 : V⟦Γ⟧)).coeff
      x_2
Tactic: ext
-- 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 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
⊢ embDomain f (r • x) = r • embDomain f x
have coeff : ∀ (g : Γ'), (embDomain f (r • x)).coeff g = (r • embDomain f x).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 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
have pos : ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
  (embDomain f (r • x)).coeff g = (r • embDomain f x).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 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
pos :
  ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
    (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
have neg : ∀ (hg : g ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
  (embDomain f (r • x)).coeff g = (r • embDomain f x).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 : Semiring R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
have pos : ∀ (a : Γ), (embDomain f (r • x)).coeff ((f : (a : Γ) → Γ') a) = (r • embDomain f x).coeff ((f : (a : Γ) → Γ') a)
Tactic: obtain ⟨a, rfl⟩ := hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.support.Nonempty ↔ x ≠ 0
have rw : (Function.support x.coeff).Nonempty ↔ x ≠ 0
Tactic: rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
rw : (Function.support x.coeff).Nonempty ↔ x ≠ 0
⊢ x.support.Nonempty ↔ x ≠ 0
have rw₁ : x.coeff ≠ 0 ↔ x ≠ 0
Tactic: rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
rw : (Function.support x.coeff).Nonempty ↔ x ≠ 0
rw₁ : x.coeff ≠ 0 ↔ x ≠ 0
⊢ x.support.Nonempty ↔ x ≠ 0
have rw₂ : ¬x.coeff = 0 ↔ x ≠ 0
Tactic: rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
rw : (Function.support x.coeff).Nonempty ↔ x ≠ 0
rw₁ : x.coeff ≠ 0 ↔ x ≠ 0
rw₂ : ¬x.coeff = 0 ↔ x ≠ 0
⊢ x.support.Nonempty ↔ x ≠ 0
have rw₃ : ¬x = 0 ↔ x ≠ 0
Tactic: rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero S
f : ZeroHom R S
⊢ Eq (α := S⟦Γ⟧) (map 0 f) 0
have coeff : ∀ (x : Γ), coeff (map 0 f) x = coeff 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ Set.IsPWO (α := Lex (Γ × Γ')) (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
have refine_1 : Set.IsPWO.{u_1} (α := Γ)
  ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
    Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
Tactic: refine Set.PartiallyWellOrderedOn.subsetProdLex ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
refine_1 :
  Set.IsPWO.{u_1} (α := Γ)
    ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
⊢ Set.IsPWO (α := Lex (Γ × Γ')) (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
have refine_2 : ∀ (a : Γ),
  Set.IsPWO.{u_2} (α := Γ')
    {y : Γ' |
      Membership.mem (α := Lex (Γ × Γ')) (γ := Set (Lex (Γ × Γ')))
        (Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
        ((toLex : (a : Γ × Γ') → Lex (Γ × Γ')) (a, y) : Lex (Γ × Γ'))}
Tactic: refine Set.PartiallyWellOrderedOn.subsetProdLex ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ)
    ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2)
have refine_1 : ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
    Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2) ⊆
  Function.support x.coeff
Tactic: refine Set.IsPWO.mono x.isPWO_support' ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun (x : Lex (Γ × Γ')) ↦ ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x).1) ''
      Function.support (M := R) fun (g : Lex (Γ × Γ')) ↦ (x.coeff g.1).coeff g.2) ⊆
    Function.support x.coeff
have refine_1 : ∀ (x_1 : Lex (Γ × Γ')), (x.coeff x_1.1).coeff x_1.2 ≠ 0 → x.coeff ((ofLex : (a : Lex (Γ × Γ')) → Γ × Γ') x_1).1 ≠ 0
Tactic: simp_rw [Set.image_subset_iff, support_subset_iff, Set.mem_preimage, Function.mem_support]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h : R⟦Γ⟧ } = 0 ↔ f = 0
have simp_rw : f = coeff 0 ↔ f = 0
Tactic: simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
f : Γ → R
h : (Function.support f).IsPWO
simp_rw : f = coeff 0 ↔ f = 0
⊢ { coeff := f, isPWO_support' := h : R⟦Γ⟧ } = 0 ↔ f = 0
have simp_rw₁ : (∀ (x : Γ), f x = coeff 0 x) ↔ ∀ (x : Γ), f x = 0 x
Tactic: simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
f : Γ → R
h : (Function.support f).IsPWO
simp_rw : f = coeff 0 ↔ f = 0
simp_rw₁ : (∀ (x : Γ), f x = coeff 0 x) ↔ ∀ (x : Γ), f x = 0 x
⊢ { coeff := f, isPWO_support' := h : R⟦Γ⟧ } = 0 ↔ f = 0
have simp_rw₂ : (∀ (x : Γ), f x = 0) ↔ ∀ (x : Γ), f x = 0 x
Tactic: simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
⊢ Set.IsPWO.{u_1} (α := Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
have h₁ : Eq.{u_1 + 1} (α := Set Γ)
  (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := sorry })
  (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))
Tactic: have h₁ : (Function.support fun g => HahnSeries.mk (fun g' => x.coeff (g, g'))
        (Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g)) = Function.support
        fun g => fun g' => x.coeff (g, g') := by
      simp only [Function.support, ne_eq, mk_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  Eq.{u_1 + 1} (α := Set Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
    (Function.support (M := (g' : Γ') → R) fun (g : Γ) (g' : Γ') ↦ x.coeff (g, g'))
⊢ Set.IsPWO.{u_1} (α := Γ)
    (Function.support (M := R⟦Γ'⟧) fun (g : Γ) ↦ { coeff := fun (g' : Γ') ↦ x.coeff (g, g'), isPWO_support' := ⋯ })
have rw : (Prod.fst '' Function.support x.coeff).IsPWO
Tactic: rw [h₁, Function.support_fun_curry x.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) b = if b = a then r else 0
have pos : ∀ (h : b = a), coeff ((single a : (a : R) → R⟦Γ⟧) r) b = r
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
pos : ∀ (h : b = a), coeff ((single a : (a : R) → R⟦Γ⟧) r) b = r
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) r) b = if b = a then r else 0
have neg : ∀ (h : ¬b = a), Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) b) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r s : R
rs : Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
⊢ r = s
have rw : coeff ((single a : (a : R) → R⟦Γ⟧) r) a = s
Tactic: rw [← coeff_single_same a r, ← coeff_single_same a s, rs]