awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ IsUnit (M := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
have refine : ∃ (b : R⟦Γ⟧), HMul.hMul (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧) b = 1
Tactic: refine isUnit_iff_exists_inv.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ ∃ (b : R⟦Γ⟧), HMul.hMul (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧) b = 1
have h : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
    ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) u.inv : R⟦Γ⟧) =
  1
Tactic: use heval x u.inv
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
      ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) u.inv : R⟦Γ⟧) =
    1
have h : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((↑u : R⟦X⟧) * u.inv) : R⟦Γ⟧) (1 : R⟦Γ⟧)
Tactic: rw [← heval_mul, Units.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
h : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((↑u : R⟦X⟧) * u.inv) : R⟦Γ⟧) (1 : R⟦Γ⟧)
⊢ HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
      ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) u.inv : R⟦Γ⟧) =
    1
have h₁ : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) 1) 1
Tactic: rw [← heval_mul, Units.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
h : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) ((↑u : R⟦X⟧) * u.inv) : R⟦Γ⟧) (1 : R⟦Γ⟧)
h₁ : Eq (α := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) 1) 1
⊢ HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) (↑u : R⟦X⟧) : R⟦Γ⟧)
      ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) u.inv : R⟦Γ⟧) =
    1
have h₂ : Eq (α := R⟦Γ⟧) 1 1
Tactic: rw [← heval_mul, Units.val_inv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
⊢ Eq (α := R) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) f) 0 : R)
    ((constantCoeff : (a : R⟦X⟧) → R) f : R)
have rw : Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) 0 : R) ((coeff 0 : (a : R⟦X⟧) → R) f : R)
Tactic: rw [coeff_heval, finsum_eq_single (fun n => ((powerSeriesFamily x f).coeff 0) n) 0,
    ← PowerSeries.coeff_zero_eq_constantCoeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
rw : Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) 0 : R) ((coeff 0 : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((heval x : (a : R⟦X⟧) → R⟦Γ⟧) f) 0 : R)
    ((constantCoeff : (a : R⟦X⟧) → R) f : R)
have rw₁ : ∀ (x_1 : ℕ), x_1 ≠ 0 → Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) x_1 : R) (0 : R)
Tactic: rw [coeff_heval, finsum_eq_single (fun n => ((powerSeriesFamily x f).coeff 0) n) 0,
    ← PowerSeries.coeff_zero_eq_constantCoeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ Eq (α := R) (((powerSeriesFamily x f).coeff 0 : (a : ℕ) → R) n : R) (0 : R)
have simp : HMul.hMul (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R)
    (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((powers x : (a : ℕ) → R⟦Γ⟧) n) 0 : R) =
  0
Tactic: simp only [coeff_apply, smulFamily_toFun, HahnSeries.coeff_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ HMul.hMul (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f : R)
      (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((powers x : (a : ℕ) → R⟦Γ⟧) n) 0 : R) =
    0
have refine : LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
Tactic: refine mul_eq_zero_of_right (coeff n f) (coeff_eq_zero_of_lt_orderTop ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
have pos : ∀ (h : 0 < x.orderTop),
  LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
Tactic: by_cases h : 0 < x.orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
pos :
  ∀ (h : 0 < x.orderTop),
    LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
have neg : ∀ (h : ¬0 < x.orderTop),
  LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
Tactic: by_cases h : 0 < x.orderTop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : 0 < x.orderTop
⊢ LT.lt.{u_1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n))
have pos : n • x.orderTop ≤ orderTop.{u_1, u_3} (R := R) ((powers x : (a : ℕ) → R⟦Γ⟧) n)
Tactic: refine (lt_of_lt_of_le ((nsmul_pos_iff hn).mpr h) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
have obtain : ∀ (strata : HahnEmbedding.ArchimedeanStrata ℚ M), Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
Tactic: obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
have choose : ∀ (f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ)
  (hf :
    ∀ (c : FiniteArchimedeanClass M),
      Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)),
  Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
Tactic: choose f hf using fun c ↦ Archimedean.exists_orderAddMonoidHom_real_injective (strata.stratum c)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf :
  ∀ (c : FiniteArchimedeanClass M),
    Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)
⊢ Nonempty.{max 1 (u_1 + 1)} (HahnEmbedding.Seed ℚ M ℝ)
have refine : ∀ (c : FiniteArchimedeanClass M),
  StrictMono.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
    (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
      (a : ↥(strata.stratum c)) → ℝ)
Tactic: refine ⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf :
  ∀ (c : FiniteArchimedeanClass M),
    Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)
c : FiniteArchimedeanClass M
⊢ StrictMono.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
    (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
      (a : ↥(strata.stratum c)) → ℝ)
have h₁ : Monotone.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
  (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
    (a : ↥(strata.stratum c)) → ℝ)
Tactic: apply Monotone.strictMono_of_injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf :
  ∀ (c : FiniteArchimedeanClass M),
    Function.Injective (α := ↥(strata.stratum c)) (β := ℝ) (⇑(f c) : (a : ↥(strata.stratum c)) → ℝ)
c : FiniteArchimedeanClass M
h₁ :
  Monotone.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
    (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
      (a : ↥(strata.stratum c)) → ℝ)
