awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
refine : ∀ (r : ℝ) (x : EReal × EReal) (h : (↑0 : EReal) < x.1 ∧ (↑r : EReal) < x.2), (↑r : EReal) < x.1 + x.2
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 + a.2

Tactic:
refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_

Premises used: Filter.Eventually.mono, Filter.Eventually.prod_nhds, OfNat.ofNat, lt_mem_nhds, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
r : ℝ
x : EReal × EReal
h : (↑0 : EReal) < x.1 ∧ (↑r : EReal) < x.2
⊢ (↑r : EReal) < x.1 + x.2

Tactic:
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

Premises used: EReal.coe_zero, zero_add, And.right, And.left, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, (↑a : EReal)), a.1 + a.2 < (↑x : EReal)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]

Premises used: ContinuousAt, EReal.bot_add, EReal.tendsto_nhds_bot_iff_real
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, (↑a : EReal)), a.1 + a.2 < (↑x : EReal)

Tactic:
fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_

Premises used: Iff.mpr, gt_mem_nhds, lt_add_one, EReal.bot_lt_coe, HSub.hSub, Filter.Eventually.mono, HAdd.hAdd, Filter.Eventually.prod_nhds, OfNat.ofNat, EReal.coe_lt_coe_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
refine :
  ∀ (r : ℝ) (x : EReal × EReal) (h : x.1 < (↑(r - (a + 1)) : EReal) ∧ x.2 < (↑(a + 1) : EReal)),
    x.1 + x.2 < (↑r : EReal)
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, (↑a : EReal)), a.1 + a.2 < (↑x : EReal)

Tactic:
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_

Premises used: Iff.mpr, gt_mem_nhds, lt_add_one, EReal.bot_lt_coe, HSub.hSub, Filter.Eventually.mono, HAdd.hAdd, Filter.Eventually.prod_nhds, OfNat.ofNat, EReal.coe_lt_coe_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a r : ℝ
x : EReal × EReal
h : x.1 < (↑(r - (a + 1)) : EReal) ∧ x.2 < (↑(a + 1) : EReal)
⊢ x.1 + x.2 < (↑r : EReal)

Tactic:
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

Premises used: And.right, And.left, EReal.coe_add, EReal.add_lt_add, sub_add_cancel
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)

Tactic:
simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
    using Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))

Premises used: ContinuousAt, continuous_swap, Prod.mk, Bot.bot, EReal.continuousAt_add_bot_coe, add_comm, Continuous.tendsto, Function.comp_def, Prod.swap, Filter.Tendsto.comp, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < (↑x : EReal)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]

Premises used: ContinuousAt, EReal.bot_add, EReal.tendsto_nhds_bot_iff_real
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < (↑x : EReal)

