awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / - -c ↔ b < a * - -c
⊢ a < b / c ↔ b < a * c
have rw₁ : a < b / - -c ↔ b < -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / - -c ↔ b < a * - -c
rw₁ : a < b / - -c ↔ b < -(a * -c)
⊢ a < b / c ↔ b < a * c
have rw₂ : a < -(b / -c) ↔ b < -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / - -c ↔ b < a * - -c
rw₁ : a < b / - -c ↔ b < -(a * -c)
rw₂ : a < -(b / -c) ↔ b < -(a * -c)
⊢ a < b / c ↔ b < a * c
have rw₃ : b / -c < -a ↔ b < -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / - -c ↔ b < a * - -c
rw₁ : a < b / - -c ↔ b < -(a * -c)
rw₂ : a < -(b / -c) ↔ b < -(a * -c)
rw₃ : b / -c < -a ↔ b < -(a * -c)
⊢ a < b / c ↔ b < a * c
have rw₄ : b < -a * -c ↔ b < -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / - -c ↔ b < a * - -c
rw₁ : a < b / - -c ↔ b < -(a * -c)
rw₂ : a < -(b / -c) ↔ b < -(a * -c)
rw₃ : b / -c < -a ↔ b < -(a * -c)
rw₄ : b < -a * -c ↔ b < -(a * -c)
⊢ a < b / c ↔ b < a * c
have rw₅ : b < -(a * -c) ↔ b < -(a * -c)
Tactic: rw [← neg_neg c, mul_neg, div_neg, lt_neg, div_lt_iff₀ (neg_pos.2 hc), neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a < b / c ↔ b < c * a
have rw : a < b / c ↔ b < a * c
Tactic: rw [mul_comm, lt_div_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : a < b / c ↔ b < a * c
⊢ a < b / c ↔ b < c * a
have rw₁ : b < a * c ↔ b < a * c
Tactic: rw [mul_comm, lt_div_iff_of_neg hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw : 1 / a ≤ b⁻¹ ↔ b ≤ a
Tactic: rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : 1 / a ≤ b⁻¹ ↔ b ≤ a
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw₁ : b⁻¹ * a ≤ 1 ↔ b ≤ a
Tactic: rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : 1 / a ≤ b⁻¹ ↔ b ≤ a
rw₁ : b⁻¹ * a ≤ 1 ↔ b ≤ a
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw₂ : a / b ≤ 1 ↔ b ≤ a
Tactic: rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : 1 / a ≤ b⁻¹ ↔ b ≤ a
rw₁ : b⁻¹ * a ≤ 1 ↔ b ≤ a
rw₂ : a / b ≤ 1 ↔ b ≤ a
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw₃ : 1 * b ≤ a ↔ b ≤ a
Tactic: rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : 1 / a ≤ b⁻¹ ↔ b ≤ a
rw₁ : b⁻¹ * a ≤ 1 ↔ b ≤ a
rw₂ : a / b ≤ 1 ↔ b ≤ a
rw₃ : 1 * b ≤ a ↔ b ≤ a
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
have rw₄ : b ≤ a ↔ b ≤ a
Tactic: rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
have rw : b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a
Tactic: rw [← inv_le_inv_of_neg hb (inv_lt_zero'.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : b⁻¹ ≤ a⁻¹⁻¹ ↔ b⁻¹ ≤ a
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
have rw₁ : b⁻¹ ≤ a ↔ b⁻¹ ≤ a
Tactic: rw [← inv_le_inv_of_neg hb (inv_lt_zero'.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
have rw : b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
Tactic: rw [← inv_le_inv_of_neg (inv_lt_zero'.2 hb) ha, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
rw : b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
have rw₁ : b ≤ a⁻¹ ↔ b ≤ a⁻¹
Tactic: rw [← inv_le_inv_of_neg (inv_lt_zero'.2 hb) ha, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (hypothesis)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ < b⁻¹ ↔ b < a
have this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
Tactic: have := div_lt_iff_of_neg ha (b := 1) (a := b⁻¹)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rwa : ∀ (this : a⁻¹ < b⁻¹ ↔ b⁻¹ * a < 1), a⁻¹ < b⁻¹ ↔ b < a
Tactic: rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
rwa : ∀ (this : a⁻¹ < b⁻¹ ↔ b⁻¹ * a < 1), a⁻¹ < b⁻¹ ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rwa₁ : ∀ (this : a⁻¹ < b⁻¹ ↔ a * b⁻¹ < 1), a⁻¹ < b⁻¹ ↔ b < a
Tactic: rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
rwa : ∀ (this : a⁻¹ < b⁻¹ ↔ b⁻¹ * a < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₁ : ∀ (this : a⁻¹ < b⁻¹ ↔ a * b⁻¹ < 1), a⁻¹ < b⁻¹ ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rwa₂ : ∀ (this : a⁻¹ < b⁻¹ ↔ a / b < 1), a⁻¹ < b⁻¹ ↔ b < a
Tactic: rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
rwa : ∀ (this : a⁻¹ < b⁻¹ ↔ b⁻¹ * a < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₁ : ∀ (this : a⁻¹ < b⁻¹ ↔ a * b⁻¹ < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₂ : ∀ (this : a⁻¹ < b⁻¹ ↔ a / b < 1), a⁻¹ < b⁻¹ ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rwa₃ : ∀ (this : a⁻¹ < b⁻¹ ↔ 1 * b < a), a⁻¹ < b⁻¹ ↔ b < a
Tactic: rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
rwa : ∀ (this : a⁻¹ < b⁻¹ ↔ b⁻¹ * a < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₁ : ∀ (this : a⁻¹ < b⁻¹ ↔ a * b⁻¹ < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₂ : ∀ (this : a⁻¹ < b⁻¹ ↔ a / b < 1), a⁻¹ < b⁻¹ ↔ b < a
rwa₃ : ∀ (this : a⁻¹ < b⁻¹ ↔ 1 * b < a), a⁻¹ < b⁻¹ ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a
have rwa₄ : ∀ (this : a⁻¹ < b⁻¹ ↔ b < a), a⁻¹ < b⁻¹ ↔ b < a
Tactic: rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : c < a
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
have pos : ∀ (hab : a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : c < a
pos : ∀ (hab : a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
have neg : ∀ (hab : ¬a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : b < c
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
have pos : ∀ (hab : a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
ha : b < c
pos : ∀ (hab : a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
⊢ AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
have neg : ∀ (hab : ¬a ≤ b), AntitoneOn (β := α) (fun (x : α) ↦ (x - c)⁻¹) (Set.Icc a b)
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Ioi 0)
have h : ∀ (x : α), x = x - 0
Tactic: convert! sub_inv_antitoneOn_Ioi (α := α)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Iio 0)
have h : ∀ (x : α), x = x - 0
Tactic: convert! sub_inv_antitoneOn_Iio (α := α)
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
ha : 0 < a
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Icc a b)
have h : ∀ (x : α), x = x - 0
Tactic: convert! sub_inv_antitoneOn_Icc_right ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ AntitoneOn (β := α) (fun (x : α) ↦ x⁻¹) (Set.Icc a b)
have h : ∀ (x : α), x = x - 0
Tactic: convert! sub_inv_antitoneOn_Icc_left hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a / c ≤ b / c
have rw : a * c⁻¹ ≤ b * c⁻¹
Tactic: rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
h : b < a
⊢ a / c < b / c
have rw : a * c⁻¹ < b * c⁻¹
Tactic: rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a / c ≤ b / c ↔ b ≤ a
have rw : b / c * c ≤ a ↔ b ≤ a
Tactic: rw [div_le_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : b / c * c ≤ a ↔ b ≤ a
⊢ a / c ≤ b / c ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [div_le_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a / c < b / c ↔ b < a
have rw : b / c * c < a ↔ b < a
Tactic: rw [div_lt_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b c : α
hc : c < 0
rw : b / c * c < a ↔ b < a
⊢ a / c < b / c ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [div_lt_iff_of_neg hc, div_mul_cancel₀ _ hc.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ a ≤ b
have rw : a ≤ 1 * b ↔ a ≤ b
Tactic: rw [le_div_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : a ≤ 1 * b ↔ a ≤ b
⊢ 1 ≤ a / b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [le_div_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ b ≤ a
have rw : 1 * b ≤ a ↔ b ≤ a
Tactic: rw [div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : 1 * b ≤ a ↔ b ≤ a
⊢ a / b ≤ 1 ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [div_le_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ a < b
have rw : a < 1 * b ↔ a < b
Tactic: rw [lt_div_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : a < 1 * b ↔ a < b
⊢ 1 < a / b ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [lt_div_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b < 1 ↔ b < a
have rw : 1 * b < a ↔ b < a
Tactic: rw [div_lt_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
rw : 1 * b < a ↔ b < a
⊢ a / b < 1 ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [div_lt_iff_of_neg hb, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ 1 / b ≤ 1 / a
have rwa : b * (1 / a) ≤ 1
Tactic: rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
rwa : b * (1 / a) ≤ 1
⊢ 1 / b ≤ 1 / a
have rwa₁ : b / a ≤ 1
Tactic: rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a
have rwa : b * (1 / a) < 1
Tactic: rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a < b
rwa : b * (1 / a) < 1
⊢ 1 / b < 1 / a
have rwa₁ : b / a < 1
Tactic: rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 < a
this : 1 / a < HDiv.hDiv (α := α) 1 (-1)
⊢ 1 / a < -1
have rwa : ∀ (this : 1 / a < -1), 1 / a < -1
Tactic: rwa [one_div_neg_one_eq_neg_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
h1 : a < 0
h2 : -1 ≤ a
this : 1 / a ≤ HDiv.hDiv (α := α) 1 (-1)
⊢ 1 / a ≤ -1
have rwa : ∀ (this : 1 / a ≤ -1), 1 / a ≤ -1
Tactic: rwa [one_div_neg_one_eq_neg_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + (b - a) / 2 < b
have rwa : a + (b / 2 - a / 2) < b
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
⊢ a + (b - a) / 2 < b
have rwa₁ : a + (b / 2 + -(a / 2)) < b
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
⊢ a + (b - a) / 2 < b
have rwa₂ : a + (-(a / 2) + b / 2) < b
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
rwa₂ : a + (-(a / 2) + b / 2) < b
⊢ a + (b - a) / 2 < b
have rwa₃ : a + -(a / 2) + b / 2 < b
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
rwa₂ : a + (-(a / 2) + b / 2) < b
rwa₃ : a + -(a / 2) + b / 2 < b
⊢ a + (b - a) / 2 < b
have rwa₄ : a - a / 2 + b / 2 < b
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
rwa₂ : a + (-(a / 2) + b / 2) < b
rwa₃ : a + -(a / 2) + b / 2 < b
rwa₄ : a - a / 2 + b / 2 < b
⊢ a + (b - a) / 2 < b
have rwa₅ : a - a / 2 < b - b / 2
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
rwa₂ : a + (-(a / 2) + b / 2) < b
rwa₃ : a + -(a / 2) + b / 2 < b
rwa₄ : a - a / 2 + b / 2 < b
rwa₅ : a - a / 2 < b - b / 2
⊢ a + (b - a) / 2 < b
have rwa₆ : a / 2 < b - b / 2
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a b : α
h : a < b
rwa : a + (b / 2 - a / 2) < b
rwa₁ : a + (b / 2 + -(a / 2)) < b
rwa₂ : a + (-(a / 2) + b / 2) < b
rwa₃ : a + -(a / 2) + b / 2 < b
rwa₄ : a - a / 2 + b / 2 < b
rwa₅ : a - a / 2 < b - b / 2
rwa₆ : a / 2 < b - b / 2
⊢ a + (b - a) / 2 < b
have rwa₇ : a / 2 < b / 2
Tactic: rwa [← div_sub_div_same, sub_eq_add_neg, add_comm (b / 2), ← add_assoc, ← sub_eq_add_neg, ←
    lt_sub_iff_add_lt, sub_self_div_two, sub_self_div_two,
    div_lt_div_iff_of_pos_right (zero_lt_two' α)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2
have refine : 2⁻¹ ≤ 1 - 1 / a
Tactic: refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))
-- Lean 4 proof step from Mathlib.Algebra.Order.Field.Basic (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : PartialOrder α
inst_2 : PosMulReflectLT α
inst_3 : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a
have rw : 1 / a ≤ HSub.hSub (α := α) 1 2⁻¹
Tactic: rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]