awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)
⊢ Continuous[instTopologicalSpaceProd, _] fun (b : α × α) ↦ edist b.1 b.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)
⊢ Continuous[instTopologicalSpaceProd, _] fun (b : α × α) ↦ (↑K : ℝ≥0∞) * edist b.1 b.2

Tactic:
exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop)

Premises used: Continuous.comp, ENNReal.continuous_const_mul
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}

Tactic:
have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
    apply isClosed_le (by fun_prop)
    exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop)
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
apply : s ×ˢ s ⊆ {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
⊢ Dense.{u_4} (X := α × α)
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}

Tactic:
apply (hs.prod hs).mono

Premises used: Dense.mono, Dense.prod
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
⊢ hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)

Tactic:
have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
⊢ hs.extend (s := s) f y = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Ay : hs.extend (s := s) f y = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
simp :
  edist (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)) ≤
    (↑K : ℝ≥0∞) * edist x y
⊢ Membership.mem (γ := Set (α × α))
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2} (x, y)

Tactic:
simp only [Set.mem_setOf_eq, Ax, Ay]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Ay : hs.extend (s := s) f y = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ edist (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)) ≤
    (↑K : ℝ≥0∞) * edist x y

Tactic:
hf ⟨x, hx⟩ ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
x y : α
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
Ax : hs.extend (s := s) f x = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Ay : hs.extend (s := s) f y = f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ edist (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) (f (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)) ≤
    (↑K : ℝ≥0∞) * edist x y

Tactic:
exact hf ⟨x, hx⟩ ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
⊢ Dense.{u_4} (X := α × α)
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}

Tactic:
have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by
    apply (hs.prod hs).mono
    rintro ⟨x, y⟩ ⟨hx, hy⟩
    have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩
    have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩
    simp only [Set.mem_setOf_eq, Ax, Ay]
    exact hf ⟨x, hx⟩ ⟨y, hy⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this_1 :
  IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
this :
  Dense.{u_4} (X := α × α)
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}
⊢ LipschitzWith K (hs.extend (s := s) f)

Tactic:
simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq, Prod.forall] using this

Premises used: IsClosed.closure_eq, Dense, Set.mem_setOf_eq, Prod.forall
-- Module: Mathlib.Topology.Instances.ENat
Goal:
⊢ OrderTopology ℕ∞

Tactic:
⟨rfl⟩

Premises used: OrderTopology.mk, rfl
-- Module: Mathlib.Topology.Instances.ENat
Goal:
⊢ Eq (α := Set ℕ∞) (range Nat.cast) (Iio ⊤)

Tactic:
WithTop.range_coe

Premises used: ENat, WithTop.range_coe
-- Module: Mathlib.Topology.Instances.ENat
Goal:
⊢ IsEmbedding (Y := ℕ∞) Nat.cast

Tactic:
Nat.strictMono_cast.isEmbedding_of_ordConnected <| range_natCast ▸ ordConnected_Iio

Premises used: StrictMono.isEmbedding_of_ordConnected, Nat.strictMono_cast
-- Module: Mathlib.Topology.Instances.ENat
Goal:
⊢ IsOpenEmbedding (Y := ℕ∞) Nat.cast

Tactic:
⟨isEmbedding_natCast, range_natCast ▸ isOpen_Iio⟩

Premises used: Eq.rec, isOpen_Iio, ENat.isEmbedding_natCast, Eq.symm, Topology.IsOpenEmbedding.mk, ENat.range_natCast
-- Module: Mathlib.Topology.Instances.ENat
Goal:
n : ℕ
⊢ Eq (α := Filter ℕ∞) (𝓝 (↑n : ℕ∞)) (pure (↑n : ℕ∞))

Tactic:
simp [← isOpenEmbedding_natCast.map_nhds_eq]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, ENat.isOpenEmbedding_natCast
-- Module: Mathlib.Topology.Instances.ENat
Goal:
n : ℕ∞
h : n ≠ ⊤
⊢ n ≠ ⊤

Tactic:
h
-- Module: Mathlib.Topology.Instances.ENat
Goal:
n : ℕ∞
h : n ≠ ⊤
lift : ∀ (n : ℕ), Eq (α := Filter ℕ∞) (𝓝 (↑n : ℕ∞)) (pure (↑n : ℕ∞))
⊢ 𝓝 n = pure n