Tactic:
fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
    (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_

Premises used: gt_mem_nhds, EReal.bot_lt_coe, Filter.Eventually.mono, Filter.Eventually.prod_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
refine : ∀ (r : ℝ) (x : EReal × EReal) (h : x.1 < (↑0 : EReal) ∧ x.2 < (↑r : EReal)), x.1 + x.2 < (↑r : EReal)
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < (↑x : EReal)

Tactic:
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
    (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_

Premises used: gt_mem_nhds, EReal.bot_lt_coe, Filter.Eventually.mono, Filter.Eventually.prod_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
r : ℝ
x : EReal × EReal
h : x.1 < (↑0 : EReal) ∧ x.2 < (↑r : EReal)
⊢ x.1 + x.2 < (↑r : EReal)

Tactic:
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

Premises used: EReal.coe_zero, zero_add, And.right, And.left, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
p : EReal × EReal
h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥
h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤
rcases :
  ∀ (x y : EReal) (h : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ ⊥) (h' : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ ⊤),
    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 ≠ ⊤ ∨ (x, y).2 ≠ ⊥
h' : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ ⊤
bot :
  ∀ (h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥) (h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
coe :
  ∀ (a : ℝ) (h : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥)
    (h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), y)
top :
  ∀ (h : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ ⊥) (h' : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ ⊤),
    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 ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤
bot :
  ∀ (h : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
    (h' : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)
bot₁ :
  ∀ (a : ℝ) (h : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ ⊥)
    (h' : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))
bot₂ :
  ∀ (h : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥)
    (h' : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤),
    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 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥
h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤
coe :
  ∀ (h : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
    (h' : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)
coe₁ :
  ∀ (a_1 : ℝ) (h : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥)
    (h' : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), (↑a_1 : EReal))
coe₂ :
  ∀ (h : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥)
    (h' : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤),
    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 ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ ⊤
top :
  ∀ (h : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
    (h' : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊥)
top₁ :
  ∀ (a : ℝ) (h : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ ⊥)
    (h' : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))
top₂ :
  ∀ (h : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥)
    (h' : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤),
    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 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥
h' : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)

Tactic:
continuousAt_add_bot_bot

Premises used: EReal.continuousAt_add_bot_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥
h' : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)

Tactic:
exact continuousAt_add_bot_bot

Premises used: EReal.continuousAt_add_bot_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ ⊥
h' : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))

Tactic:
continuousAt_add_bot_coe _

Premises used: EReal.continuousAt_add_bot_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ ⊥
h' : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))

Tactic:
exact continuousAt_add_bot_coe _

Premises used: EReal.continuousAt_add_bot_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥
h' : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊤)

Tactic:
simp at h'
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥
h' : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)

Tactic:
continuousAt_add_coe_bot _

Premises used: EReal.continuousAt_add_coe_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥
h' : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)

Tactic:
exact continuousAt_add_coe_bot _

Premises used: EReal.continuousAt_add_coe_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a a_1 : ℝ
h : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥
h' : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), (↑a_1 : EReal))

Tactic:
continuousAt_add_coe_coe _ _

Premises used: EReal.continuousAt_add_coe_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a a_1 : ℝ
h : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥
h' : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), (↑a_1 : EReal))

Tactic:
exact continuousAt_add_coe_coe _ _

Premises used: EReal.continuousAt_add_coe_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥
h' : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊤)

Tactic:
continuousAt_add_coe_top _

Premises used: EReal.continuousAt_add_coe_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥
h' : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊤)

Tactic:
exact continuousAt_add_coe_top _

Premises used: EReal.continuousAt_add_coe_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥
h' : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊥)

Tactic:
simp at h
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ ⊥
h' : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))

Tactic:
continuousAt_add_top_coe _

Premises used: EReal.continuousAt_add_top_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
h : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ ⊥
h' : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))

Tactic:
exact continuousAt_add_top_coe _

Premises used: EReal.continuousAt_add_top_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥
h' : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
continuousAt_add_top_top

Premises used: EReal.continuousAt_add_top_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
h : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥
h' : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
exact continuousAt_add_top_top

Premises used: EReal.continuousAt_add_top_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal × EReal
y : EReal
pos :
  ∀ (hx₁ : x.1 = ⊥),
    (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
      ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
        (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
neg :
  ∀ (hx₁ : ¬x.1 = ⊥),
    (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
      ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
        (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
by_cases hx₁ : x.1 = ⊥

Premises used: Prod.fst
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal × EReal
y : EReal
hx₁ : x.1 = ⊥
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
simp [hx₁]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
pos :
  ∀ (hx₂ : x.2 = ⊥),
    (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
      ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
        (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
neg :
  ∀ (hx₂ : ¬x.2 = ⊥),
    (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
      ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
        (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
by_cases hx₂ : x.2 = ⊥

Premises used: Prod.snd
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : x.2 = ⊥
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
simp [hx₂]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
continuousAt_add (.inr hx₂) (.inl hx₁) |>.lowerSemicontinuousAt _

Premises used: EReal.continuousAt_add, Or.inl, ContinuousAt.lowerSemicontinuousAt, Or.inr
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
exact continuousAt_add (.inr hx₂) (.inl hx₁) |>.lowerSemicontinuousAt _

Premises used: EReal.continuousAt_add, Or.inl, ContinuousAt.lowerSemicontinuousAt, Or.inr
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (Y := EReal) ((fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ Prod.swap) (b, a)

Tactic:
h.comp continuous_swap.continuousAt (x := (b, a))

Premises used: continuous_swap, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
h₁ : ∀ (x : EReal × EReal), x.1 * x.2 = ((fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ Prod.swap) x
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (b, a)

Tactic:
convert! h.comp continuous_swap.continuousAt (x := (b, a))

Premises used: continuous_swap, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
x : EReal × EReal
⊢ x.1 * x.2 = ((fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ Prod.swap) x

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
h₁ :
  ∀ (p : EReal × EReal),
    p.1 * p.2 =
      ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) p
⊢ Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))

Tactic:
ext p
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
p : EReal × EReal
⊢ p.1 * p.2 = ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) p

Tactic:
simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))

Tactic:
have : (fun p : EReal × EReal ↦ p.1 * p.2) = (fun x : EReal ↦ -x)
      ∘ (fun p : EReal × EReal ↦ p.1 * p.2) ∘ (fun p : EReal × EReal ↦ (-p.1, p.2)) := by
    ext p
    simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
this :
  Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
rw :
  ContinuousAt (Y := EReal)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) (-a, b)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (-a, b)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
this :
  Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
apply : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (Prod.map (fun (a : EReal) ↦ -a) id (-a, b))
⊢ ContinuousAt (Y := EReal)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) (-a, b)

Tactic:
apply ContinuousAt.comp (Continuous.continuousAt continuous_neg)
    <| ContinuousAt.comp _ (ContinuousAt.prodMap (Continuous.continuousAt continuous_neg)
      (Continuous.continuousAt continuous_id))

Premises used: ContinuousNeg.continuous_neg, ContinuousAt.prodMap, Continuous.continuousAt, continuous_id, ContinuousAt.comp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
this :
  Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (Prod.map (fun (a : EReal) ↦ -a) id (-a, b))

Tactic:
simp [h]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, -b)

Tactic:
continuousAt_mul_swap (continuousAt_mul_symm1 (continuousAt_mul_swap h))

Premises used: _private.0.EReal.continuousAt_mul_swap, _private.0.EReal.continuousAt_mul_symm1
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (-a, -b)

Tactic:
continuousAt_mul_symm1 (continuousAt_mul_symm2 h)

Premises used: _private.0.EReal.continuousAt_mul_symm1, _private.0.EReal.continuousAt_mul_symm2
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : ℝ
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), (↑b : EReal))

Tactic:
simp [ContinuousAt, EReal.nhds_coe_coe, ← EReal.coe_mul, Filter.tendsto_map'_iff,
    Function.comp_def, EReal.tendsto_coe, tendsto_mul]

Premises used: ContinuousAt, Filter.tendsto_map'_iff, EReal.tendsto_coe, Function.comp_def, tendsto_mul, EReal.coe_mul, EReal.nhds_coe_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 * a.2
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊤)

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

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

Tactic:
rw [_root_.eventually_nhds_iff]

Premises used: eventually_nhds_iff