-- Mathlib/Data/Real/EReal.lean
private lemma exists_lt_mul_left_of_nonneg (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
    ∃ a' ∈ Ico 0 a, c < a' * b

Proof state:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Tactic:
rwa [mul_top_of_pos a0']

Result:
no goals

Proof state:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0
⊢ ∃ a' ∈ Ico 0 0, c < a' * ⊤

Tactic:
exact (not_le_of_lt h hc).rec

Result:
no goals

Proof state:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ico 0 a, c < a' * b

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

Result:
case inr.intro.intro
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' ∈ Ico 0 a, c < a' * b

Proof state:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ a' ∈ Ico 0 a, c < a' * b

Tactic:
rcases eq_or_ne b ⊤ with rfl | b_top

Result:
case inl
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
⊢ ∃ a' ∈ Ico 0 a, c < a' * ⊤

case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ico 0 a, c < a' * b

Proof state:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Tactic:
rw [mul_top_of_pos ha] at h

Result:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Proof state:
case inl.inr.intro.intro
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ ∃ a' ∈ Ico 0 a, c < a' * ⊤

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

Result:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Proof state:
case inr.intro.intro
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' ∈ Ico 0 a, c < a' * b

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

Result:
no goals

Proof state:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0 * ⊤
⊢ ∃ a' ∈ Ico 0 0, c < a' * ⊤

Tactic:
rw [zero_mul] at h

Result:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0
⊢ ∃ a' ∈ Ico 0 0, c < a' * ⊤

Proof state:
case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
⊢ ∃ a' ∈ Ico 0 a, c < a' * ⊤

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

Result:
case inl.inr.intro.intro
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ ∃ a' ∈ Ico 0 a, c < a' * ⊤

Proof state:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
⊢ ∃ a' ∈ Ico 0 a, c < a' * b

Tactic:
have b0 : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha

Result:
case inr
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ico 0 a, c < a' * b

Proof state:
case inl
a c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
⊢ ∃ a' ∈ Ico 0 a, c < a' * ⊤

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha

Result:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0 * ⊤
⊢ ∃ a' ∈ Ico 0 0, c < a' * ⊤

case inl.inr
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
⊢ ∃ a' ∈ Ico 0 a, c < a' * ⊤