Tactic:
lift n to ℕ using h
-- Module: Mathlib.Topology.Instances.ENat
Goal:
n : ℕ
⊢ Eq (α := Filter ℕ∞) (𝓝 (↑n : ℕ∞)) (pure (↑n : ℕ∞))

Tactic:
simp [nhds_natCast]

Premises used: ENat.nhds_natCast
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞
hx : x ≠ ⊤
rw : 𝓝 x = pure x
rw₁ rw₂ : Eq (α := Filter ℕ∞) (pure x) (pure x)
⊢ IsOpen (X := ℕ∞) {x}

Tactic:
rw [isOpen_singleton_iff_nhds_eq_pure, ENat.nhds_eq_pure hx]

Premises used: ENat.nhds_eq_pure, isOpen_singleton_iff_nhds_eq_pure
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Instances.ENat
Goal:
n : ℕ
s : Set ℕ∞
⊢ Membership.mem (γ := Filter ℕ∞) (𝓝 (↑n : ℕ∞)) s ↔ (↑n : ℕ∞) ∈ s

Tactic:
mem_nhds_iff (coe_ne_top _)

Premises used: ENat.mem_nhds_iff, ENat.coe_ne_top
-- Module: Mathlib.Topology.Instances.ENat
Goal:
α : Type u_1
l : Filter α
f : α → ℕ∞
simp_rw : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l < ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₁ : Tendsto f l (⨅ (l : ℕ∞), ⨅ (_ : l ≠ ⊤), 𝓟 (Ioi l)) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₂ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), Tendsto f l (𝓟 (Ioi i))) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₃ : (∀ (i : ℕ∞) (i_1 : i ≠ ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
simp_rw₄ :
  (∀ (x : ℕ), ∀ᶠ (a : α) in l, Membership.mem (γ := Set ℕ∞) (Ioi (↑x : ℕ∞)) (f a)) ↔
    ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a
⊢ Tendsto f l (𝓝 ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, (↑n : ℕ∞) < f a

Tactic:
simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top,
    mem_Ioi]

Premises used: Set.mem_Ioi, Filter.tendsto_principal, lt_top_iff_ne_top, nhds_top_order, Filter.tendsto_iInf, ENat.forall_ne_top
-- Module: Mathlib.Topology.Instances.ENat
Goal:
⊢ ContinuousAdd ℕ∞

Tactic:
⟨continuous_iff_continuousAt.2 fun (a, b) ↦ ?_⟩

Premises used: Iff.mpr, _private.0.ENat.instContinuousAdd.match_1, ContinuousAt, Prod.fst, HAdd.hAdd, Prod.snd, ContinuousAdd.mk, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.ENat
Goal:
refine : ∀ (x : ℕ∞ × ℕ∞) (a b : ℕ∞), ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) (a, b)
⊢ ContinuousAdd ℕ∞

Tactic:
refine ⟨continuous_iff_continuousAt.2 fun (a, b) ↦ ?_⟩
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞ × ℕ∞
a b x_1 : ℕ∞
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) (⊤, x_1)

Tactic:
tendsto_nhds_top_mono' continuousAt_fst fun p ↦ le_add_right le_rfl

Premises used: le_rfl, ContinuousAt, WithTop.map₂, tendsto_nhds_top_mono', continuousAt_fst, Option.map₂, le_add_right
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞ × ℕ∞
a b x_1 : ℕ∞
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) (⊤, x_1)

Tactic:
exact tendsto_nhds_top_mono' continuousAt_fst fun p ↦ le_add_right le_rfl
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞ × ℕ∞
a_1 b : ℕ∞
a : ℕ
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) ((↑a : ℕ∞), ⊤)

Tactic:
tendsto_nhds_top_mono' continuousAt_snd fun p ↦ le_add_left le_rfl

Premises used: le_rfl, ContinuousAt, WithTop.map₂, tendsto_nhds_top_mono', continuousAt_snd, Option.map₂, le_add_left
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞ × ℕ∞
a_1 b : ℕ∞
a : ℕ
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) ((↑a : ℕ∞), ⊤)

Tactic:
exact tendsto_nhds_top_mono' continuousAt_snd fun p ↦ le_add_left le_rfl
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞ × ℕ∞
a_1 b_1 : ℕ∞
a b : ℕ
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) ((↑a : ℕ∞), (↑b : ℕ∞))

