awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⟦Γ⟧)
rw : coeff ((single a : (a : R) → R⟦Γ⟧) r) a = s
⊢ r = s
have rw₁ : Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) a) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a)
Tactic: rw [← coeff_single_same a r, ← coeff_single_same a s, rs]
-- 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⟦Γ⟧)
rw : coeff ((single a : (a : R) → R⟦Γ⟧) r) a = s
rw₁ : Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) a) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a)
⊢ r = s
have rw₂ : Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a)
Tactic: rw [← coeff_single_same a r, ← coeff_single_same a s, rs]
-- 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
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
⊢ Eq (α := S⟦Γ⟧) (map ((single a : (a : R) → R⟦Γ⟧) r) f) ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r))
have coeff : ∀ (g : Γ), coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
Tactic: ext g
-- 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
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
g : Γ
⊢ coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
have pos : ∀ (h : g = a),
  coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
Tactic: by_cases h : g = a
-- 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
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
g : Γ
pos :
  ∀ (h : g = a),
    coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
⊢ coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
have neg : ∀ (h : ¬g = a),
  coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
Tactic: by_cases h : g = a
-- 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
a b : Γ
r : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
have obtain : ∀ (r s : R) (rs : r ≠ s), ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
Tactic: obtain ⟨r, s, rs⟩ := exists_pair_ne R
-- 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
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
have inhabit : ∀ (inhabited_h : Inhabited Γ), ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
Tactic: inhabit Γ
-- 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
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
have refine : ∀ (con : Eq (α := R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)),
  r = s
Tactic: refine ⟨single default r, single default s, fun con => rs ?_⟩
-- 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
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : Eq (α := R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
⊢ r = s
have rw : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) r) default = s
Tactic: rw [← coeff_single_same (default : Γ) r, con, coeff_single_same]
-- 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
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : Eq (α := R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
rw : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) r) default = s
⊢ r = s
have rw₁ : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) s) default = s
Tactic: rw [← coeff_single_same (default : Γ) r, con, coeff_single_same]
-- 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
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : Eq (α := R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
rw : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) r) default = s
rw₁ : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) s) default = s
⊢ r = s
have rw₂ : s = s
Tactic: rw [← coeff_single_same (default : Γ) r, con, coeff_single_same]
-- 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⟦Γ⟧
g : Γ
hg : g ∈ x.support
hx : ∀ g' ∈ x.support, g ≤ g'
⊢ x.orderTop = (↑g : WithTop Γ)
have rw : (↑(sorry.min (s := x.support) sorry) : WithTop Γ) = (↑g : WithTop Γ)
Tactic: rw [orderTop_of_ne_zero <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
    x.isWF_support.min_eq_of_le hg hx]
