-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_top_pos {a : ℝ} (h : 0 < a) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (⊤, a)

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ 2 * ((x + 1) ⊔ 0) / a

Tactic:
apply mul_nonneg _ (le_of_lt (inv_pos_of_pos h))

Result:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ 2 * ((x + 1) ⊔ 0)

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ x < a / a * (2 / 2 * ((x + 1) ⊔ 0))

Tactic:
simp only [ne_eq, Ne.symm (ne_of_lt h), not_false_eq_true, _root_.div_self, OfNat.ofNat_ne_zero,
  one_mul, lt_max_iff, lt_add_iff_pos_right, zero_lt_one, true_or]

Result:
no goals

Proof state:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
apply lt_of_lt_of_le _ lock

Result:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2)

Proof state:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2

Tactic:
have a2_pos : 0 < ((a/2 : ℝ) : EReal) := by rw [EReal.coe_pos]; linarith

Result:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
⊢ ↑x < p.1 * p.2

Proof state:
a : ℝ
h : 0 < a
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2

Tactic:
intro x

Result:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2

Proof state:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * ↑(a / 2)
⊢ ↑x < p.1 * p.2

Tactic:
have key := mul_le_mul_of_nonneg_left (le_of_lt p2_gt) (le_of_lt p1_pos)

Result:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Proof state:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1 ∧ ↑(a / 2) < p.2
⊢ ↑x < p.1 * p.2

Tactic:
rcases p_in_prod with ⟨p1_gt, p2_gt⟩

Result:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ ↑x < p.1 * p.2

Proof state:
case h
a : ℝ
h : 0 < a
x : ℝ
⊢ (∀ y ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2) ∧
    IsOpen (Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2)) ∧ (⊤, ↑a) ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2)

Tactic:
split_ands

Result:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2))

case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a)

case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 < p.1

Tactic:
apply lt_of_le_of_lt _ p1_gt

Result:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ ↑(2 * ((x + 1) ⊔ 0) / a)

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
⊢ 0 < a / 2

Tactic:
linarith

Result:
no goals

Proof state:
case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a)

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2

Tactic:
rw [_root_.eventually_nhds_iff]

Result:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ↑a) ∈ t

Proof state:
a : ℝ
h : 0 < a
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)

Tactic:
simp only [ContinuousAt, EReal.top_mul_coe_of_pos h, EReal.tendsto_nhds_top_iff_real]

Result:
a : ℝ
h : 0 < a
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2

Proof state:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
⊢ ↑x < p.1 * p.2

Tactic:
have lock := mul_le_mul_of_nonneg_right (le_of_lt p1_gt) (le_of_lt a2_pos)

Result:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * ↑(a / 2)
⊢ ↑x < p.1 * p.2

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ 2 * ((x + 1) ⊔ 0)

Tactic:
simp only [gt_iff_lt, Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, le_refl, or_true]

Result:
no goals

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ ↑(2 * ((x + 1) ⊔ 0) / a)

Tactic:
rw [EReal.coe_nonneg]

Result:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ 0 ≤ 2 * ((x + 1) ⊔ 0) / a

Proof state:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ↑a) ∈ t

Tactic:
use (Set.Ioi ((2*(max (x+1) 0)/a : ℝ) : EReal)) ×ˢ (Set.Ioi ((a/2 : ℝ) : EReal))

Result:
case h
a : ℝ
h : 0 < a
x : ℝ
⊢ (∀ y ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2) ∧
    IsOpen (Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2)) ∧ (⊤, ↑a) ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2)

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
⊢ 0 < ↑(a / 2)

Tactic:
rw [EReal.coe_pos]

Result:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
⊢ 0 < a / 2

Proof state:
case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
simp [h]

Result:
no goals

Proof state:
case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2))

Tactic:
exact IsOpen.prod isOpen_Ioi isOpen_Ioi

Result:
no goals

Proof state:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
⊢ ↑x < p.1 * p.2

Tactic:
have p1_pos : 0 < p.1 := by
  apply lt_of_le_of_lt _ p1_gt
  rw [EReal.coe_nonneg]
  apply mul_nonneg _ (le_of_lt (inv_pos_of_pos h))
  simp only [gt_iff_lt, Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, le_refl, or_true]

Result:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2