Tactic:
simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]

Premises used: ContinuousAt, tendsto_pure_nhds, nhds_prod_eq
-- Module: Mathlib.Topology.Instances.ENat
Goal:
x : ℕ∞ × ℕ∞
a b : ℕ∞
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 + p.2) (a, b)

Tactic:
match a, b with
  | ⊤, _ => exact tendsto_nhds_top_mono' continuousAt_fst fun p ↦ le_add_right le_rfl
  | (a : ℕ), ⊤ => exact tendsto_nhds_top_mono' continuousAt_snd fun p ↦ le_add_left le_rfl
  | (a : ℕ), (b : ℕ) => simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
inl : ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (0, ⊤)
inr : ∀ (ha : 0 < a), ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)

Tactic:
rcases eq_zero_or_pos a with rfl | ha

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Topology.Instances.ENat
Goal:
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (0, ⊤)

Tactic:
simp [ContinuousAt, nhds_prod_eq]

Premises used: ContinuousAt, nhds_prod_eq
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
inr : Tendsto (α := ℕ∞ × ℕ∞) (β := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (𝓝 (a, ⊤)) (𝓝 ⊤)
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)

Tactic:
simp only [ContinuousAt, Function.uncurry, mul_top ha.ne']

Premises used: ContinuousAt, LT.lt.ne', Function.uncurry, ENat.mul_top
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
⊢ Tendsto (α := ℕ∞ × ℕ∞) (β := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (𝓝 (a, ⊤)) (𝓝 ⊤)

Tactic:
tendsto_nhds_top_mono continuousAt_snd ?_

Premises used: tendsto_nhds_top_mono, continuousAt_snd
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
inr : EventuallyLE (α := ℕ∞ × ℕ∞) (𝓝 (a, ⊤)) Prod.snd (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2)
⊢ Tendsto (α := ℕ∞ × ℕ∞) (β := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (𝓝 (a, ⊤)) (𝓝 ⊤)

Tactic:
refine tendsto_nhds_top_mono continuousAt_snd ?_
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
x y : ℕ∞
h : ∀ (hx : 0 < x), (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)
⊢ Membership.mem (γ := Set (ℕ∞ × ℕ∞)) (Prod.fst ⁻¹' {x : ℕ∞ | 0 < x}) (x, y) →
    (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)

Tactic:
(hx : 0 < x)
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
h : ∀ (x y : ℕ∞) (hx : 0 < x), (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)
⊢ EventuallyLE (α := ℕ∞ × ℕ∞) (𝓝 (a, ⊤)) Prod.snd (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2)

Tactic:
filter_upwards [continuousAt_fst (lt_mem_nhds ha)] with (x, y) (hx : 0 < x)

Premises used: continuousAt_fst, lt_mem_nhds
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
x y : ℕ∞
hx : 0 < x
⊢ (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)

Tactic:
le_mul_of_one_le_left' (Order.one_le_iff_pos.2 hx)

Premises used: Iff.mpr, le_mul_of_one_le_left', Order.one_le_iff_pos
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a : ℕ∞
ha : 0 < a
x y : ℕ∞
hx : 0 < x
⊢ (x, y).2 ≤ Function.uncurry (fun (x1 x2 : ℕ∞) ↦ x1 * x2) (x, y)

Tactic:
exact le_mul_of_one_le_left' (Order.one_le_iff_pos.2 hx)

Premises used: Iff.mpr, le_mul_of_one_le_left', Order.one_le_iff_pos
-- Module: Mathlib.Topology.Instances.ENat
Goal:
key : ∀ (a : ℕ∞), ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 * x2) (a, ⊤)
a b : ℕ
⊢ ContinuousAt (Y := ℕ∞) (fun (p : ℕ∞ × ℕ∞) ↦ p.1 * p.2) ((↑a : ℕ∞), (↑b : ℕ∞))

Tactic:
simp [ContinuousAt, nhds_prod_eq, tendsto_pure_nhds]

Premises used: ContinuousAt, tendsto_pure_nhds, nhds_prod_eq
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a_1 b_1 : ℕ∞
h : a_1 ≠ ⊤ ∨ b_1 ≠ ⊤
a b : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) (↑b : ℕ∞) ⊤
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) ((↑a : ℕ∞), (↑b : ℕ∞))

Tactic:
simp [ContinuousAt, nhds_prod_eq]

Premises used: ContinuousAt, nhds_prod_eq
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a_1 b : ℕ∞
h : a_1 ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
this : ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, (↑a : ℕ∞) - b = 0
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) ((↑a : ℕ∞), ⊤)

