awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
rw₁ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊓ y + x ⊓ y)
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)
have rw₂ : x ⊓ y =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊓ y))
Tactic: rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
rw₁ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊓ y + x ⊓ y)
rw₂ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊓ y))
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)
have rw₃ : x ⊓ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊓ y)
Tactic: rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
rw₁ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊓ y + x ⊓ y)
rw₂ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊓ y))
rw₃ : x ⊓ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊓ y)
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)
have rw₄ : x ⊓ y = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (x ⊓ y)
Tactic: rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊓ y))
rw₁ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊓ y + x ⊓ y)
rw₂ :
  x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊓ y))
rw₃ : x ⊓ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊓ y)
rw₄ : x ⊓ y = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (x ⊓ y)
⊢ x ⊓ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y - |y - x|)
have rw₅ : x ⊓ y = x ⊓ y
Tactic: rw [← two_nsmul_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)
have rw : x ⊔ y =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
Tactic: rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)
have rw₁ : x ⊔ y =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊔ y + x ⊔ y)
Tactic: rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
rw₁ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊔ y + x ⊔ y)
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)
have rw₂ : x ⊔ y =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊔ y))
Tactic: rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
rw₁ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊔ y + x ⊔ y)
rw₂ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊔ y))
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)
have rw₃ : x ⊔ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊔ y)
Tactic: rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
rw₁ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊔ y + x ⊔ y)
rw₂ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊔ y))
rw₃ : x ⊔ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊔ y)
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)
have rw₄ : x ⊔ y = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (x ⊔ y)
Tactic: rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Invertible (α := R) 2
inst_2 : Lattice M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : IsOrderedAddMonoid M
x y : M
rw :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℕ) 2 (x ⊔ y))
rw₁ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (x ⊔ y + x ⊔ y)
rw₂ :
  x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2 (x ⊔ y))
