awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
smul₁ : ∀ (a : α) (b : β), True
zero₁ : True
⊢ 0 < f b

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
smul₁ : ∀ (a : α) (b : β), True
zero₁ : True
hb₁ : 0 < f b
⊢ a₁ • f b ≤ a₂ • f b

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
h : a₁ • f b ≤ a₂ • f b
⊢ a₁ ≤ a₂

Tactic:
le_of_smul_le_smul_right h hb

Premises used: le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLE α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
h : a₁ • f b ≤ a₂ • f b
⊢ a₁ ≤ a₂

Tactic:
exact le_of_smul_le_smul_right h hb

Premises used: le_of_smul_le_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ ∀ {b₁ b₂ : β}, True

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
⊢ ∀ (a : α) (b : β), True

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
smul₁ : ∀ (a : α) (b : β), True
⊢ True

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
smul₁ : ∀ (a : α) (b : β), True
zero₁ : True
⊢ 0 ≤ f b

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hf₁ : ∀ {b₁ b₂ : β}, True
smul₁ : ∀ (a : α) (b : β), True
zero₁ : True
hb₁ : 0 ≤ f b
⊢ a₁ • f b < a₂ • f b

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
h : a₁ • f b < a₂ • f b
⊢ a₁ < a₂

Tactic:
lt_of_smul_lt_smul_right h hb

Premises used: lt_of_smul_lt_smul_right
-- Module: Mathlib.Algebra.Order.Module.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : SMul α β
inst_4 : SMul α γ
f : β → γ
inst_5 : Zero β
inst_6 : Zero γ
inst_7 : SMulPosReflectLT α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
h : a₁ • f b < a₂ • f b
⊢ a₁ < a₂

Tactic:
exact lt_of_smul_lt_smul_right h hb