Tactic:
simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le, ContinuousAt, nhds_prod_eq
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a_1 b : ℕ∞
h : a_1 ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
suffices : ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, (↑a : ℕ∞) - b = 0
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) ((↑a : ℕ∞), ⊤)

Tactic:
suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
      simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a_1 b_1 : ℕ∞
h : a_1 ≠ ⊤ ∨ b_1 ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
b : ℕ∞
⊢ (↑a : WithTop ℕ) ≤ b → (↑a : ℕ∞) - b = 0

Tactic:
tsub_eq_zero_of_le

Premises used: tsub_eq_zero_of_le
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a_1 b : ℕ∞
h : a_1 ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
h_1 : Ne (α := ℕ∞) (↑a : ℕ∞) ⊤ ∨ Ne (α := ℕ∞) ⊤ ⊤
h₁ :
  ∀ (a_2 : ℕ∞),
    Membership.mem (γ := Set ℕ∞)
      {x : ℕ∞ |
        Membership.mem (γ := Set ℕ∞) {x : ℕ∞ | (fun (x : ℕ∞) ↦ (↑a : WithTop ℕ) ≤ x) x} x →
          Membership.mem (γ := Set ℕ∞) {x : ℕ∞ | (fun (b : ℕ∞) ↦ (↑a : ℕ∞) - b = 0) x} x}
      a_2
h₂ h₃ : ∀ (b : ℕ∞), (↑a : WithTop ℕ) ≤ b → (↑a : ℕ∞) - b = 0
⊢ ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, (↑a : ℕ∞) - b = 0

Tactic:
filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le

Premises used: tsub_eq_zero_of_le
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a b_1 : ℕ∞
h : a ≠ ⊤ ∨ b_1 ≠ ⊤
b : ℕ
h_1 : Ne (α := ℕ∞) ⊤ ⊤ ∨ Ne (α := ℕ∞) (↑b : ℕ∞) ⊤
this : ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, HAdd.hAdd (α := ℕ∞) (↑b : ℕ∞) (↑n : ℕ∞) < a
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) (⊤, (↑b : ℕ∞))

Tactic:
simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]

Premises used: ContinuousAt, Function.comp, nhds_prod_eq, ENat.tendsto_nhds_top_iff_natCast_lt, lt_tsub_iff_left
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a b_1 : ℕ∞
h : a ≠ ⊤ ∨ b_1 ≠ ⊤
b : ℕ
h_1 : Ne (α := ℕ∞) ⊤ ⊤ ∨ Ne (α := ℕ∞) (↑b : ℕ∞) ⊤
suffices : ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, HAdd.hAdd (α := ℕ∞) (↑b : ℕ∞) (↑n : ℕ∞) < a
⊢ ContinuousAt (X := ℕ∞ × ℕ∞) (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) (⊤, (↑b : ℕ∞))

Tactic:
suffices ∀ n : ℕ, ∀ᶠ a : ℕ∞ in 𝓝 ⊤, b + n < a by
      simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a b_1 : ℕ∞
h : a ≠ ⊤ ∨ b_1 ≠ ⊤
b : ℕ
h_1 : Ne (α := ℕ∞) ⊤ ⊤ ∨ Ne (α := ℕ∞) (↑b : ℕ∞) ⊤
⊢ ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, HAdd.hAdd (α := ℕ∞) (↑b : ℕ∞) (↑n : ℕ∞) < a

Tactic:
fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)

Premises used: WithTop.coe_lt_top, HAdd.hAdd, lt_mem_nhds
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a b_1 : ℕ∞
h : a ≠ ⊤ ∨ b_1 ≠ ⊤
b : ℕ
h_1 : Ne (α := ℕ∞) ⊤ ⊤ ∨ Ne (α := ℕ∞) (↑b : ℕ∞) ⊤
⊢ ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, HAdd.hAdd (α := ℕ∞) (↑b : ℕ∞) (↑n : ℕ∞) < a

