awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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)) → ℝ)
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)) → ℝ)
⊢ StrictMono.{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

Premises used: Monotone.strictMono_of_injective
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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
⊢ Monotone.{u_1, 0} (α := ↥(strata.stratum c)) (β := ℝ)
    (⇑((fun (c : FiniteArchimedeanClass M) ↦ ((f c).toRatLinearMap : ↥(strata.stratum c) →ₗ[ℚ] ℝ)) c) :
      (a : ↥(strata.stratum c)) → ℝ)

Tactic:
simpa using OrderHomClass.monotone (f c)

Premises used: OrderHomClass.monotone
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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
⊢ 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:
simpa using hf c
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Module ℚ M
inst_4 : IsOrderedModule ℚ M
⊢ ∃ (f : M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass M⟧),
    StrictMono (α := 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:
apply hahnEmbedding_isOrderedModule

Premises used: hahnEmbedding_isOrderedModule
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
Goal:
M : Type u_1
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
⊢ Function.Injective (α := M) (β := DivisibleHull M) (⇑f₁ : (a : M) → DivisibleHull M)

Tactic:
have hf₁ : Function.Injective f₁ := DivisibleHull.coe_injective
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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)
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:
simp [f₁]
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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)
⊢ ∀ (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₁]
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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)))
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⟧))))
⊢ ∃ (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)

Premises used: DivisibleHull, hahnEmbedding_isOrderedModule_rat
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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' := ⋯ }
⊢ Function.Injective (α := DivisibleHull M) (β := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)
    (⇑f₂ : (a : DivisibleHull M) → Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧)

Tactic:
have hf₂ : Function.Injective f₂ := hf₂'.injective
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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)⟧)
⊢ ∀ (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
-- Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding
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)⟧)
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₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (r := fun (x1 x2 : FiniteArchimedeanClass (DivisibleHull M)) ↦ x1 ≤ x2) (s :=
      fun (x1 x2 : FiniteArchimedeanClass M) ↦ x1 ≤ x2)
      (FiniteArchimedeanClass.congrOrderIso (OrderIso.symm (DivisibleHull.archimedeanClassOrderIso M))))
⊢ Function.Injective (α := Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) (β := Lex ℝ⟦FiniteArchimedeanClass M⟧)
    (⇑f₃ : (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧) → Lex ℝ⟦FiniteArchimedeanClass M⟧)

Tactic:
have hf₃ : Function.Injective f₃ := HahnSeries.embDomainOrderAddMonoidHom_injective _
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder R
x y : Lex R⟦Γ⟧
⊢ Eq (α := Lex (Γ → R))
      ((fun (x : Lex R⟦Γ⟧) ↦
          ((toLex : (a : Γ → R) → Lex (Γ → R)) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) : Lex (Γ → R)))
        x)
      ((fun (x : Lex R⟦Γ⟧) ↦
          ((toLex : (a : Γ → R) → Lex (Γ → R)) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x)) : Lex (Γ → R)))
        y) →
    x = y

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder R
a b : Lex R⟦Γ⟧
⊢ a < b ↔
    ∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)

Tactic:
rfl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
inr : ∀ (hab : a ≠ b), a ≤ b ∨ b ≤ a
⊢ a ≤ b ∨ b ≤ a

Tactic:
rcases eq_or_ne a b with hab | hab

Premises used: eq_or_ne
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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

Tactic:
Or.inl hab.le

Premises used: Eq.le, Or.inl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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

Tactic:
exact Or.inl hab.le

Premises used: Eq.le, Or.inl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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_1 : Γ), a.coeff a_1 ≠ b.coeff a_1

Tactic:
have hab := Function.ne_iff.mp <| HahnSeries.ext_iff.ne.mp hab
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
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
⊢ i ∈ u

Tactic:
rw [Set.mem_union, Set.mem_setOf_eq, Set.mem_setOf_eq]

Premises used: Set.mem_union, Set.mem_setOf_eq
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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
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
⊢ 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:
contrapose! h
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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 :
  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
rw : ¬Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
rw₁ : Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
rw₂ : Eq.{u_2 + 1} (α := R) 0 (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ i ∉ v

Tactic:
rw [Set.notMem_setOf_iff, not_not, h.1, h.2]

Premises used: Classical.not_not, Set.notMem_setOf_iff, And.right, And.left
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)}
⊢ v ⊆ u

Tactic:
have hvu : v ⊆ u := by
        intro i h
        rw [Set.mem_union, Set.mem_setOf_eq, Set.mem_setOf_eq]
        contrapose! h
        rw [Set.notMem_setOf_iff, not_not, h.1, h.2]
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)}
hvu : v ⊆ u
⊢ v.IsWF

Tactic:
have hv : v.IsWF :=
        ((ofLex a).isPWO_support'.isWF.union (ofLex b).isPWO_support'.isWF).subset hvu
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min (s := v) hab
⊢ ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)

Tactic:
have hji (j) : j < i → (ofLex a).coeff j = (ofLex b).coeff j :=
        not_imp_not.mp <| fun h' ↦ hv.not_lt_min hab h'
-- Module: Mathlib.RingTheory.HahnSeries.Lex
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)}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min (s := v) hab
hji :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
⊢ Ne.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)

Tactic:
have hne : (ofLex a).coeff i ≠ (ofLex b).coeff i := hv.min_mem hab