awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Inv
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
refine_1₂ refine_1₃ : b * a = b * a
⊢ c = a * b

Tactic:
rw [← @mul_div_cancel c b hbot htop hzero, h, mul_comm a b]

Premises used: EReal.mul_div_cancel, mul_comm
-- Module: Mathlib.Data.EReal.Inv
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
refine_2₃ refine_2₄ : a = a
⊢ c / b = a

Tactic:
rw [h, mul_comm a b, ← mul_div b a b, @mul_div_cancel a b hbot htop hzero]

Premises used: EReal.mul_div, EReal.mul_div_cancel, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : 0 ≤ b
⊢ Monotone (β := EReal) fun (a : EReal) ↦ a / b

Tactic:
fun _ _ h' ↦ mul_le_mul_of_nonneg_right h' (inv_nonneg_of_nonneg h)

Premises used: EReal.inv_nonneg_of_nonneg, Monotone, DivInvMonoid.div', mul_le_mul_of_nonneg_right, EReal.mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 ≤ c
h' : a ≤ b
⊢ a / c ≤ b / c

Tactic:
monotone_div_right_of_nonneg h h'

Premises used: EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
apply : a / b ≠ a' / b
⊢ LT.lt (α := EReal) ((fun (a : EReal) ↦ a / b) a) ((fun (a : EReal) ↦ a / b) a')

Tactic:
apply lt_of_le_of_ne <| div_le_div_right_of_nonneg (le_of_lt h) (le_of_lt a_lt_a')

Premises used: EReal.div_le_div_right_of_nonneg, le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
apply : a = a'
⊢ False

Tactic:
apply ne_of_lt a_lt_a'

Premises used: ne_of_lt
-- Module: Mathlib.Data.EReal.Inv
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'
rw₂ rw₃ : a' = a'
⊢ 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']

Premises used: LT.lt.ne', EReal.mul_div_cancel, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : 0 < c
h₂ : c ≠ ⊤
h₃ : a < b
⊢ a / c < b / c

Tactic:
strictMono_div_right_of_pos h₁ h₂ h₃

Premises used: EReal.strictMono_div_right_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
change : a' * b⁻¹ ≤ a * b⁻¹
⊢ LE.le (α := EReal) ((fun (a : EReal) ↦ a / b) a') ((fun (a : EReal) ↦ a / b) a)

Tactic:
change a' * b⁻¹ ≤ a * b⁻¹
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
rw : a * (-b)⁻¹ ≤ a' * (-b)⁻¹
⊢ 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]

Premises used: HMul.hMul, EReal.neg_le_neg_iff, neg_neg, EReal.inv_neg, Inv.inv, mul_comm, neg_mul, Neg.neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
h₁ : b ≤ -0
⊢ 0 ≤ -b

Tactic:
apply EReal.le_neg_of_le_neg

Premises used: EReal.le_neg_of_le_neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ b ≤ -0

Tactic:
simp [h]
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ 0 ≤ -b

Tactic:
have : 0 ≤ -b := by apply EReal.le_neg_of_le_neg; simp [h]
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
this : 0 ≤ -b
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Tactic:
div_le_div_right_of_nonneg this h'

Premises used: EReal.div_le_div_right_of_nonneg, DivInvMonoid.div', EReal.mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
this : 0 ≤ -b
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Tactic:
exact div_le_div_right_of_nonneg this h'

Premises used: EReal.div_le_div_right_of_nonneg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : c ≤ 0
h' : a ≤ b
⊢ b / c ≤ a / c

Tactic:
antitone_div_right_of_nonpos h h'

Premises used: EReal.antitone_div_right_of_nonpos
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
apply : a' / b ≠ a / b
⊢ 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')

Premises used: le_of_lt, EReal.div_le_div_right_of_nonpos, lt_of_le_of_ne
-- Module: Mathlib.Data.EReal.Inv
Goal:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
apply : a = a'
⊢ False

Tactic:
apply ne_of_lt a_lt_a'

Premises used: ne_of_lt
-- Module: Mathlib.Data.EReal.Inv
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'
rw₂ rw₃ : a' = a'
⊢ 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)]

Premises used: EReal.mul_div_cancel, ne_top_of_lt, ne_of_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : c < 0
h₂ : c ≠ ⊥
h₃ : a < b
⊢ b / c < a / c

Tactic:
strictAnti_div_right_of_neg h₁ h₂ h₃

Premises used: EReal.strictAnti_div_right_of_neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
nth_rw : b * (a / b) ≤ c / b ↔ a * b ≤ c
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']

Premises used: LT.lt.ne', EReal.mul_div_cancel, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
rw : b * a / b ≤ c / b ↔ b * a ≤ c
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c

Tactic:
rw [mul_div b a b, mul_comm a b]

Premises used: EReal.mul_div, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c