Tactic:
exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)
-- Module: Mathlib.Topology.Instances.ENat
Goal:
a b : ℕ∞
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ ContinuousAt (Y := ℕ∞) (Function.uncurry fun (x1 x2 : ℕ∞) ↦ x1 - x2) (a, b)

Tactic:
match a, b, h with
  | (a : ℕ), (b : ℕ), _ => simp [ContinuousAt, nhds_prod_eq]
  | (a : ℕ), ⊤, _ =>
    suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
      simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]
    filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le
  | ⊤, (b : ℕ), _ =>
    suffices ∀ n : ℕ, ∀ᶠ a : ℕ∞ in 𝓝 ⊤, b + n < a by
      simpa [ContinuousAt, nhds_prod_eq, (· ∘ ·), lt_tsub_iff_left, tendsto_nhds_top_iff_natCast_lt]
    exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)
-- Module: Mathlib.Topology.Instances.ENat
Goal:
α : Type u_1
l : Filter α
f g : α → ℕ∞
a b : ℕ∞
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ Tendsto (fun (x : α) ↦ f x - g x) l (𝓝 (a - b))

Tactic:
(ENat.continuousAt_sub h).tendsto.comp (hf.prodMk_nhds hg)

Premises used: ENat.continuousAt_sub, ContinuousAt.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Instances.ENat
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : X → ℕ∞
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
h : f x ≠ ⊤ ∨ g x ≠ ⊤
⊢ ContinuousWithinAt (Y := ℕ∞) (fun (x : X) ↦ f x - g x) s x

Tactic:
hf.enatSub hg h

Premises used: ContinuousWithinAt, Filter.Tendsto.enatSub
-- Module: Mathlib.Topology.Instances.ENat
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : X → ℕ∞
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
h : f x ≠ ⊤ ∨ g x ≠ ⊤
⊢ ContinuousAt (Y := ℕ∞) (fun (x : X) ↦ f x - g x) x

Tactic:
hf.enatSub hg h

Premises used: ContinuousAt, Filter.Tendsto.enatSub
-- Module: Mathlib.Topology.Instances.ENat
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : X → ℕ∞
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
h : ∀ x ∈ s, f x ≠ ⊤ ∨ g x ≠ ⊤
⊢ ContinuousOn (Y := ℕ∞) (fun (x : X) ↦ f x - g x) s

Tactic:
fun x hx ↦
  (hf x hx).enatSub (hg x hx) (h x hx)

Premises used: ContinuousWithinAt.enatSub, ContinuousOn
-- Module: Mathlib.Topology.Instances.ENat
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : X → ℕ∞
hf : Continuous[inst, _] f
hg : Continuous[inst, _] g
h : ∀ (x : X), f x ≠ ⊤ ∨ g x ≠ ⊤
⊢ Continuous[inst, _] fun (x : X) ↦ f x - g x

Tactic:
continuous_iff_continuousAt.2 fun x ↦ hf.continuousAt.enatSub hg.continuousAt (h x)

Premises used: Iff.mpr, ContinuousAt.enatSub, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
rw : OrdConnected (α := EReal) (Ioo ⊥ ⊤)
⊢ (range Real.toEReal).OrdConnected

Tactic:
rw [range_coe_eq_Ioo]

Premises used: EReal.range_coe_eq_Ioo
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ OrdConnected (α := EReal) (Ioo ⊥ ⊤)

Tactic:
ordConnected_Ioo

Premises used: Set.ordConnected_Ioo
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ OrdConnected (α := EReal) (Ioo ⊥ ⊤)

Tactic:
exact ordConnected_Ioo

Premises used: Set.ordConnected_Ioo
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ IsOpen (range Real.toEReal)

Tactic:
simp only [range_coe_eq_Ioo, isOpen_Ioo]

Premises used: isOpen_Ioo, EReal.range_coe_eq_Ioo
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → ℝ
a : ℝ
⊢ Tendsto (fun (a : α) ↦ (↑(m a) : EReal)) f (𝓝 (↑a : EReal)) ↔ Tendsto m f (𝓝 a)

Tactic:
isEmbedding_coe.tendsto_nhds_iff.symm

Premises used: Topology.IsEmbedding.tendsto_nhds_iff, EReal.isEmbedding_coe, Iff.symm, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ Continuous Real.toEReal

Tactic:
isEmbedding_coe.continuous

Premises used: EReal.isEmbedding_coe, Topology.IsEmbedding.continuous