awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), PosSMulStrictMono.{u_1, u_4} α (β i)
⊢ ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : (i : ι) → β i⦄ (hb : b₁ < b₂), a • b₁ < a • b₂
have simp_rw : ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : (i : ι) → β i⦄ (hb : b₁ ≤ b₂ ∧ ∃ (i : ι), b₁ i < b₂ i),
  a • b₁ ≤ a • b₂ ∧ ∃ (i : ι), (a • b₁) i < (a • b₂) i
Tactic: simp_rw [lt_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosStrictMono.{u_1, u_4} α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 < b) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂), a₁ • b < a₂ • b
have simp_rw : ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 ≤ b ∧ ∃ (i : ι), 0 i < b i) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂),
  a₁ • b ≤ a₂ • b ∧ ∃ (i : ι), (a₁ • b) i < (a₂ • b) i
Tactic: simp_rw [lt_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β_1 : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β_1
ι : Type u_3
β : ι → Type u_4
inst : Zero α
inst_1 : (i : ι) → Zero (β i)
inst_2 : PartialOrder α
inst_3 : (i : ι) → PartialOrder (β i)
inst_4 : (i : ι) → SMulWithZero.{u_1, u_4} α (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLT.{u_1, u_4} α (β i)
⊢ ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (hb : a₁ • b < a₂ • b), a₁ < a₂
have simp_rw : ∀ ⦃b : (i : ι) → β i⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (hb : a₁ • b ≤ a₂ • b ∧ ∃ (i : ι), (a₁ • b) i < (a₂ • b) i), a₁ < a₂
Tactic: simp_rw [lt_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
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 : PosSMulMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
hb : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂
have simp : ∀ (hf : ∀ {b₁ b₂ : β}, True) (smul : ∀ (a : α) (b : β), True) (hb : f b₁ ≤ f b₂), a • f b₁ ≤ a • f b₂
Tactic: simp only [← hf, smul] at *
Cleared hypotheses: hf, smul, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
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 : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
hb : b₁ < b₂
⊢ a • b₁ < a • b₂
have simp : ∀ (smul : ∀ (a : α) (b : β), True) (hb : f b₁ < f b₂), a • f b₁ < a • f b₂
Tactic: simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *
Cleared hypotheses: smul, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
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 : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂
have simp : ∀ (smul : ∀ (a : α) (b : β), True) (h : a • f b₁ < a • f b₂), f b₁ < f b₂
Tactic: simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *
Cleared hypotheses: smul, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
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 : SMulPosMono α γ
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₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b
have simp : ∀ (hf : ∀ {b₁ b₂ : β}, True) (smul : ∀ (a : α) (b : β), True) (zero : True) (hb : 0 ≤ f b), a₁ • f b ≤ a₂ • f b
Tactic: simp only [← hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
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 : SMulPosStrictMono α γ
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₂ : α
ha : a₁ < a₂
⊢ a₁ • b < a₂ • b
have simp : ∀ (smul : ∀ (a : α) (b : β), True) (zero : True) (hb : 0 < f b), a₁ • f b < a₂ • f b
Tactic: simp only [← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: smul, zero, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ ≤ a₂
have hf₁ : ∀ {b₁ b₂ : β}, True
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ ≤ a₂
have smul₁ : ∀ (a : α) (b : β), True
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ ≤ a₂
have zero₁ : True
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ ≤ a₂
have hb₁ : 0 < f b
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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₁ ≤ a₂
have h₁ : a₁ • f b ≤ a₂ • f b
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ < a₂
have hf₁ : ∀ {b₁ b₂ : β}, True
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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₁ < a₂
have smul₁ : ∀ (a : α) (b : β), True
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ < a₂
have zero₁ : True
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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
⊢ a₁ < a₂
have hb₁ : 0 ≤ f b
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
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₁ < a₂
have h₁ : a₁ • f b < a₂ • f b
Tactic: simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
Cleared hypotheses: hf, smul, zero, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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
⊢ a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁
have rw : a • b₂ ≤ a • a⁻¹ • b₁ ↔ a • b₂ ≤ b₁
Tactic: rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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₁
⊢ a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁
have rw₁ : a • b₂ ≤ b₁ ↔ a • b₂ ≤ b₁
Tactic: rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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
⊢ b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁
have rw : a • a⁻¹ • b₂ ≤ a • b₁ ↔ b₂ ≤ a • b₁
Tactic: rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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₁
⊢ b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁
have rw₁ : b₂ ≤ a • b₁ ↔ b₂ ≤ a • b₁
Tactic: rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁
have rw : a • b₂ < a • a⁻¹ • b₁ ↔ a • b₂ < b₁
Tactic: rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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₁
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁
have rw₁ : a • b₂ < b₁ ↔ a • b₂ < b₁
Tactic: rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁
have rw : a • a⁻¹ • b₂ < a • b₁ ↔ b₂ < a • b₁
Tactic: rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Field (goal)
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₁
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁
have rw₁ : b₂ < a • b₁ ↔ b₂ < a • b₁
Tactic: rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ Nonempty.{u_2 + 1} (ArchimedeanStrata K M)
have hstratum : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ Nonempty.{u_2 + 1} (ArchimedeanStrata K M)
have 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)
Tactic: choose g h1 h2 using hstratum
Cleared hypotheses: hstratum
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)
have a₁ : ArchimedeanClass.mk a ≤ (↑c : ArchimedeanClass M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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)
⊢ ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)
have a₂ : (↑c : ArchimedeanClass M) ≤ ArchimedeanClass.mk a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ ArchimedeanClass.mk a ≤ (↑c : ArchimedeanClass M)
have a₁ : ∀ (hlt : (↑c : ArchimedeanClass M) < ArchimedeanClass.mk a), a = 0
Tactic: contrapose! h0 with hlt
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ a = 0
have ha' : Membership.mem (γ := Submodule K M) (ball K c) a
Tactic: have ha' : a ∈ ball K c := (mem_ball_iff K).mpr fun _ ↦ hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ (↑c : ArchimedeanClass M) ≤ ArchimedeanClass.mk a
have apply : Membership.mem (γ := Submodule K M) (closedBall K c) a
Tactic: apply (mem_closedBall_iff K).mp _ h0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ Membership.mem (γ := Submodule K M) (closedBall K c) a
have rw : a ∈ ball K c ⊔ u.stratum c
Tactic: rw [← u.ball_sup_stratum_eq c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ Archimedean.{u_2} ↥(u.stratum c)
have h : ∀ (a : ↥(u.stratum c)),
  a ≠ 0 →
    ∀ (b : ↥(u.stratum c)),
      b ≠ 0 → Eq (α := ArchimedeanClass ↥(u.stratum c)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)
Tactic: apply ArchimedeanClass.archimedean_of_mk_eq_mk
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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))
⊢ Eq (α := ArchimedeanClass ↥(u.stratum c)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)
have rw : ∀ (this : (∃ (m : ℕ), |(↑b : M)| ≤ m • |(↑a : M)|) ∧ ∃ (n : ℕ), |(↑a : M)| ≤ n • |(↑b : M)|),
  (∃ (m : ℕ), |b| ≤ m • |a|) ∧ ∃ (n : ℕ), |a| ≤ n • |b|
Tactic: rw [ArchimedeanClass.mk_eq_mk] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ Eq (α := ArchimedeanClass ↥(u.stratum c)) (ArchimedeanClass.mk a) (ArchimedeanClass.mk b)
have h : Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑a : M)) (ArchimedeanClass.mk (↑b : M))
Tactic: suffices ArchimedeanClass.mk a.val = ArchimedeanClass.mk b.val by
    rw [ArchimedeanClass.mk_eq_mk] at this ⊢
    exact this
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑a : M)) (ArchimedeanClass.mk (↑b : M))
have h : (↑c : ArchimedeanClass M) = ArchimedeanClass.mk (↑b : M)
Tactic: rw [u.archimedeanClassMk_of_mem_stratum a.prop (by simpa using ha)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ (↑c : ArchimedeanClass M) = ArchimedeanClass.mk (↑b : M)
have h : (↑c : ArchimedeanClass M) = (↑c : ArchimedeanClass M)
Tactic: rw [u.archimedeanClassMk_of_mem_stratum b.prop (by simpa using hb)]