Tactic:
StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.le_iff_le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c

Tactic:
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.le_iff_le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
nth_rw : a / b ≤ b * (c / b) ↔ a ≤ b * c
⊢ a / b ≤ c ↔ a ≤ b * c

Tactic:
nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' h.ne']

Premises used: LT.lt.ne', EReal.mul_div_cancel, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
rw : a / b ≤ c * b / b ↔ a ≤ c * b
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c

Tactic:
rw [mul_div b c b, mul_comm b]

Premises used: EReal.mul_div, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b

Tactic:
StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.le_iff_le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b

Tactic:
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.le_iff_le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
nth_rw : b * (a / b) < c / b ↔ a * b < c
⊢ a < c / b ↔ a * b < c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']

Premises used: LT.lt.ne', EReal.mul_div_cancel, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
rw : b * a / b < c / b ↔ b * a < c
⊢ b * (a / b) < c / b ↔ a * b < c

Tactic:
rw [EReal.mul_div b a b, mul_comm a b]

Premises used: EReal.mul_div, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c

Tactic:
(strictMono_div_right_of_pos h h').lt_iff_lt

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c

Tactic:
exact (strictMono_div_right_of_pos h h').lt_iff_lt

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
nth_rw : b / c < c * (a / c) ↔ b < a * c
⊢ b / c < a ↔ b < a * c

Tactic:
nth_rw 1 [← @mul_div_cancel a c (ne_bot_of_gt h) h' h.ne']

Premises used: LT.lt.ne', EReal.mul_div_cancel, ne_bot_of_gt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
rw : b / c < c * a / c ↔ b < c * a
⊢ b / c < c * (a / c) ↔ b < a * c

Tactic:
rw [EReal.mul_div c a c, mul_comm a c]

Premises used: EReal.mul_div, mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a

Tactic:
(strictMono_div_right_of_pos h h').lt_iff_lt

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a

Tactic:
exact (strictMono_div_right_of_pos h h').lt_iff_lt

Premises used: EReal.strictMono_div_right_of_pos, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : 0 ≤ a
h' : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
mul_nonneg h (inv_nonneg_of_nonneg h')

Premises used: mul_nonneg, EReal.inv_nonneg_of_nonneg, DivInvMonoid.div', EReal.mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
ha : 0 < a
hb : 0 < b
hb' : b ≠ ⊤
⊢ 0 < a / b

Tactic:
EReal.mul_pos ha (inv_pos_of_pos_ne_top hb hb')

Premises used: DivInvMonoid.div', EReal.mul_pos, EReal.mul, EReal.inv_pos_of_pos_ne_top
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : a ≤ 0
h' : 0 ≤ b
⊢ a / b ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg h (inv_nonneg_of_nonneg h')

Premises used: EReal.inv_nonneg_of_nonneg, mul_nonpos_of_nonpos_of_nonneg, DivInvMonoid.div', EReal.mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : 0 ≤ a
h' : b ≤ 0
⊢ a / b ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos h (inv_nonpos_of_nonpos h')

Premises used: EReal.inv_nonpos_of_nonpos, DivInvMonoid.div', EReal.mul, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b : EReal
h : a ≤ 0
h' : b ≤ 0
⊢ 0 ≤ a / b

Tactic:
le_of_eq_of_le zero_div.symm (div_le_div_right_of_nonpos h' h)

Premises used: EReal.div_le_div_right_of_nonpos, le_of_eq_of_le, EReal.zero_div, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
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' * ⊤
inr : ∀ (b_top : b ≠ ⊤), ∃ a' ∈ Ioo 0 a, c < a' * b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
rcases eq_or_ne b ⊤ with rfl | b_top

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.EReal.Inv
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' * ⊤
inl₁ : ∀ (ha : 0 < a), ∃ a' ∈ Ioo 0 a, c < a' * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
hc : 0 ≤ c
ha : LE.le (α := EReal) 0 0
h : c < HMul.hMul (α := EReal) 0 ⊤
⊢ c < 0

Tactic:
rw [zero_mul] at h

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
hc : 0 ≤ c
ha : LE.le (α := EReal) 0 0
h : c < 0
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 0) a' ∧ c < a' * ⊤

Tactic:
(not_le_of_gt h hc).rec

Premises used: HMul.hMul, Membership.mem, Exists, And, LT.lt, False.rec, not_le_of_gt, Top.top, OfNat.ofNat, Set.Ioo
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
hc : 0 ≤ c
ha : LE.le (α := EReal) 0 0
h : c < 0
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 0) a' ∧ c < a' * ⊤

Tactic:
exact (not_le_of_gt h hc).rec
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
ha_1 : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
inl : ∀ (a' : EReal) (a0' : 0 < a') (aa' : a' < a), ∃ a' ∈ Ioo 0 a, c < a' * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
obtain ⟨a', a0', aa'⟩ := exists_between ha

Premises used: exists_between
-- Module: Mathlib.Data.EReal.Inv
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
right : c < a' * ⊤
⊢ ∃ a' ∈ Ioo 0 a, c < a' * ⊤

Tactic:
use a', mem_Ioo.2 ⟨a0', aa'⟩

Premises used: Iff.mpr, Set.mem_Ioo, And.intro
-- Module: Mathlib.Data.EReal.Inv
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
right : ∀ (h : c < ⊤) (ha : 0 < a) (a' : EReal) (a0' : 0 < a') (aa' : a' < a), c < a' * ⊤
⊢ c < a' * ⊤

Tactic:
rw [mul_top_of_pos ha] at h

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
ha_1 : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
right right₁ right₂ right₃ : c < ⊤
⊢ c < a' * ⊤

Tactic:
rwa [mul_top_of_pos a0']

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ 0 < b

Tactic:
have b0 : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
inr : ∀ (a' : EReal) (ha' : c / b < a') (aa' : a' < a), ∃ a' ∈ Ioo 0 a, c < a' * b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
obtain ⟨a', ha', aa'⟩ := exists_between ((div_lt_iff b0 b_top).2 h)

Premises used: Iff.mpr, exists_between, EReal.div_lt_iff
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
a' : EReal
ha' : c / b < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
⟨a', ⟨(div_nonneg hc b0.le).trans_lt ha', aa'⟩, (div_lt_iff b0 b_top).1 ha'⟩

Premises used: LT.lt.le, EReal.div_lt_iff, And.intro, Exists.intro, Iff.mp, EReal.div_nonneg, LE.le.trans_lt
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
a' : EReal
ha' : c / b < a'
aa' : a' < a
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b

Tactic:
exact ⟨a', ⟨(div_nonneg hc b0.le).trans_lt ha', aa'⟩, (div_lt_iff b0 b_top).1 ha'⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ 0 < b

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
simp_rw : ∀ (h : c < b * a), ∃ b' ∈ Ioo 0 b, c < b' * a
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'

Tactic:
simp_rw [mul_comm a] at h ⊢

Premises used: mul_comm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Ioo 0 b, c < b' * a

Tactic:
exists_lt_mul_left_of_nonneg hb.le hc h

Premises used: _private.0.EReal.exists_lt_mul_left_of_nonneg, LT.lt.le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Ioo 0 b, c < b' * a

Tactic:
exact exists_lt_mul_left_of_nonneg hb.le hc h

Premises used: _private.0.EReal.exists_lt_mul_left_of_nonneg, LT.lt.le
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
inl :
  ∀ (h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤) (h₂ : Ne (α := EReal) ⊤ ⊤ ∨ 0 < b) (hc : ⊤ * b < c),
    ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c
inr : ∀ (a_top : a < ⊤), ∃ a' ∈ Ioo a ⊤, a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
rcases eq_top_or_lt_top a with rfl | a_top

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : Ne (α := EReal) ⊤ ⊤ ∨ 0 < b
hc : ⊤ * b < c
⊢ 0 < b

Tactic:
rw [ne_self_iff_false, false_or] at h₂

Premises used: ne_self_iff_false, false_or
-- Module: Mathlib.Data.EReal.Inv
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : Ne (α := EReal) ⊤ ⊤ ∨ 0 < b
hc : ⊤ * b < c
h₃ : 0 < b
⊢ ⊤ * b < c

Tactic:
rw [ne_self_iff_false, false_or] at h₂

Premises used: ne_self_iff_false, false_or
-- Module: Mathlib.Data.EReal.Inv
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ⊤ < c

Tactic:
rw [top_mul_of_pos h₂] at hc

Premises used: EReal.top_mul_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c

Tactic:
(not_top_lt hc).rec

Premises used: HMul.hMul, not_top_lt, Membership.mem, Exists, And, LT.lt, False.rec, Top.top, Set.Ioo
-- Module: Mathlib.Data.EReal.Inv
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c

Tactic:
exact (not_top_lt hc).rec
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
inr : ∀ (b0 : b ≤ 0), ∃ a' ∈ Ioo a ⊤, a' * b < c
inr₁ : ∀ (b0 : 0 < b), ∃ a' ∈ Ioo a ⊤, a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
rcases le_or_gt b 0 with b0 | b0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
inr : ∀ (a' : EReal) (aa' : a < a') (a_top' : a' < ⊤), ∃ a' ∈ Ioo a ⊤, a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
obtain ⟨a', aa', a_top'⟩ := exists_between a_top

Premises used: exists_between
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
a' : EReal
aa' : a < a'
a_top' : a' < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
⟨a', mem_Ioo.2 ⟨aa', a_top'⟩, lt_of_le_of_lt (mul_le_mul_of_nonpos_right aa'.le b0) hc⟩

Premises used: Iff.mpr, lt_of_le_of_lt, Set.mem_Ioo, LT.lt.le, And.intro, EReal.mul_le_mul_of_nonpos_right, Exists.intro
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
a' : EReal
aa' : a < a'
a_top' : a' < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
exact ⟨a', mem_Ioo.2 ⟨aa', a_top'⟩, lt_of_le_of_lt (mul_le_mul_of_nonpos_right aa'.le b0) hc⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
inr :
  ∀ (h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤) (h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤) (hc : a * ⊤ < c)
    (b0 : LT.lt (α := EReal) 0 ⊤), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
inr₁ : ∀ (b_top : b < ⊤), ∃ a' ∈ Ioo a ⊤, a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
rcases eq_top_or_lt_top b with rfl | b_top

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
inr : ∀ (a0 : a < 0), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
inr₁ :
  ∀ (a_top : LT.lt (α := EReal) 0 ⊤) (h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤)
    (h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤) (hc : HMul.hMul (α := EReal) 0 ⊤ < c),
    ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 ⊤) a' ∧ a' * ⊤ < c
inr₂ : ∀ (a0 : 0 < a), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
rcases lt_trichotomy a 0 with a0 | rfl | a0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : a < 0
inr : ∀ (a' : EReal) (aa' : a < a') (a0' : a' < 0), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
obtain ⟨a', aa', a0'⟩ := exists_between a0

Premises used: exists_between
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
inr :
  ∀ (hc : ⊥ < c) (b0 : LT.lt (α := EReal) 0 ⊤) (a0 : a < 0) (a' : EReal) (aa' : a < a') (a0' : a' < 0),
    ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
rw [mul_top_of_neg a0] at hc

Premises used: EReal.mul_top_of_neg
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : ⊥ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt a0'⟩, mul_top_of_neg a0' ▸ hc⟩

Premises used: Iff.mpr, Set.mem_Ioo, lt_top_of_lt, Eq.rec, EReal.mul_top_of_neg, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : ⊥ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
refine ⟨a', mem_Ioo.2 ⟨aa', lt_top_of_lt a0'⟩, mul_top_of_neg a0' ▸ hc⟩
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
b0 : LT.lt (α := EReal) 0 ⊤
a_top : LT.lt (α := EReal) 0 ⊤
h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : HMul.hMul (α := EReal) 0 ⊤ < c
⊢ False

Tactic:
rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁

Premises used: ne_self_iff_false, false_or
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
b0 : LT.lt (α := EReal) 0 ⊤
a_top : LT.lt (α := EReal) 0 ⊤
h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : HMul.hMul (α := EReal) 0 ⊤ < c
h₃ : False
⊢ Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤

Tactic:
rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁

Premises used: ne_self_iff_false, false_or
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
b0 : LT.lt (α := EReal) 0 ⊤
a_top : LT.lt (α := EReal) 0 ⊤
h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : HMul.hMul (α := EReal) 0 ⊤ < c
h₃ : False
h₄ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
⊢ HMul.hMul (α := EReal) 0 ⊤ < c

Tactic:
rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁

Premises used: ne_self_iff_false, false_or
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
b0 : LT.lt (α := EReal) 0 ⊤
a_top : LT.lt (α := EReal) 0 ⊤
h₁ : False
h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : HMul.hMul (α := EReal) 0 ⊤ < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 ⊤) a' ∧ a' * ⊤ < c

Tactic:
h₁.rec

Premises used: HMul.hMul, Membership.mem, Exists, And, LT.lt, False.rec, Top.top, OfNat.ofNat, Set.Ioo
-- Module: Mathlib.Data.EReal.Inv
Goal:
c : EReal
b0 : LT.lt (α := EReal) 0 ⊤
a_top : LT.lt (α := EReal) 0 ⊤
h₁ : False
h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : HMul.hMul (α := EReal) 0 ⊤ < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 ⊤) a' ∧ a' * ⊤ < c

Tactic:
exact h₁.rec
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : 0 < a
⊢ ⊤ < c

Tactic:
rw [mul_top_of_pos a0] at hc

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : 0 < a
hc₁ : ⊤ < c
⊢ LT.lt (α := EReal) 0 ⊤

Tactic:
rw [mul_top_of_pos a0] at hc

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : 0 < a
hc₁ : ⊤ < c
b0₁ : LT.lt (α := EReal) 0 ⊤
⊢ 0 < a

Tactic:
rw [mul_top_of_pos a0] at hc

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
(not_top_lt hc).rec

Premises used: HMul.hMul, not_top_lt, Membership.mem, Exists, And, LT.lt, False.rec, Top.top, Set.Ioo
-- Module: Mathlib.Data.EReal.Inv
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
exact (not_top_lt hc).rec