awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
h : 0 ≤ (↑a : EReal)
⊢ 0 ≤ (↑a : EReal)⁻¹
have coe : 0 ≤ a
Tactic: rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : 0 ≤ a
⊢ 0 ≤ a⁻¹
have bot : ∀ (h : LE.le (α := EReal) 0 ⊥), LE.le (α := EReal) 0 ⊥⁻¹
Tactic: cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : 0 ≤ a
bot : ∀ (h : LE.le (α := EReal) 0 ⊥), LE.le (α := EReal) 0 ⊥⁻¹
⊢ 0 ≤ a⁻¹
have top : ∀ (h : LE.le (α := EReal) 0 ⊤), LE.le (α := EReal) 0 ⊤⁻¹
Tactic: cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : 0 ≤ a
bot : ∀ (h : LE.le (α := EReal) 0 ⊥), LE.le (α := EReal) 0 ⊥⁻¹
top : ∀ (h : LE.le (α := EReal) 0 ⊤), LE.le (α := EReal) 0 ⊤⁻¹
⊢ 0 ≤ a⁻¹
have coe : ∀ (a : ℝ) (h : 0 ≤ (↑a : EReal)), 0 ≤ (↑a : EReal)⁻¹
Tactic: cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonneg, inv_nonneg]; exact EReal.coe_nonneg.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
h : (↑a : EReal) ≤ 0
⊢ (↑a : EReal)⁻¹ ≤ 0
have coe : a ≤ 0
Tactic: rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≤ 0
⊢ a⁻¹ ≤ 0
have bot : ∀ (h : LE.le (α := EReal) ⊥ 0), LE.le (α := EReal) ⊥⁻¹ 0
Tactic: cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≤ 0
bot : ∀ (h : LE.le (α := EReal) ⊥ 0), LE.le (α := EReal) ⊥⁻¹ 0
⊢ a⁻¹ ≤ 0
have top : ∀ (h : LE.le (α := EReal) ⊤ 0), LE.le (α := EReal) ⊤⁻¹ 0
Tactic: cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a ≤ 0
bot : ∀ (h : LE.le (α := EReal) ⊥ 0), LE.le (α := EReal) ⊥⁻¹ 0
top : ∀ (h : LE.le (α := EReal) ⊤ 0), LE.le (α := EReal) ⊤⁻¹ 0
⊢ a⁻¹ ≤ 0
have coe : ∀ (a : ℝ) (h : (↑a : EReal) ≤ 0), (↑a : EReal)⁻¹ ≤ 0
Tactic: cases a with
  | bot | top => simp
  | coe a => rw [← coe_inv a, EReal.coe_nonpos, inv_nonpos]; exact EReal.coe_nonpos.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : 0 < a