Premises used: lt_of_smul_lt_smul_right
-- Module: Mathlib.Algebra.Order.Module.Equiv
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
⊢ Eq (α := (a : β) → Lex β) (⇑(toLexLinearEquiv α β) : (a : β) → Lex β) (⇑toLex : (a : β) → Lex β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.Equiv
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
⊢ Eq (α := (a : Lex β) → β) (⇑(ofLexLinearEquiv α β) : (a : Lex β) → β) (⇑ofLex : (a : Lex β) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Module.Equiv
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
⊢ Eq (α := Lex β ≃ₗ[α] β) (LinearEquiv.symm (toLexLinearEquiv α β)) (ofLexLinearEquiv α β)

Tactic:
rfl

Premises used: LinearEquiv.symm, Lex, ofLexLinearEquiv, AddEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Order.Module.Equiv
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
⊢ Eq (α := β ≃ₗ[α] Lex β) (LinearEquiv.symm (ofLexLinearEquiv α β)) (toLexLinearEquiv α β)

Tactic:
rfl

Premises used: toLexLinearEquiv, LinearEquiv.symm, Lex, AddEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
𝕜 : Type u_1
G : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup G
inst_4 : PartialOrder G
inst_5 : MulAction 𝕜 G
inst_6 : PosSMulMono 𝕜 G
_a : 𝕜
ha : 0 < _a
b₁ b₂ : G
h : _a • b₁ ≤ _a • b₂
⊢ b₁ ≤ b₂

Tactic:
simpa [ha.ne'] using smul_le_smul_of_nonneg_left h <| inv_nonneg.2 ha.le

Premises used: Iff.mpr, LT.lt.le, LT.lt.ne', inv_nonneg, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
𝕜 : Type u_1
G : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup G
inst_4 : PartialOrder G
inst_5 : MulActionWithZero 𝕜 G
inst_6 : PosSMulStrictMono 𝕜 G
a : 𝕜
ha : 0 < a
b₁ b₂ : G
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha

Premises used: Iff.mpr, inv_pos, LT.lt.ne', smul_lt_smul_of_pos_left
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
𝕜 : Type u_1
G : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup G
inst_4 : PartialOrder G
inst_5 : IsOrderedAddMonoid G
inst_6 : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst_7 : PosSMulMono 𝕜 G
h : a < 0
rw : a • b₂ ≤ a • a⁻¹ • b₁ ↔ a • b₂ ≤ b₁
rw₁ rw₂ : a • b₂ ≤ b₁ ↔ a • b₂ ≤ b₁
⊢ a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁

Tactic:
rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Premises used: smul_inv_smul₀, smul_le_smul_iff_of_neg_left, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
𝕜 : Type u_1
G : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup G
inst_4 : PartialOrder G
inst_5 : IsOrderedAddMonoid G
inst_6 : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst_7 : PosSMulMono 𝕜 G
h : a < 0
rw : a • a⁻¹ • b₂ ≤ a • b₁ ↔ b₂ ≤ a • b₁
rw₁ rw₂ : b₂ ≤ a • b₁ ↔ b₂ ≤ a • b₁
⊢ b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁

Tactic:
rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Premises used: smul_inv_smul₀, smul_le_smul_iff_of_neg_left, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
𝕜 : Type u_1
G : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup G
inst_4 : PartialOrder G
inst_5 : IsOrderedAddMonoid G
inst_6 : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst_7 : PosSMulStrictMono 𝕜 G
h : a < 0
rw : a • b₂ < a • a⁻¹ • b₁ ↔ a • b₂ < b₁
rw₁ rw₂ : a • b₂ < b₁ ↔ a • b₂ < b₁
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

Tactic:
rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Premises used: smul_inv_smul₀, smul_lt_smul_iff_of_neg_left, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
𝕜 : Type u_1
G : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup G
inst_4 : PartialOrder G
inst_5 : IsOrderedAddMonoid G
inst_6 : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst_7 : PosSMulStrictMono 𝕜 G
h : a < 0
rw : a • a⁻¹ • b₂ < a • b₁ ↔ b₂ < a • b₁
rw₁ rw₂ : b₂ < a • b₁ ↔ b₂ < a • b₁
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

Tactic:
rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Premises used: smul_inv_smul₀, smul_lt_smul_iff_of_neg_left, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
a : α
b : β
ha : 0 < a
hb : 0 ≤ b
⊢ 0 ≤ a • b

Tactic:
smul_nonneg ha.le hb

Premises used: smul_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
a : α
b : β
ha : 0 ≤ a
hb : 0 < b
⊢ 0 ≤ a • b

Tactic:
smul_nonneg ha hb.le

Premises used: smul_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Zero β
inst_2 : SMulZeroClass α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : PosSMulMono α β
a : α
b : β
ha : 0 < a
hb : 0 < b
⊢ 0 ≤ a • b

Tactic:
smul_nonneg ha.le hb.le

Premises used: smul_nonneg, LT.lt.le
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
α : Type u_3
β : Type u_4
inst : Semiring α
inst_1 : IsDomain α
inst_2 : AddCommMonoid β
inst_3 : _root_.Module α β
inst_4 : Module.IsTorsionFree α β
a : α
b : β
inst_5 : Preorder α
ha : 0 < a
hb : b ≠ 0
⊢ a • b ≠ 0

Tactic:
smul_ne_zero ha.ne' hb

Premises used: smul_ne_zero, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Module.Field
Goal:
α : Type u_3
β : Type u_4
inst : Semiring α
inst_1 : IsDomain α
inst_2 : AddCommMonoid β
inst_3 : _root_.Module α β
inst_4 : Module.IsTorsionFree α β
a : α
b : β
inst_5 : Preorder β
ha : a ≠ 0
hb : 0 < b
⊢ a • b ≠ 0

Tactic:
smul_ne_zero ha hb.ne'

Premises used: smul_ne_zero, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ ∀ (c : FiniteArchimedeanClass M), ∃ (G : Submodule K M), Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c

Tactic:
have hstratum (c : FiniteArchimedeanClass M) :
      ∃ G : Submodule K M, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c :=
    IsModularLattice.exists_disjoint_and_sup_eq (ball_lt_closedBall _).le
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
hstratum :
  ∀ (c : FiniteArchimedeanClass M), ∃ (G : Submodule K M), Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c
choose :
  ∀ (g : (c : FiniteArchimedeanClass M) → Submodule K M)
    (h1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (ball K c) (g c))
    (h2 : ∀ (c : FiniteArchimedeanClass M), ball K c ⊔ g c = closedBall K c), Nonempty.{u_2 + 1} (ArchimedeanStrata K M)
⊢ Nonempty.{u_2 + 1} (ArchimedeanStrata K M)

Tactic:
choose g h1 h2 using hstratum
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
g : (c : FiniteArchimedeanClass M) → Submodule K M
h1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (ball K c) (g c)
h2 : ∀ (c : FiniteArchimedeanClass M), ball K c ⊔ g c = closedBall K c
⊢ Nonempty.{u_2 + 1} (ArchimedeanStrata K M)

Tactic:
⟨g, h1, h2⟩

Premises used: Nonempty.intro, HahnEmbedding.ArchimedeanStrata.mk
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
g : (c : FiniteArchimedeanClass M) → Submodule K M
h1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (ball K c) (g c)
h2 : ∀ (c : FiniteArchimedeanClass M), ball K c ⊔ g c = closedBall K c
⊢ Nonempty.{u_2 + 1} (ArchimedeanStrata K M)

Tactic:
exact ⟨g, h1, h2⟩
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
eq : u.stratum c = ⊥
⊢ LT.lt (α := Submodule K M) (ball K c ⊔ ⊥) (closedBall K c)

Tactic:
simpa using ball_lt_closedBall _

Premises used: FiniteArchimedeanClass.ball_lt_closedBall
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Nontrivial.{u_2} ↥(u.stratum c)

Tactic:
(Submodule.nontrivial_iff_ne_bot).mpr (stratum_ne_bot _)

Premises used: Iff.mpr, Submodule.nontrivial_iff_ne_bot, HahnEmbedding.ArchimedeanStrata.stratum_ne_bot
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
a₁ : ArchimedeanClass.mk a ≤ (↑c : ArchimedeanClass M)
a₂ : (↑c : ArchimedeanClass M) ≤ ArchimedeanClass.mk a
⊢ ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
a₁ : ∀ (hlt : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk a), a = 0
⊢ ArchimedeanClass.mk a ≤ (↑c : ArchimedeanClass M)

Tactic:
contrapose! h0 with hlt
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
hlt : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk a
⊢ Membership.mem (γ := Submodule K M) (ball K c) a

Tactic:
have ha' : a ∈ ball K c := (mem_ball_iff K).mpr fun _ ↦ hlt
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
hlt : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk a
ha' : Membership.mem (γ := Submodule K M) (ball K c) a
⊢ a = 0

Tactic:
(Submodule.disjoint_def.mp (u.disjoint_ball_stratum _)) _ ha' ha

Premises used: HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum, Iff.mp, Submodule.disjoint_def
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
hlt : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk a
ha' : Membership.mem (γ := Submodule K M) (ball K c) a
⊢ a = 0

Tactic:
exact (Submodule.disjoint_def.mp (u.disjoint_ball_stratum _)) _ ha' ha

Premises used: HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum, Iff.mp, Submodule.disjoint_def
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
apply : Membership.mem (γ := Submodule K M) (closedBall K c) a
⊢ (↑c : ArchimedeanClass M) ≤ ArchimedeanClass.mk a

Tactic:
apply (mem_closedBall_iff K).mp _ h0

Premises used: Iff.mp, FiniteArchimedeanClass.mem_closedBall_iff
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
rw : a ∈ ball K c ⊔ u.stratum c
⊢ Membership.mem (γ := Submodule K M) (closedBall K c) a

Tactic:
rw [← u.ball_sup_stratum_eq c]

Premises used: HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
⊢ a ∈ ball K c ⊔ u.stratum c

Tactic:
Submodule.mem_sup_right ha

Premises used: Submodule.mem_sup_right
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
⊢ a ∈ ball K c ⊔ u.stratum c

Tactic:
exact Submodule.mem_sup_right ha

Premises used: Submodule.mem_sup_right
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
h :
  ∀ (a : ↥(u.stratum c)),
    a ≠ 0 →
      ∀ (b : ↥(u.stratum c)),
        b ≠ 0 → Eq (α := ArchimedeanClass ↥(u.stratum c)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)
⊢ Archimedean.{u_2} ↥(u.stratum c)

Tactic:
apply ArchimedeanClass.archimedean_of_mk_eq_mk

Premises used: ArchimedeanClass.archimedean_of_mk_eq_mk
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑a : M)) (ArchimedeanClass.mk (↑b : M))
rw :
  ∀ (this : (∃ (m : ℕ), |(↑b : M)| ≤ m • |(↑a : M)|) ∧ ∃ (n : ℕ), |(↑a : M)| ≤ n • |(↑b : M)|),
    (∃ (m : ℕ), |b| ≤ m • |a|) ∧ ∃ (n : ℕ), |a| ≤ n • |b|
⊢ Eq (α := ArchimedeanClass ↥(u.stratum c)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)

Tactic:
rw [ArchimedeanClass.mk_eq_mk] at this ⊢

Premises used: ArchimedeanClass.mk_eq_mk
-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : (∃ (m : ℕ), |(↑b : M)| ≤ m • |(↑a : M)|) ∧ ∃ (n : ℕ), |(↑a : M)| ≤ n • |(↑b : M)|
⊢ (∃ (m : ℕ), |b| ≤ m • |a|) ∧ ∃ (n : ℕ), |a| ≤ n • |b|

Tactic:
this

Premises used: abs