-- 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⟦Γ⟧
g : Γ
hg : g ∈ x.support
hx : ∀ g' ∈ x.support, g ≤ g'
rw : (↑(⋯.min (s := x.support) ⋯) : WithTop Γ) = (↑g : WithTop Γ)
⊢ x.orderTop = (↑g : WithTop Γ)
have rw₁ : (↑g : WithTop Γ) = (↑g : WithTop Γ)
Tactic: rw [orderTop_of_ne_zero <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
    x.isWF_support.min_eq_of_le hg hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
⊢ x.coeff g ≠ 0
have h : x.orderTop ≠ ⊤
Tactic: have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
h : x.orderTop ≠ ⊤
⊢ x.coeff g ≠ 0
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := orderTop_ne_top.1 h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
h : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff g ≠ 0
have hg₁ : sorry.min (s := x.support) sorry = g
Tactic: rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hg
Cleared hypotheses: 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⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min (s := x.support) ⋯ = g
⊢ x.coeff g ≠ 0
have rw : x.coeff (sorry.min (s := x.support) sorry) ≠ 0
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
R : Type u_3
inst : Zero R
Γ : Type u_5
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ x.orderTop ≤ (↑g : WithTop Γ)
have rw : sorry.min (s := x.support) sorry ≤ g
Tactic: rw [orderTop_of_ne_zero (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]
-- 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 : R
⊢ (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
have pos : ∀ (hr : r = 0), (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
Tactic: by_cases hr : r = 0
-- 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 : R
pos : ∀ (hr : r = 0), (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
⊢ (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
have neg : ∀ (hr : ¬r = 0), (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
Tactic: by_cases hr : r = 0
-- 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 : R
hr : ¬r = 0
⊢ (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
have neg : (↑a : WithTop Γ) ≤ (↑a : WithTop Γ)
Tactic: rw [orderTop_single hr]
-- 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⟦Γ⟧
i : Γ
hi : (↑i : WithTop Γ) < x.orderTop
⊢ x.coeff i = 0
have inl : ∀ (hi : (↑i : WithTop Γ) < orderTop.{u_1, u_3} (R := R) 0), Eq.{u_3 + 1} (α := R) (coeff 0 i) 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x, hi
-- 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⟦Γ⟧
i : Γ
hi : (↑i : WithTop Γ) < x.orderTop
inl : ∀ (hi : (↑i : WithTop Γ) < orderTop.{u_1, u_3} (R := R) 0), Eq.{u_3 + 1} (α := R) (coeff 0 i) 0
⊢ x.coeff i = 0
have inr : ∀ (hx : x ≠ 0), x.coeff i = 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- 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⟦Γ⟧
i : Γ
hi : (↑i : WithTop Γ) < x.orderTop
hx : x ≠ 0
⊢ x.coeff i = 0
have inr : ∀ (hi : x.coeff i ≠ 0), ¬(↑i : WithTop Γ) < x.orderTop
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ ¬(↑i : WithTop Γ) < x.orderTop
have hi₁ : i ∈ x.support
Tactic: rw [← mem_support] at hi
Cleared hypotheses: hi
-- 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⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬(↑i : WithTop Γ) < x.orderTop
have inr : ¬i < sorry.min (s := x.support) sorry
Tactic: rw [orderTop_of_ne_zero hx, WithTop.coe_lt_coe]
-- 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.leadingCoeff = 0 ↔ x = 0
have inl : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) 0 ↔ Eq (α := R⟦Γ⟧) 0 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- 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⟦Γ⟧
inl : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) 0 ↔ Eq (α := R⟦Γ⟧) 0 0
⊢ x.leadingCoeff = 0 ↔ x = 0
have inr : ∀ (hx : x ≠ 0), x.leadingCoeff = 0 ↔ x = 0
Tactic: obtain rfl | hx := eq_or_ne x 0
-- 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 : R
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
have pos : ∀ (h : r = 0), leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
Tactic: by_cases h : r = 0
-- 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 : R
pos : ∀ (h : r = 0), leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
have neg : ∀ (h : ¬r = 0), leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx : x.orderTop ≠ ⊤
⊢ x.coeff (x.orderTop.untop hx) = x.leadingCoeff
have hx₁ : x ≠ 0
Tactic: rw [orderTop_ne_top] at hx
-- 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⟦Γ⟧
hx_1 : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx_1) = x.leadingCoeff
have rw : x.coeff (x.orderTop.untop hx_1) = x.coeff (x.orderTop.untop sorry)
Tactic: rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]
-- 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⟦Γ⟧
hx_1 : x.orderTop ≠ ⊤
hx : x ≠ 0
rw : x.coeff (x.orderTop.untop hx_1) = x.coeff (x.orderTop.untop ⋯)
⊢ x.coeff (x.orderTop.untop hx_1) = x.leadingCoeff
have rw₁ : x.coeff (sorry.min (s := x.support) sorry) = x.coeff (sorry.min (s := x.support) sorry)
Tactic: rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]
-- 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⟦Γ⟧
inst_2 : Zero Γ
hx : x ≠ 0
⊢ (↑x.order : WithTop Γ) = x.orderTop
have rw : (↑(sorry.min (s := x.support) sorry) : WithTop Γ) = x.orderTop
Tactic: rw [order_of_ne hx, orderTop_of_ne_zero hx]
-- 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⟦Γ⟧
inst_2 : Zero Γ
hx : x ≠ 0
rw : (↑(⋯.min (s := x.support) ⋯) : WithTop Γ) = x.orderTop
⊢ (↑x.order : WithTop Γ) = x.orderTop
have rw₁ : (↑(sorry.min (s := x.support) sorry) : WithTop Γ) = (↑(sorry.min (s := x.support) sorry) : WithTop Γ)
Tactic: rw [order_of_ne hx, orderTop_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
⊢ x.coeff x.order = 0 ↔ x = 0
have refine : ∀ (hx : ¬x = 0), ¬x.coeff x.order = 0
Tactic: refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff x.order = 0
have rw : ¬x.coeff (sorry.min (s := x.support) sorry) = 0
Tactic: rw [order_of_ne hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hi : i < x.order
⊢ x.coeff i = 0
have inl : ∀ (hi : i < order.{u_1, u_3} (R := R) 0), Eq.{u_3 + 1} (α := R) (coeff 0 i) 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x, hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hi : i < x.order
inl : ∀ (hi : i < order.{u_1, u_3} (R := R) 0), Eq.{u_3 + 1} (α := R) (coeff 0 i) 0
⊢ x.coeff i = 0
have inr : ∀ (hx : x ≠ 0), x.coeff i = 0
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hi : i < x.order
hx : x ≠ 0
⊢ x.coeff i = 0
have inr : ∀ (hi : x.coeff i ≠ 0), ¬i < x.order
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ ¬i < x.order
have hi₁ : i ∈ x.support
Tactic: rw [← mem_support] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order
have inr : ¬i < sorry.min (s := x.support) sorry
Tactic: rw [order_of_ne hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
⊢ 0 < x.orderTop
have pos : ∀ (h : x = 0), 0 < x.orderTop
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
pos : ∀ (h : x = 0), 0 < x.orderTop
⊢ 0 < x.orderTop
have neg : ∀ (h : ¬x = 0), 0 < x.orderTop
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order
have pos : ∀ (h : x = 0), 0 ≤ x.orderTop ↔ 0 ≤ x.order
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
pos : ∀ (h : x = 0), 0 ≤ x.orderTop ↔ 0 ≤ x.order
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order
have neg : ∀ (h : ¬x = 0), 0 ≤ x.orderTop ↔ 0 ≤ x.order
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
⊢ x.leadingCoeff = x.coeff x.order
have pos : ∀ (h : x = 0), x.leadingCoeff = x.coeff x.order
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
pos : ∀ (h : x = 0), x.leadingCoeff = x.coeff x.order
⊢ x.leadingCoeff = x.coeff x.order
have neg : ∀ (h : ¬x = 0), x.leadingCoeff = x.coeff x.order
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ x.leadingCoeff = x.coeff x.order
have pos : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
Tactic: rw [h, leadingCoeff_zero, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : x = 0
pos :
  Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
⊢ x.leadingCoeff = x.coeff x.order
have pos₁ : Eq.{u_3 + 1} (α := R) 0 (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
Tactic: rw [h, leadingCoeff_zero, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : x = 0
pos :
  Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
pos₁ : Eq.{u_3 + 1} (α := R) 0 (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
⊢ x.leadingCoeff = x.coeff x.order
have pos₂ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [h, leadingCoeff_zero, coeff_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
a b_1 : Γ
r : R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb :
  Membership.mem (γ := Set Γ')
    (Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0)
    b
⊢ Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b
have contrapose : ∀ (hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support),
  b ∉
    Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0
Tactic: contrapose hb
Cleared hypotheses: hb
-- 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
a b_1 : Γ
r : R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support
⊢ b ∉
    Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0
have rw : ¬Ne.{u_3 + 1} (α := R)
    (if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
      x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
    else 0)
    0
Tactic: rw [Function.mem_support, dif_neg hb, Classical.not_not]
-- 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
a b_1 : Γ
r : R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support
rw :
  ¬Ne.{u_3 + 1} (α := R)
      (if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0)
      0
⊢ b ∉
    Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0
have rw₁ : ¬Ne.{u_3 + 1} (α := R) 0 0
Tactic: rw [Function.mem_support, dif_neg hb, Classical.not_not]
-- 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
a b_1 : Γ
r : R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support
rw :
  ¬Ne.{u_3 + 1} (α := R)
      (if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0)
      0
rw₁ : ¬Ne.{u_3 + 1} (α := R) 0 0
⊢ b ∉
    Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0
have rw₂ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [Function.mem_support, dif_neg hb, Classical.not_not]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
⊢ (embDomain f x).coeff ((f : (a : Γ) → Γ') a) = x.coeff a
have rw : {
        coeff := fun (b : Γ') ↦
          if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
            x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
          else 0,
        isPWO_support' := sorry : R⟦Γ'⟧ }.coeff
    ((f : (a : Γ) → Γ') a) =
  x.coeff a
Tactic: rw [embDomain]