h' : a ≠ ⊤
⊢ 0 < a⁻¹
have lift : ∀ (a : ℝ) (h : 0 < (↑a : EReal)) (h' : (↑a : EReal) ≠ ⊤), 0 < (↑a : EReal)⁻¹
Tactic: lift a to ℝ using ⟨h', ne_bot_of_gt h⟩
Cleared hypotheses: a, h, h'
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
h : 0 < (↑a : EReal)
h' : (↑a : EReal) ≠ ⊤
⊢ 0 < (↑a⁻¹ : EReal)
have norm_cast : ∀ (h : 0 < a), 0 < a⁻¹
Tactic: norm_cast at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h : a < 0
h' : a ≠ ⊥
⊢ a⁻¹ < 0
have lift : ∀ (a : ℝ) (h : (↑a : EReal) < 0) (h' : (↑a : EReal) ≠ ⊥), (↑a : EReal)⁻¹ < 0
Tactic: lift a to ℝ using ⟨ne_top_of_lt h, h'⟩
Cleared hypotheses: a, h, h'
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : ℝ
h : (↑a : EReal) < 0
h' : (↑a : EReal) ≠ ⊥
⊢ (↑a⁻¹ : EReal) < 0
have norm_cast : ∀ (h : a < 0), a⁻¹ < 0
Tactic: norm_cast at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a : EReal
a_0 : Membership.mem (γ := Set EReal) (Ioi 0) a
b : EReal
b_0 : Membership.mem (γ := Set EReal) (Ioi 0) b
a_b : a < b
⊢ LT.lt (α := EReal) ((fun (x : EReal) ↦ x⁻¹) b) ((fun (x : EReal) ↦ x⁻¹) a)
have b_0₁ : 0 < b
Tactic: push _ ∈ _ at *
Cleared hypotheses: a_0, b_0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a : EReal
a_0 : Membership.mem (γ := Set EReal) (Ioi 0) a
b : EReal
b_0 : Membership.mem (γ := Set EReal) (Ioi 0) b
a_b : a < b
b_0₁ : 0 < b
⊢ LT.lt (α := EReal) ((fun (x : EReal) ↦ x⁻¹) b) ((fun (x : EReal) ↦ x⁻¹) a)
have a_0₁ : 0 < a
Tactic: push _ ∈ _ at *
Cleared hypotheses: a_0, b_0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
a_b : a < b
b_0 : 0 < b
a_0 : 0 < a
⊢ b⁻¹ < a⁻¹
have lift : ∀ (a : ℝ) (a_b : (↑a : EReal) < b) (a_0 : 0 < (↑a : EReal)), b⁻¹ < (↑a : EReal)⁻¹
Tactic: lift a to ℝ using ⟨ne_top_of_lt a_b, ne_bot_of_gt a_0⟩
Cleared hypotheses: a, a_b, a_0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b_1 : EReal
a : ℝ
a_0 : 0 < (↑a : EReal)
b : ℝ
b_0 : 0 < (↑b : EReal)
a_b : (↑a : EReal) < (↑b : EReal)
⊢ (↑b : EReal)⁻¹ < (↑a : EReal)⁻¹
have rw : b⁻¹ < a⁻¹
Tactic: rw [← coe_inv a, ← coe_inv b, EReal.coe_lt_coe_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
m n : ℕ
⊢ (↑(m / n) : EReal) ≤ HDiv.hDiv (α := EReal) (↑m : EReal) (↑n : EReal)
have rw : (↑(m / n) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_div,
    EReal.coe_le_coe_iff]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
⊢ a / 0 = 0
have change : a * 0⁻¹ = 0
Tactic: change a * 0⁻¹ = 0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
⊢ a * 0⁻¹ = 0
have rw : a * 0 = 0
Tactic: rw [inv_zero, mul_zero a]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
rw : a * 0 = 0
⊢ a * 0⁻¹ = 0
have rw₁ : Eq (α := EReal) 0 0
Tactic: rw [inv_zero, mul_zero a]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : a ≠ 0
⊢ a / a = 1
have rw : ∀ (h₃ : (↑a.toReal : EReal) ≠ 0), (↑a.toReal : EReal) / (↑a.toReal : EReal) = 1
Tactic: rw [← coe_toReal h₂ h₁] at h₃ ⊢
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : (↑a.toReal : EReal) ≠ 0
⊢ (↑a.toReal : EReal) / (↑a.toReal : EReal) = 1
have rw : (↑(a.toReal / a.toReal) : EReal) = 1
Tactic: rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : (↑a.toReal : EReal) ≠ 0
rw : (↑(a.toReal / a.toReal) : EReal) = 1
⊢ (↑a.toReal : EReal) / (↑a.toReal : EReal) = 1
have rw₁ : (↑1 : EReal) = 1
Tactic: rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : (↑a.toReal : EReal) ≠ 0
rw : (↑(a.toReal / a.toReal) : EReal) = 1
rw₁ : (↑1 : EReal) = 1
⊢ (↑a.toReal : EReal) / (↑a.toReal : EReal) = 1
have rw₂ : Eq (α := EReal) 1 1
Tactic: rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
⊢ a * (b / c) = a * b / c
have change : a * (b * c⁻¹) = a * b * c⁻¹
Tactic: change a * (b * c⁻¹) = (a * b) * c⁻¹
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
⊢ a * (b * c⁻¹) = a * b * c⁻¹
have rw : a * (b * c⁻¹) = a * (b * c⁻¹)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
⊢ a / b * c = a * c / b
have rw : c * (a / b) = a * c / b
Tactic: rw [mul_comm, EReal.mul_div, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
rw : c * (a / b) = a * c / b
⊢ a / b * c = a * c / b
have rw₁ : c * a / b = a * c / b
Tactic: rw [mul_comm, EReal.mul_div, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
rw : c * (a / b) = a * c / b
rw₁ : c * a / b = a * c / b
⊢ a / b * c = a * c / b
have rw₂ : a * c / b = a * c / b
Tactic: rw [mul_comm, EReal.mul_div, mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
⊢ a * (b / c) = b * (a / c)
have rw : a * b / c = b * (a / c)
Tactic: rw [mul_div a b c, mul_comm a b, ← mul_div b a c]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
rw : a * b / c = b * (a / c)
⊢ a * (b / c) = b * (a / c)
have rw₁ : b * a / c = b * (a / c)
Tactic: rw [mul_div a b c, mul_comm a b, ← mul_div b a c]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
rw : a * b / c = 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 [mul_div a b c, mul_comm a b, ← mul_div b a c]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
⊢ a / b / c = a / (b * c)
have change : a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
Tactic: change (a * b⁻¹) * c⁻¹ = a * (b * c)⁻¹
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
have rw : a * (b⁻¹ * c⁻¹) = a * (b * c)⁻¹
Tactic: rw [mul_assoc a b⁻¹, mul_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
rw : a * (b⁻¹ * c⁻¹) = a * (b * c)⁻¹
⊢ a * b⁻¹ * c⁻¹ = a * (b * c)⁻¹
have rw₁ : a * (b⁻¹ * c⁻¹) = a * (b⁻¹ * c⁻¹)
Tactic: rw [mul_assoc a b⁻¹, mul_inv]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c d : EReal
⊢ a / b * (c / d) = a * c / (b * d)
have rw : a / b * (c / d) = a * (c / (b * d))
Tactic: rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c d : EReal
rw : a / b * (c / d) = a * (c / (b * d))
⊢ a / b * (c / d) = a * c / (b * d)
have rw₁ : a / b * (c / d) = a * (c / (d * b))
Tactic: rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c d : EReal
rw : a / b * (c / d) = a * (c / (b * d))
rw₁ : a / b * (c / d) = a * (c / (d * b))
⊢ a / b * (c / d) = a * c / (b * d)
have rw₂ : a / b * (c / d) = a * (c / d / b)
Tactic: rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c d : EReal
rw : a / b * (c / d) = a * (c / (b * d))
rw₁ : a / b * (c / d) = a * (c / (d * b))
rw₂ : a / b * (c / d) = a * (c / d / b)
⊢ a / b * (c / d) = a * c / (b * d)
have rw₃ : a / b * (c / d) = c / d * (a / b)
Tactic: rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c d : EReal
rw : a / b * (c / d) = a * (c / (b * d))
rw₁ : a / b * (c / d) = a * (c / (d * b))
rw₂ : a / b * (c / d) = a * (c / d / b)
rw₃ : a / b * (c / d) = c / d * (a / b)
⊢ a / b * (c / d) = a * c / (b * d)
have rw₄ : c / d * (a / b) = c / d * (a / b)
Tactic: rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ a / b * b = a
have rw : b * (a / b) = a
Tactic: rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
rw : b * (a / b) = a
⊢ a / b * b = a
have rw₁ : a * (b / b) = a
Tactic: rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
rw : b * (a / b) = a
rw₁ : a * (b / b) = a
⊢ a / b * b = a
have rw₂ : a * 1 = a
Tactic: rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
rw : b * (a / b) = a
rw₁ : a * (b / b) = a
rw₂ : a * 1 = a
⊢ a / b * b = a
have rw₃ : a = a
Tactic: rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ b * (a / b) = a
have rw : a / b * b = a
Tactic: rw [mul_comm, div_mul_cancel h₁ h₂ h₃]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
rw : a / b * b = a
⊢ b * (a / b) = a
have rw₁ : a = a
Tactic: rw [mul_comm, div_mul_cancel h₁ h₂ h₃]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a * c / (b * c) = a / b
have rw : a / (b * c) * c = a / b
Tactic: rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
rw : a / (b * c) * c = a / b
⊢ a * c / (b * c) = a / b
have rw₁ : a / b / c * c = a / b
Tactic: rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
rw : a / (b * c) * c = a / b
rw₁ : a / b / c * c = a / b
⊢ a * c / (b * c) = a / b
have rw₂ : a / b = a / b
Tactic: rw [← mul_div_right a (b * c) c, ← div_div a b c, div_mul_cancel h₁ h₂ h₃]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
⊢ c / b = a ↔ c = a * b
have refine_1 : ∀ (h : c / b = a), c = a * b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
refine_1 : ∀ (h : c / b = a), c = a * b
⊢ c / b = a ↔ c = a * b
have refine_2 : ∀ (h : c = a * b), c / b = a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ c = a * b
have refine_1 : b * (c / b) = a * b
Tactic: rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
refine_1 : b * (c / b) = a * b
⊢ c = a * b
have refine_1₁ : b * a = a * b
Tactic: rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
refine_1 : b * (c / b) = a * b
refine_1₁ : b * a = a * b
⊢ c = a * b
have refine_1₂ : b * a = b * a
Tactic: rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ c / b = a
have refine_2 : a * b / b = a
Tactic: rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
refine_2 : a * b / b = a
⊢ c / b = a
have refine_2₁ : b * a / b = a
Tactic: rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
refine_2 : a * b / b = a
refine_2₁ : b * a / b = a
⊢ c / b = a
have refine_2₂ : b * (a / b) = a
Tactic: rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
refine_2 : a * b / b = a
refine_2₁ : b * a / b = a
refine_2₂ : b * (a / b) = a
⊢ c / b = a
have refine_2₃ : a = a
Tactic: rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
⊢ LT.lt (α := EReal) ((fun (a : EReal) ↦ a / b) a) ((fun (a : EReal) ↦ a / b) a')
have apply : a / b ≠ a' / b
Tactic: apply lt_of_le_of_ne <| div_le_div_right_of_nonneg (le_of_lt h) (le_of_lt a_lt_a')
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ False
have apply : a = a'
Tactic: apply ne_of_lt a_lt_a'
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ a = a'
have rw : b * (a / b) = a'
Tactic: rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' h.ne', hyp,
    @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
rw : b * (a / b) = a'
⊢ a = a'
have rw₁ : b * (a' / b) = a'
Tactic: rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' h.ne', hyp,
    @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
rw : b * (a / b) = a'
rw₁ : b * (a' / b) = a'
⊢ a = a'
have rw₂ : a' = a'
Tactic: rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' h.ne', hyp,
    @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ LE.le (α := EReal) ((fun (a : EReal) ↦ a / b) a') ((fun (a : EReal) ↦ a / b) a)
have change : a' * b⁻¹ ≤ a * b⁻¹
Tactic: change a' * b⁻¹ ≤ a * b⁻¹
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a' * b⁻¹ ≤ a * b⁻¹
have rw : a * (-b)⁻¹ ≤ a' * (-b)⁻¹
Tactic: rw [← neg_neg (a * b⁻¹), ← neg_neg (a' * b⁻¹), neg_le_neg_iff, mul_comm a b⁻¹, mul_comm a' b⁻¹,
    ← neg_mul b⁻¹ a, ← neg_mul b⁻¹ a', mul_comm (-b⁻¹) a, mul_comm (-b⁻¹) a', ← inv_neg b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ 0 ≤ -b
have h₁ : b ≤ -0
Tactic: apply EReal.le_neg_of_le_neg
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹
have this : 0 ≤ -b
Tactic: have : 0 ≤ -b := by apply EReal.le_neg_of_le_neg; simp [h]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ a' / b < a / b
have apply : a' / b ≠ a / b
Tactic: apply lt_of_le_of_ne <| div_le_div_right_of_nonpos (le_of_lt h) (le_of_lt a_lt_a')
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ False
have apply : a = a'
Tactic: apply ne_of_lt a_lt_a'
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ a = a'
have rw : b * (a / b) = a'
Tactic: rw [← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
    @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
rw : b * (a / b) = a'
⊢ a = a'
have rw₁ : b * (a' / b) = a'
Tactic: rw [← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
    @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
rw : b * (a / b) = a'
rw₁ : b * (a' / b) = a'
⊢ a = a'
have rw₂ : a' = a'
Tactic: rw [← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
    @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c
have nth_rw : b * (a / b) ≤ c / b ↔ a * b ≤ c
Tactic: nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c
have rw : b * a / b ≤ c / b ↔ b * a ≤ c
Tactic: rw [mul_div b a b, mul_comm a b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c ↔ a ≤ b * c
have nth_rw : a / b ≤ b * (c / b) ↔ a ≤ b * c
Tactic: nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c
have rw : a / b ≤ c * b / b ↔ a ≤ c * b
Tactic: rw [mul_div b c b, mul_comm b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a < c / b ↔ a * b < c
have nth_rw : b * (a / b) < c / b ↔ a * b < c
Tactic: nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c
have rw : b * a / b < c / b ↔ b * a < c
Tactic: rw [EReal.mul_div b a b, mul_comm a b]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < a ↔ b < a * c
have nth_rw : b / c < c * (a / c) ↔ b < a * c
Tactic: nth_rw 1 [← @mul_div_cancel a c (ne_bot_of_gt h) h' h.ne']
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * (a / c) ↔ b < a * c
have rw : b / c < c * a / c ↔ b < c * a
Tactic: rw [EReal.mul_div c a c, mul_comm a c]
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
have inl : ∀ (h : c < a * ⊤), ∃ a' ∈ Ioo 0 a, c < a' * ⊤
Tactic: rcases eq_or_ne b ⊤ with rfl | b_top
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
inl : ∀ (h : c < a * ⊤), ∃ a' ∈ Ioo 0 a, c < a' * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
have inr : ∀ (b_top : b ≠ ⊤), ∃ a' ∈ Ioo 0 a, c < a' * b
Tactic: rcases eq_or_ne b ⊤ with rfl | b_top
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤
have inl : ∀ (ha : LE.le (α := EReal) 0 0) (h : c < HMul.hMul (α := EReal) 0 ⊤),
  ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 0) a' ∧ c < a' * ⊤
Tactic: rcases eq_or_lt_of_le ha with rfl | ha
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
inl :
  ∀ (ha : LE.le (α := EReal) 0 0) (h : c < HMul.hMul (α := EReal) 0 ⊤),
    ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 0) a' ∧ c < a' * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤
have inl₁ : ∀ (ha : 0 < a), ∃ a' ∈ Ioo 0 a, c < a' * ⊤
Tactic: rcases eq_or_lt_of_le ha with rfl | ha
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
c : EReal
hc : 0 ≤ c
ha : LE.le (α := EReal) 0 0
h : c < HMul.hMul (α := EReal) 0 ⊤
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 0) a' ∧ c < a' * ⊤
have h₁ : c < 0
Tactic: rw [zero_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
ha_1 : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤
have inl : ∀ (a' : EReal) (a0' : 0 < a') (aa' : a' < a), ∃ a' ∈ Ioo 0 a, c < a' * ⊤
Tactic: obtain ⟨a', a0', aa'⟩ := exists_between ha
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
ha_1 : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤
have right : c < a' * ⊤
Tactic: use a', mem_Ioo.2 ⟨a0', aa'⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
ha_1 : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤
have right : ∀ (h : c < ⊤) (ha : 0 < a) (a' : EReal) (a0' : 0 < a') (aa' : a' < a), c < a' * ⊤
Tactic: rw [mul_top_of_pos ha] at h
Cleared hypotheses: h, ha, a', a0', aa'
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
have b0 : 0 < b
Tactic: have b0 : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha