awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
h :
  (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
      (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
⊢ ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ⊤) ∈ t

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

Premises used: Set.Ioi, Max.max, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
h : ∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2
h₁ : IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1))
h₂ : (⊤, ⊤).1 ∈ Ioi (max (↑x : EReal) 0)
h₃ : Membership.mem (γ := Set EReal) (Ioi 1) (⊤, ⊤).2
⊢ (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
      (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)

Tactic:
split_ands
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
⊢ ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2

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

Premises used: Set.mem_Ioi, max_lt_iff, Set.mem_prod
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
⊢ 1 < p.2

Tactic:
rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
p2_gt_1 : 1 < p.2
⊢ (↑x : EReal) < p.1

Tactic:
rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
⊢ 0 < p.1

Tactic:
rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
p1_pos : 0 < p.1
⊢ p.1 * 1 ≤ p.1 * p.2

Tactic:
have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
p1_pos : 0 < p.1
this : p.1 * 1 ≤ p.1 * p.2
⊢ p.1 ≤ p.1 * p.2

Tactic:
rw [mul_one p.1] at this

Premises used: Prod.fst, mul_one
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
p1_pos : 0 < p.1
this : p.1 ≤ p.1 * p.2
⊢ (↑x : EReal) < p.1 * p.2

Tactic:
lt_of_lt_of_le p1_gt_x this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
p1_pos : 0 < p.1
this : p.1 ≤ p.1 * p.2
⊢ (↑x : EReal) < p.1 * p.2

Tactic:
exact lt_of_lt_of_le p1_gt_x this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
⊢ IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1))

Tactic:
IsOpen.prod isOpen_Ioi isOpen_Ioi

Premises used: isOpen_Ioi, IsOpen.prod
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
⊢ IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1))

Tactic:
exact IsOpen.prod isOpen_Ioi isOpen_Ioi

Premises used: isOpen_Ioi, IsOpen.prod
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x : EReal) 0)

Tactic:
simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
⊢ (↑1 : EReal) < (⊤, ⊤).2

Tactic:
EReal.coe_lt_top 1

Premises used: OfNat.ofNat, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : ℝ
⊢ (↑1 : EReal) < (⊤, ⊤).2

Tactic:
exact EReal.coe_lt_top 1

Premises used: OfNat.ofNat, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 * a.2
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

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

Premises used: EReal.top_mul_coe_of_pos, ContinuousAt, EReal.tendsto_nhds_top_iff_real
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
rw : ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, (↑a : EReal)) ∈ t
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 * a.2

Tactic:
rw [_root_.eventually_nhds_iff]

Premises used: eventually_nhds_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
h₁ :
  (∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)) ∧
      (⊤, (↑a : EReal)) ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)
⊢ ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, (↑a : EReal)) ∈ t

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

Premises used: Set.Ioi, HMul.hMul, HDiv.hDiv, HAdd.hAdd, Max.max, OfNat.ofNat, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
h₁ : ∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2
h₂ : IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal))
h₃ : (⊤, (↑a : EReal)).1 ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal)
h₄ : (⊤, (↑a : EReal)).2 ∈ Ioi (↑(a / 2) : EReal)
⊢ (∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)) ∧
      (⊤, (↑a : EReal)) ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)

Tactic:
split_ands
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)
⊢ (↑(2 * max (x + 1) 0 / a) : EReal) < p.1 ∧ (↑(a / 2) : EReal) < p.2

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

Premises used: Set.mem_Ioi, Set.mem_prod
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1 ∧ (↑(a / 2) : EReal) < p.2
⊢ (↑(2 * max (x + 1) 0 / a) : EReal) < p.1

Tactic:
rcases p_in_prod with ⟨p1_gt, p2_gt⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1 ∧ (↑(a / 2) : EReal) < p.2
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
⊢ (↑(a / 2) : EReal) < p.2

Tactic:
rcases p_in_prod with ⟨p1_gt, p2_gt⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
apply : 0 ≤ (↑(2 * max (x + 1) 0 / a) : EReal)
⊢ 0 < p.1

Tactic:
apply lt_of_le_of_lt _ p1_gt

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
rw : 0 ≤ 2 * max (x + 1) 0 / a
⊢ 0 ≤ (↑(2 * max (x + 1) 0 / a) : EReal)

Tactic:
rw [EReal.coe_nonneg]

Premises used: EReal.coe_nonneg
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
apply : 0 ≤ 2 * max (x + 1) 0
⊢ 0 ≤ 2 * max (x + 1) 0 / a

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

Premises used: mul_nonneg, le_of_lt, inv_pos_of_pos
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
⊢ 0 ≤ 2 * max (x + 1) 0

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

Premises used: le_refl, Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, or_true
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
⊢ 0 < p.1

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 [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, le_refl, or_true]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
rw : 0 < a / 2
⊢ 0 < (↑(a / 2) : EReal)

Tactic:
rw [EReal.coe_pos]

Premises used: EReal.coe_pos
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
linarith : a / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : a / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : a / 2 ≤ 0 → 0 - a + (1 * a - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 < a / 2

Tactic:
linarith
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
⊢ 0 < (↑(a / 2) : EReal)

Tactic:
have a2_pos : 0 < ((a / 2 : ℝ) : EReal) := by rw [EReal.coe_pos]; linarith
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
⊢ (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * (↑(a / 2) : EReal)

Tactic:
have lock := mul_le_mul_of_nonneg_right (le_of_lt p1_gt) (le_of_lt a2_pos)
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * (↑(a / 2) : EReal)
⊢ p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2

Tactic:
have key := mul_le_mul_of_nonneg_left (le_of_lt p2_gt) (le_of_lt p1_pos)
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
⊢ (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2

Tactic:
replace lock := le_trans lock key
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2
apply : (↑x : EReal) < (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal)
⊢ (↑x : EReal) < p.1 * p.2

Tactic:
apply lt_of_lt_of_le _ lock

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2
rw : x < a / a * (2 / 2 * max (x + 1) 0)
⊢ (↑x : EReal) < (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal)

Tactic:
rw [← EReal.coe_mul, EReal.coe_lt_coe_iff, _root_.div_mul_div_comm, mul_comm,
      ← _root_.div_mul_div_comm, mul_div_right_comm]

Premises used: div_mul_div_comm, mul_div_right_comm, mul_comm, EReal.coe_mul, EReal.coe_lt_coe_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2
⊢ x < a / a * (2 / 2 * max (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]

Premises used: lt_add_iff_pos_right, OfNat.ofNat_ne_zero, true_or, Ne.symm, ne_eq, zero_lt_one, not_false_eq_true, ne_of_lt, one_mul, div_self, lt_max_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal))

Tactic:
IsOpen.prod isOpen_Ioi isOpen_Ioi

Premises used: isOpen_Ioi, IsOpen.prod
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal))

Tactic:
exact IsOpen.prod isOpen_Ioi isOpen_Ioi

Premises used: isOpen_Ioi, IsOpen.prod
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, (↑a : EReal)).1 ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal)

Tactic:
simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, (↑a : EReal)).2 ∈ Ioi (↑(a / 2) : EReal)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : a ≠ 0
inl : ∀ (a_neg : a < 0), ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
inr : ∀ (a_pos : 0 < a), ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
rcases lt_or_gt_of_ne h with a_neg | a_pos

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
neg_neg a ▸ continuousAt_mul_symm2 (continuousAt_mul_top_pos (neg_pos.2 a_neg))

Premises used: Iff.mpr, neg_pos, Eq.rec, neg_neg, _private.0.EReal.continuousAt_mul_top_pos, _private.0.EReal.continuousAt_mul_symm2
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
exact neg_neg a ▸ continuousAt_mul_symm2 (continuousAt_mul_top_pos (neg_pos.2 a_neg))
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
continuousAt_mul_top_pos a_pos

Premises used: _private.0.EReal.continuousAt_mul_top_pos
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))

Tactic:
exact continuousAt_mul_top_pos a_pos

Premises used: _private.0.EReal.continuousAt_mul_top_pos
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
p : EReal × EReal
h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥
h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤
h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0
h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0
rcases :
  ∀ (x y : EReal) (h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥) (h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤)
    (h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0) (h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (x, y)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) p

Tactic:
rcases p with ⟨x, y⟩
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
bot :
  ∀ (h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥) (h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0) (h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, y)
coe :
  ∀ (a : ℝ) (h₁ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥)
    (h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤) (h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0)
    (h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), y)
top :
  ∀ (h₁ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊥) (h₂ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ 0) (h₄ : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, y)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (x, y)

Tactic:
induction x
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0
bot :
  ∀ (h₁ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
    (h₂ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤)
    (h₃ : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 0)
    (h₄ : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊥)
bot₁ :
  ∀ (a : ℝ) (h₁ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥)
    (h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ 0)
    (h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, (↑a : EReal))
bot₂ :
  ∀ (h₁ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥)
    (h₂ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤)
    (h₃ : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 0)
    (h₄ : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊤)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, y)

Tactic:
induction y
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
y : EReal
a : ℝ
h₁ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥
h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤
h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0
h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0
coe :
  ∀ (h₁ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
    (h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤)
    (h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0)
    (h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊥)
coe₁ :
  ∀ (a_1 : ℝ) (h₁ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥)
    (h₂ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤)
    (h₃ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0)
    (h₄ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), (↑a_1 : EReal))
coe₂ :
  ∀ (h₁ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥)
    (h₂ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤)
    (h₃ : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0)
    (h₄ : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊤)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), y)

Tactic:
induction y
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ 0
top :
  ∀ (h₁ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
    (h₂ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤)
    (h₃ : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 0)
    (h₄ : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊥)
top₁ :
  ∀ (a : ℝ) (h₁ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥)
    (h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0)
    (h₄ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
top₂ :
  ∀ (h₁ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥)
    (h₂ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤)
    (h₃ : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 0)
    (h₄ : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊤)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, y)

Tactic:
induction y
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥
h₂ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤
h₃ : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 0
h₄ : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊥)

Tactic:
continuousAt_mul_symm3 continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top, _private.0.EReal.continuousAt_mul_symm3, EReal.neg
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h₁ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥
h₂ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤
h₃ : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 0
h₄ : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊥)

Tactic:
exact continuousAt_mul_symm3 continuousAt_mul_top_top

Premises used: _private.0.EReal.continuousAt_mul_top_top, _private.0.EReal.continuousAt_mul_symm3
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ 0
h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0
⊢ ¬a = 0

Tactic:
simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃

Premises used: not_true_eq_false, false_or, ne_eq, EReal.coe_eq_zero
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤
h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0
h₃ : ¬a = 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, (↑a : EReal))

Tactic:
continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)

Premises used: _private.0.EReal.continuousAt_mul_top_ne_zero, _private.0.EReal.continuousAt_mul_symm1, EReal.neg