rw₃ : x ⊔ y = HMul.hMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 • (x ⊔ y)
rw₄ : x ⊔ y = HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 (x ⊔ y)
⊢ x ⊔ y =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (x + y + |y - x|)
have rw₅ : x ⊔ y = x ⊔ y
Tactic: rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
⊢ |a • b| = |a| • |b|
have inl : ∀ (ha : a ≤ 0), |a • b| = |a| • |b|
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
inl : ∀ (ha : a ≤ 0), |a • b| = |a| • |b|
⊢ |a • b| = |a| • |b|
have inr : ∀ (ha : 0 ≤ a), |a • b| = |a| • |b|
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
⊢ |a • b| = |a| • |b|
have inl : ∀ (hb : b ≤ 0), |a • b| = |a| • |b|
Tactic: obtain hb | hb := le_total b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
inl : ∀ (hb : b ≤ 0), |a • b| = |a| • |b|
⊢ |a • b| = |a| • |b|
have inl₁ : ∀ (hb : 0 ≤ b), |a • b| = |a| • |b|
Tactic: obtain hb | hb := le_total b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
⊢ |a • b| = |a| • |b|
have inr : ∀ (hb : b ≤ 0), |a • b| = |a| • |b|
Tactic: obtain hb | hb := le_total b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommGroup M
inst_4 : LinearOrder M
inst_5 : IsOrderedAddMonoid M
inst_6 : Module R M
inst_7 : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
inr : ∀ (hb : b ≤ 0), |a • b| = |a| • |b|
⊢ |a • b| = |a| • |b|
have inr₁ : ∀ (hb : 0 ≤ b), |a • b| = |a| • |b|
Tactic: obtain hb | hb := le_total b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : MulOneClass β
inst_6 : PosMulMono β
inst_7 : MulPosMono β
inst_8 : IsScalarTower α β β
h : Monotone.{u_1, u_2} (β := β) fun (x : α) ↦ HSMul.hSMul (β := β) x 1
x : α
ha : 0 ≤ x
x_1 x_2 : β
hb : x_1 ≤ x_2
⊢ x • x_1 ≤ x • x_2
have this : HSMul.hSMul (β := β) x 1 * x_1 ≤ HSMul.hSMul (β := β) x 1 * x_2
Tactic: have := mul_le_mul_of_nonneg_left hb (by simpa using h ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂
have inl : ∀ (ha : 0 = a), a • b₁ ≤ a • b₂
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
inl : ∀ (ha : 0 = a), a • b₁ ≤ a • b₂
⊢ a • b₁ ≤ a • b₂
have inr : ∀ (ha : 0 < a), a • b₁ ≤ a • b₂
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂
have inl : ∀ (ha : 0 = a), b₁ < b₂
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
inl : ∀ (ha : 0 = a), b₁ < b₂
⊢ b₁ < b₂
have inr : ∀ (ha : 0 < a), b₁ < b₂
Tactic: obtain ha | ha := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b
have inl : ∀ (hb : 0 = b), a₁ • b ≤ a₂ • b
Tactic: obtain hb | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
inl : ∀ (hb : 0 = b), a₁ • b ≤ a₂ • b
⊢ a₁ • b ≤ a₂ • b
have inr : ∀ (hb : 0 < b), a₁ • b ≤ a₂ • b
Tactic: obtain hb | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂
have inl : ∀ (hb : 0 = b), a₁ < a₂
Tactic: obtain hb | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : Preorder α
inst_4 : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
inl : ∀ (hb : 0 = b), a₁ < a₂
⊢ a₁ < a₂
have inr : ∀ (hb : 0 < b), a₁ < a₂
Tactic: obtain hb | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
⊢ a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
have refine : ∀ (h : a₁ • b₁ = a₂ • b₂), a₁ = a₂ ∧ b₁ = b₂
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
⊢ a₁ = a₂ ∧ b₁ = b₂
have simp : ¬a₁ < a₂ ∧ ¬b₁ < b₂
Tactic: simp only [eq_iff_le_not_lt, ha, hb, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
have refine_1 : ∀ (ha : a₁ < a₂), a₁ • b₁ < a₂ • b₂
Tactic: refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
refine_1 : ∀ (ha : a₁ < a₂), a₁ • b₁ < a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
have refine_2 : ∀ (hb : b₁ < b₂), a₁ • b₁ < a₂ • b₂
Tactic: refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
⊢ a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
have refine : ∀ (h : a₁ • b₁ = a₂ • b₂), a₁ = a₂ ∧ b₁ = b₂
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
⊢ a₁ = a₂ ∧ b₁ = b₂
have simp : ¬a₁ < a₂ ∧ ¬b₁ < b₂
Tactic: simp only [eq_iff_le_not_lt, ha, hb, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
have refine_1 : ∀ (ha : a₁ < a₂), a₁ • b₁ < a₂ • b₂
Tactic: refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : PartialOrder α
inst_4 : PartialOrder β
inst_5 : PosSMulStrictMono α β
inst_6 : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
refine_1 : ∀ (ha : a₁ < a₂), a₁ • b₁ < a₂ • b₂
⊢ ¬a₁ < a₂ ∧ ¬b₁ < b₂
have refine_2 : ∀ (hb : b₁ < b₂), a₁ • b₁ < a₂ • b₂
Tactic: refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Tactic: obtain ha | rfl | ha := lt_trichotomy a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inr : ∀ (hab : 0 < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b),
  LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
Tactic: obtain ha | rfl | ha := lt_trichotomy a 0
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
inl : ∀ (ha : a < 0), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
inr :
  ∀ (hab : 0 < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b),
    LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inr₁ : ∀ (ha : 0 < a), 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Tactic: obtain ha | rfl | ha := lt_trichotomy a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inl : ∀ (hb : 0 ≤ b), a • b ≤ 0
Tactic: refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b
⊢ LT.lt.{u_1} (α := α) 0 0 ∧ 0 < b ∨ LT.lt.{u_1} (α := α) 0 0 ∧ b < 0
have hab₁ : LT.lt.{u_2} (α := β) 0 0
Tactic: rw [zero_smul] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
inst_3 : LinearOrder α
inst_4 : LinearOrder β
inst_5 : PosSMulMono α β
inst_6 : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have inr : ∀ (hb : b ≤ 0), a • b ≤ 0
Tactic: refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosMono α β
inst_6 : SMulPosReflectLE α β
hb : 0 < b
⊢ b ≤ a • b ↔ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b ≤ a • b
have rw : b ≤ a • b ↔ b ≤ a • b
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
inst : Monoid α
inst_1 : Zero β
inst_2 : MulAction α β
inst_3 : Preorder α
inst_4 : Preorder β
inst_5 : SMulPosStrictMono α β
inst_6 : SMulPosReflectLT α β
hb : 0 < b
⊢ b < a • b ↔ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b < a • b
have rw : b < a • b ↔ b < a • b
Tactic: rw [one_smul]