⊢ StrictMono.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
    (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
      (a : ↥(strata.stratum c)) → ℝ)
have h₂ : Function.Injective.{u_1 + 1, 1} (α := ↥(strata.stratum c)) (β := ℝ)
  (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
    (a : ↥(strata.stratum c)) → ℝ)
Tactic: apply Monotone.strictMono_of_injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
⊢ ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
have hf₁ : Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)
Tactic: have hf₁ : Function.Injective f₁ := DivisibleHull.coe_injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)
⊢ ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
have hf₁class : ∀ (a : M),
  Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
    ((OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M) :
        (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
      (ArchimedeanClass.mk ((f₁ : (a : M) → DivisibleHull M) a)))
Tactic: have hf₁class (a : M) : mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (mk (f₁ a)) := by
    simp [f₁]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)
hf₁class :
  ∀ (a : M),
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
      ((OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
        (ArchimedeanClass.mk ((f₁ : (a : M) → DivisibleHull M) a)))
⊢ ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
have obtain : ∀ (f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
  (hf₂' :
    StrictMono (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
      (⇑f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))
  (hf₂class' :
    ∀ (a : DivisibleHull M),
      Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a)
        ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
            (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
          (orderTop (R := ℝ)
            ((ofLex :
                (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
              ((f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a :
                Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))))),
  ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
Tactic: obtain ⟨f₂', hf₂', hf₂class'⟩ := hahnEmbedding_isOrderedModule_rat (DivisibleHull M)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)
hf₁class :
  ∀ (a : M),
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
      ((OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
        (ArchimedeanClass.mk ((f₁ : (a : M) → DivisibleHull M) a)))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' :
  StrictMono (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
    (⇑f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
hf₂class' :
  ∀ (a : DivisibleHull M),
    Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a)
      ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
          (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
        (orderTop (R := ℝ)
          ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
            ((f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a :
              Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))))
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
⊢ ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
have hf₂ : Function.Injective (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
  (⇑f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
Tactic: have hf₂ : Function.Injective f₂ := hf₂'.injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HahnEmbedding (hypothesis)
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)
hf₁class :
  ∀ (a : M),
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
      ((OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
        (ArchimedeanClass.mk ((f₁ : (a : M) → DivisibleHull M) a)))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' :
  StrictMono (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
    (⇑f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
hf₂class' :
  ∀ (a : DivisibleHull M),
    Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a)
      ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
          (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
        (orderTop (R := ℝ)
          ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
            ((f₂' : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a :
              Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))))
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ :
  Function.Injective (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
    (⇑f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
⊢ ∃ (f : M →+o Lex ℝ⟦FiniteArchimedeanClass M⟧),
    Function.Injective (α := M) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
        (⇑f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) ∧
      ∀ (a : M),
        Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
          ((FiniteArchimedeanClass.withTopOrderIso M : (a : WithTop (FiniteArchimedeanClass M)) → ArchimedeanClass M)
            (orderTop (R := ℝ)
              ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass M⟧) → ℝ⟦FiniteArchimedeanClass M⟧)
                ((f : (a : M) → Lex ℝ⟦FiniteArchimedeanClass M⟧) a : Lex ℝ⟦FiniteArchimedeanClass M⟧))))
have hf₂class : ∀ (a : DivisibleHull M),
  Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk a)
    ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M) :
        (a : WithTop (FiniteArchimedeanClass (DivisibleHull M))) → ArchimedeanClass (DivisibleHull M))
      (orderTop (R := ℝ)
        ((ofLex : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
          ((f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) a :
            Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧))))
Tactic: have hf₂class (a : DivisibleHull M) :
      mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop :=
    hf₂class' a
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
⊢ a ≤ b ∨ b ≤ a
have inl : ∀ (hab : a = b), a ≤ b ∨ b ≤ a
Tactic: rcases eq_or_ne a b with hab | hab
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
inl : ∀ (hab : a = b), a ≤ b ∨ b ≤ a
⊢ a ≤ b ∨ b ≤ a
have inr : ∀ (hab : a ≠ b), a ≤ b ∨ b ≤ a
Tactic: rcases eq_or_ne a b with hab | hab
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a ≠ b
⊢ a ≤ b ∨ b ≤ a
have hab₁ : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
Tactic: have hab := Function.ne_iff.mp <| HahnSeries.ext_iff.ne.mp hab
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
i : Γ
h : i ∈ v
⊢ i ∈ u
have rw : Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∨
  Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0
Tactic: rw [Set.mem_union, Set.mem_setOf_eq, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : LinearOrder R
a b : Lex R⟦Γ⟧
hab_1 : a ≠ b
hab : ∃ (a_1 : Γ), a.coeff a_1 ≠ b.coeff a_1
u : Set Γ :=
  {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0} ∪
    {i : Γ | Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0}
v : Set Γ :=
  {i : Γ |
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)}
i : Γ
h : i ∈ v
⊢ Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∨
    Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0
have contrapose! : ∀
  (h :
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) 0 ∧
      Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i) 0),
  i ∉ v
Tactic: contrapose! h
Cleared hypotheses: h