-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_top_top :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (⊤, ⊤)

Proof state:
case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
rw [Set.mem_Ioi, ← EReal.coe_one]

Result:
case h.refine_2.refine_2.refine_2
x : ℝ
⊢ ↑1 < (⊤, ⊤).2

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

Tactic:
rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩

Result:
case h.refine_1.intro.intro
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2

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

Tactic:
use (Set.Ioi ((max x 0) : EReal)) ×ˢ (Set.Ioi 1)

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

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

Tactic:
intro x

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

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

Tactic:
intros p p_in_prod

Result:
case h.refine_1
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi (↑x ⊔ 0) ×ˢ Ioi 1
⊢ ↑x < p.1 * p.2

Proof state:
case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (↑x ⊔ 0) ×ˢ Ioi 1)

Tactic:
exact IsOpen.prod isOpen_Ioi isOpen_Ioi

Result:
no goals

Proof state:
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ⊤)

Tactic:
simp only [ContinuousAt, EReal.top_mul_top, EReal.tendsto_nhds_top_iff_real]

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

Proof state:
case h.refine_1
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi (↑x ⊔ 0) ×ˢ Ioi 1
⊢ ↑x < p.1 * p.2

Tactic:
simp only [Set.mem_prod, Set.mem_Ioi, max_lt_iff] at p_in_prod

Result:
case h.refine_1
x : ℝ
p : EReal × EReal
p_in_prod : (↑x < p.1 ∧ 0 < p.1) ∧ 1 < p.2
⊢ ↑x < p.1 * p.2

Proof state:
case h.refine_1.intro.intro
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 * 1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
rw [mul_one p.1] at this

Result:
case h.refine_1.intro.intro
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Proof state:
case h.refine_1.intro.intro
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
exact lt_of_lt_of_le p1_gt_x this

Result:
no goals

Proof state:
case h.refine_1.intro.intro
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
⊢ ↑x < p.1 * p.2

Tactic:
have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)

Result:
case h.refine_1.intro.intro
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 * 1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

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

Tactic:
rw [_root_.eventually_nhds_iff]

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

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

Tactic:
split_ands

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

case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (↑x ⊔ 0) ×ˢ Ioi 1)

case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (↑x ⊔ 0)

case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Proof state:
case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (↑x ⊔ 0)

Tactic:
simp

Result:
no goals

Proof state:
case h.refine_2.refine_2.refine_2
x : ℝ
⊢ ↑1 < (⊤, ⊤).2

Tactic:
exact EReal.coe_lt_top 1

Result:
no goals