awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : AddCommGroup R
inst_3 : IsOrderedAddMonoid R
inst_4 : Archimedean R
inst_5 : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    (((OrderIso.trans (OrderIso.symm (FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)))
              (OrderIso.withTopCongr (finiteArchimedeanClassOrderIso Γ R)) :
            ArchimedeanClass (Lex R⟦Γ⟧) ≃o WithTop Γ) :
          (a : ArchimedeanClass (Lex R⟦Γ⟧)) → WithTop Γ)
        (ArchimedeanClass.mk x) :
      WithTop Γ)
    (orderTop.{u_1, u_2} (R := R) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) x) : WithTop Γ)

Tactic:
simp [FiniteArchimedeanClass.withTopOrderIso_symm_apply, *]

Premises used: FiniteArchimedeanClass.withTopOrderIso_symm_apply
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
⊢ LE.le (α := Lex R⟦Γ⟧) 0 1

Tactic:
simp [← leadingCoeff_nonneg_iff]

Premises used: HahnSeries.leadingCoeff_nonneg_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : b ≤ c
rw : ∀ (hbc : 0 ≤ c - b), 0 ≤ a * c - a * b
⊢ a * b ≤ a * c

Tactic:
rw [← sub_nonneg] at hbc ⊢

Premises used: sub_nonneg
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
rw :
  0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
⊢ 0 ≤ a * c - a * b

Tactic:
rw [← mul_sub, ← leadingCoeff_nonneg_iff, ofLex_mul, leadingCoeff_mul]

Premises used: HahnSeries.leadingCoeff_mul, mul_sub, HahnSeries.leadingCoeff_nonneg_iff, ofLex_mul
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
ha₁ : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
hb : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
⊢ 0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))

Tactic:
apply mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))

Tactic:
simpa
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
hb hb₁ hb₂ hb₃ : 0 ≤ c - b
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))

Tactic:
rwa [leadingCoeff_nonneg_iff]

Premises used: HahnSeries.leadingCoeff_nonneg_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : b ≤ c
rw : ∀ (hbc : 0 ≤ c - b), 0 ≤ c * a - b * a
⊢ b * a ≤ c * a

Tactic:
rw [← sub_nonneg] at hbc ⊢

Premises used: sub_nonneg
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
rw :
  0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
⊢ 0 ≤ c * a - b * a

Tactic:
rw [← sub_mul, ← leadingCoeff_nonneg_iff, ofLex_mul, leadingCoeff_mul]

Premises used: HahnSeries.leadingCoeff_mul, sub_mul, HahnSeries.leadingCoeff_nonneg_iff, ofLex_mul
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
ha₁ : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
hb : LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
⊢ 0 ≤
    HMul.hMul (α := R) (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))
      (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))

Tactic:
apply mul_nonneg

Premises used: mul_nonneg
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : LinearOrder R
inst_2 : Ring R
inst_3 : AddCommMonoid Γ
inst_4 : IsOrderedCancelAddMonoid Γ
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
ha₁ ha₂ ha₃ ha₄ : 0 ≤ c - b
⊢ LE.le.{u_2} (α := R) 0 (leadingCoeff.{u_1, u_2} (Γ := Γ) ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) (c - b)))

Tactic:
rwa [leadingCoeff_nonneg_iff]

Premises used: HahnSeries.leadingCoeff_nonneg_iff
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
mp :
  (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
              (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
          LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
      Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
        (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 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)) ∨
      a = b
mpr :
  (∃ (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)) ∨
      a = b →
    (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
              (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
          LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
      Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
        (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b))
⊢ (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
              (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
          LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
      Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
        (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 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)) ∨
      a = b

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
contrapose :
  ∀ (hi : i ∉ Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
    ¬LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
        (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) i

Tactic:
contrapose hi
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi : i ∉ Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
⊢ ¬LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)

Tactic:
simp [embDomain_notin_range hi]

Premises used: HahnSeries.embDomain_notin_range
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) i

Tactic:
have himem : i ∈ Set.range f := by
          contrapose hi
          simp [embDomain_notin_range hi]
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
himem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) i
mp :
  ∀ (k : Γ)
    (hj :
      ∀ j < (f : (a : Γ) → Γ') k,
        Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j))
    (hi :
      LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') k))
        (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') k))),
    (∃ (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)) ∨
      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)) ∨
    a = b

Tactic:
obtain ⟨k, rfl⟩ := himem

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj :
  ∀ j < (f : (a : Γ) → Γ') k,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') k))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') k))
⊢ LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) k) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) k)

Tactic:
simpa using hi
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj :
  ∀ j < (f : (a : Γ) → Γ') k,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') k))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') k))
mp :
  ∀ (j : Γ) (hjk : j < k),
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
⊢ (∃ (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)) ∨
    a = b

Tactic:
refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩

Premises used: Or.inl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj :
  ∀ j < (f : (a : Γ) → Γ') k,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') k))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') k))
j : Γ
hjk : j < k
⊢ Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)

Tactic:
simpa using hj (f j) (f.lt_iff_lt.mpr hjk)

Premises used: Iff.mpr, OrderEmbedding.lt_iff_lt, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
heq :
  Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 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)) ∨
    a = b

Tactic:
Or.inr <| embDomain_injective.comp (ofLex.injective) heq

Premises used: HahnSeries.embDomain_injective, Function.Injective.comp, Equiv.injective, ofLex, Or.inr
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
heq :
  Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) 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)) ∨
    a = b

Tactic:
exact Or.inr <| embDomain_injective.comp (ofLex.injective) heq

Premises used: HahnSeries.embDomain_injective, Function.Injective.comp, Equiv.injective, ofLex, Or.inr
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') i))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') i))

Tactic:
simpa using hi
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
mpr :
  ∀ (k : Γ') (hki : k < (f : (a : Γ) → Γ') i),
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
⊢ (∃ (i : Γ'),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
        LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
    Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b))

Tactic:
refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩

Premises used: Or.inl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
k : Γ'
hki : k < (f : (a : Γ) → Γ') i
pos :
  ∀ (hkmem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) k),
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
neg :
  ∀ (hkmem : k ∉ Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)

Tactic:
by_cases hkmem : k ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
k : Γ'
hki : k < (f : (a : Γ) → Γ') i
hkmem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) k
pos :
  ∀ (j' : Γ) (hki : LT.lt.{u_3} (α := Γ') ((f : (a : Γ) → Γ') j' : Γ') ((f : (a : Γ) → Γ') i : Γ')),
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') j'))
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') j'))
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)

Tactic:
obtain ⟨j', rfl⟩ := hkmem

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
j' : Γ
hki : LT.lt.{u_3} (α := Γ') ((f : (a : Γ) → Γ') j' : Γ') ((f : (a : Γ) → Γ') i : Γ')
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') j'))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') j'))

Tactic:
simpa using hj _ <| f.lt_iff_lt.mp hki

Premises used: Iff.mp, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
k : Γ'
hki : k < (f : (a : Γ) → Γ') i
hkmem : k ∉ Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)

Tactic:
simp_rw [embDomain_notin_range hkmem]

Premises used: HahnSeries.embDomain_notin_range
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a : Lex R⟦Γ⟧
⊢ (∃ (i : Γ'),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)) ∧
        LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)) ∨
    Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : AddMonoid R
⊢ Eq (α := Lex R⟦Γ'⟧) (OrderHom.toFun (OrderEmbedding.toOrderHom (embDomainOrderEmbedding f)) 0) 0

Tactic:
simp