awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ a • b ≤ b ↔ a • b ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b
have rw : a • b ≤ b ↔ a • b ≤ 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
⊢ a • b < b ↔ a • b < HSMul.hSMul.{u_1, u_2, u_2} (α := α) 1 b
have rw : a • b < b ↔ a • b < 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₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂
have rw : a • a⁻¹ • b₁ ≤ a • b₂ ↔ b₁ ≤ a • b₂
Tactic: rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
rw : a • a⁻¹ • b₁ ≤ a • b₂ ↔ b₁ ≤ a • b₂
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂
have rw₁ : b₁ ≤ a • b₂ ↔ b₁ ≤ a • b₂
Tactic: rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
have rw : a • b₁ ≤ a • a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
Tactic: rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulMono α β
inst_5 : PosSMulReflectLE α β
ha : 0 < a
rw : a • b₁ ≤ a • a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
have rw₁ : a • b₁ ≤ b₂ ↔ a • b₁ ≤ b₂
Tactic: rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
⊢ a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂
have rw : a • a⁻¹ • b₁ < a • b₂ ↔ b₁ < a • b₂
Tactic: rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
rw : a • a⁻¹ • b₁ < a • b₂ ↔ b₁ < a • b₂
⊢ a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂
have rw₁ : b₁ < a • b₂ ↔ b₁ < a • b₂
Tactic: rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
⊢ b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂
have rw : a • b₁ < a • a⁻¹ • b₂ ↔ a • b₁ < b₂
Tactic: rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : GroupWithZero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : MulAction α β
inst_4 : PosSMulStrictMono α β
inst_5 : PosSMulReflectLT α β
ha : 0 < a
rw : a • b₁ < a • a⁻¹ • b₂ ↔ a • b₁ < b₂
⊢ b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂
have rw₁ : a • b₁ < b₂ ↔ a • b₁ < b₂
Tactic: rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • _b ≤ a₂ • _b
have rw : a₂ • -_b ≤ a₁ • -_b
Tactic: rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b
have rw : a₂ • -_b < a₁ • -_b
Tactic: rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₁ • _b < a₂ • _b
⊢ a₁ < a₂
have h₁ : a₂ • -_b < a₁ • -_b
Tactic: rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Preorder α
inst_1 : Monoid α
inst_2 : AddCommGroup β
inst_3 : PartialOrder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DistribMulAction α β
inst_6 : SMulPosReflectLE α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
h : a₁ • _b ≤ a₂ • _b
⊢ a₁ ≤ a₂
have h₁ : a₂ • -_b ≤ a₁ • -_b
Tactic: rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂
have obtain : ∀ (a : α) (ha₀ : 0 ≤ a) (ha : a₁ ≤ a₁ + a), a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂
Tactic: obtain ⟨a, ha₀, rfl⟩ := exists_nonneg_add_of_le ha
Cleared hypotheses: a₂, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂
have rw : a₁ • b₁ + (a₁ • b₂ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)
Tactic: rw [add_smul, add_smul, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂
have simp_rw : a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁
Tactic: simp_rw [add_comm (a₁ • _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂
have obtain : ∀ (a : α) (ha₀ : 0 < a) (ha : a₁ < a₁ + a), a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂
Tactic: obtain ⟨a, ha₀, rfl⟩ := lt_iff_exists_pos_add.1 ha
Cleared hypotheses: a₂, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂
have rw : a₁ • b₁ + (a₁ • b₂ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)
Tactic: rw [add_smul, add_smul, add_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : ExistsAddOfLE α
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedCancelAddMonoid β
inst_7 : Module α β
inst_8 : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂
have simp_rw : a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁
Tactic: simp_rw [add_comm (a₁ • _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ a • b₂ ≤ a • b₁
have rw : -a • b₁ ≤ -a • b₂
Tactic: rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • _b ≤ a₂ • _b
have rw : 0 ≤ (a₂ - a₁) • _b
Tactic: rw [← sub_nonneg, ← sub_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ a • b₂ < a • b₁
have rw : -a • b₁ < -a • b₂
Tactic: rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁_1 a₂_1 : α
b b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b
have rw : 0 < (a₂ - a₁) • _b
Tactic: rw [← sub_pos, ← sub_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
⊢ b₂ ≤ b₁
have h₁ : -a • b₂ ≤ -a • b₁
Tactic: rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : a ≤ 0
⊢ b₂ < b₁
have h₁ : -a • b₂ < -a • b₁
Tactic: rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulMono α β
inst_8 : PosSMulReflectLE α β
ha : a < 0
⊢ a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁
have rw : -a • b₂ ≤ -a • b₁ ↔ b₂ ≤ b₁
Tactic: rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : AddCommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
inst_8 : PosSMulReflectLT α β
ha : a < 0
⊢ a • b₁ < a • b₂ ↔ b₂ < b₁
have rw : -a • b₂ < -a • b₁ ↔ b₂ < b₁
Tactic: rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
have simp : (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
Tactic: simp only [Decidable.or_iff_not_not_and_not, not_and, not_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
have refine : ∀ (ab : 0 ≤ a → b < 0) (nab : a ≤ 0 → 0 < b), a • b < 0
Tactic: refine fun ab nab ↦ hab.not_gt ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a • b < 0
have inl : ∀ (ha : 0 < a), a • b < 0
Tactic: obtain ha | rfl | ha := lt_trichotomy 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
inl : ∀ (ha : 0 < a), a • b < 0
⊢ a • b < 0
have inr : ∀ (hab : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b) (ab : LE.le.{u_1} (α := α) 0 0 → b < 0)
  (nab : LE.le.{u_1} (α := α) 0 0 → 0 < b), HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b < 0
Tactic: obtain ha | rfl | ha := lt_trichotomy 0 a
Cleared hypotheses: a, hab, ab, nab
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
inl : ∀ (ha : 0 < a), a • b < 0
inr :
  ∀ (hab : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b) (ab : LE.le.{u_1} (α := α) 0 0 → b < 0)
    (nab : LE.le.{u_1} (α := α) 0 0 → 0 < b), HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 b < 0
⊢ a • b < 0
have inr₁ : ∀ (ha : a < 0), a • b < 0
Tactic: obtain ha | rfl | ha := lt_trichotomy 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw : 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₁ : 0 ≤ a • -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a • -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a • -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₃ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
rw : 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a • -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₃ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₄ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
have rw : (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Tactic: rw [← neg_smul_neg, smul_nonneg_iff_pos_imp_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
have rw : (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
Tactic: rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module α β
inst_7 : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
have rw : (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Tactic: rw [← neg_nonneg, ← neg_smul, smul_nonneg_iff_pos_imp_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂
have inl : ∀ (h₁ : 0.1 < _b.1), _a₁ ≤ _a₂
Tactic: rcases lt_iff.mp hb with ⟨h₁, -⟩ | ⟨-, h₁⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : Preorder γ
inst_4 : SMul α β
inst_5 : SMul α γ
inst_6 : Zero β
inst_7 : Zero γ
inst_8 : SMulPosReflectLE α β
inst_9 : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
inl : ∀ (h₁ : 0.1 < _b.1), _a₁ ≤ _a₂
⊢ _a₁ ≤ _a₂
have inr : ∀ (h₁ : 0.2 < _b.2), _a₁ ≤ _a₂
Tactic: rcases lt_iff.mp hb with ⟨h₁, -⟩ | ⟨-, h₁⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : PosSMulStrictMono α β
inst_9 : PosSMulStrictMono α γ
⊢ ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : β × γ⦄ (hb : b₁ < b₂), a • b₁ < a • b₂
have simp_rw : ∀ ⦃a : α⦄ (ha : 0 < a) ⦃b₁ b₂ : β × γ⦄ (hb : b₁.1 < b₂.1 ∧ b₁.2 ≤ b₂.2 ∨ b₁.1 ≤ b₂.1 ∧ b₁.2 < b₂.2),
  (a • b₁).1 < (a • b₂).1 ∧ (a • b₁).2 ≤ (a • b₂).2 ∨ (a • b₁).1 ≤ (a • b₂).1 ∧ (a • b₁).2 < (a • b₂).2
Tactic: simp_rw [lt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosStrictMono α β
inst_9 : SMulPosStrictMono α γ
⊢ ∀ ⦃b : β × γ⦄ (hb : 0 < b) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂), a₁ • b < a₂ • b
have simp_rw : ∀ ⦃b : β × γ⦄ (hb : 0.1 < b.1 ∧ 0.2 ≤ b.2 ∨ 0.1 ≤ b.1 ∧ 0.2 < b.2) ⦃a₁ a₂ : α⦄ (ha : a₁ < a₂),
  (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2
Tactic: simp_rw [lt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst : Zero α
inst_1 : PartialOrder α
inst_2 : PartialOrder β
inst_3 : PartialOrder γ
inst_4 : Zero β
inst_5 : Zero γ
inst_6 : SMulWithZero α β
inst_7 : SMulWithZero α γ
inst_8 : SMulPosReflectLT α β
inst_9 : SMulPosReflectLT α γ
⊢ ∀ ⦃b : β × γ⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄ (hb : a₁ • b < a₂ • b), a₁ < a₂
have simp_rw : ∀ ⦃b : β × γ⦄ (hb : 0 ≤ b) ⦃a₁ a₂ : α⦄
  (hb : (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2), a₁ < a₂
Tactic: simp_rw [lt_iff]
-- 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 : Preorder α
inst_2 : (i : ι) → Preorder (β i)
inst_3 : (i : ι) → SMul.{u_1, u_4} α (β i)
inst_4 : (i : ι) → Zero (β i)
inst_5 : ∀ (i : ι), SMulPosReflectLE.{u_1, u_4} α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂
have obtain : ∀ (i : ι) (hi : 0 i < _b i), _a₁ ≤ _a₂
Tactic: obtain ⟨-, i, hi⟩ := lt_def.1 hb