awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
rcases :
  ∀ (u : Set α) (hu : IsOpen[inst] u) (htu : t =ᶠ[residual α] u), ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u

Tactic:
rcases ht.residualEq_isOpen with ⟨u, hu, htu⟩

Premises used: MeasurableSet.residualEq_isOpen
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
u : Set α
hu : IsOpen[inst] u
htu : t =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u

Tactic:
⟨u, hu, hst.trans htu⟩

Premises used: Filter.EventuallyEq.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
u : Set α
hu : IsOpen[inst] u
htu : t =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u

Tactic:
exact ⟨u, hu, hst.trans htu⟩
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ BaireMeasurableSet s ↔ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u

Tactic:
⟨fun h => h.residualEq_isOpen, fun ⟨_, uo, ueq⟩ => uo.baireMeasurableSet.congr ueq.symm⟩

Premises used: BaireMeasurableSet, _private.0.BaireMeasurableSet.iff_residualEq_isOpen.match_1, Iff.intro, BaireMeasurableSet.residualEq_isOpen, BaireMeasurableSet.congr, IsOpen.baireMeasurableSet, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
apply : {t : Set β | IsOpen[inst_1] t ∧ Dense t} ⊆ (map f (residual α)).sets
⊢ Tendsto f (residual α) (residual β)

Tactic:
apply le_countableGenerate_iff_of_countableInterFilter.mpr

Premises used: Iff.mpr, Filter.le_countableGenerate_iff_of_countableInterFilter
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
t : Set β
ht : IsOpen[inst_1] t
htd : Dense t
⊢ t ∈ (map f (residual α)).sets

Tactic:
residual_of_dense_open (ht.preimage hc) (htd.preimage ho)

Premises used: Set.Mem, setOf, residual_of_dense_open, Set.preimage, IsOpen.preimage, Dense.preimage
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
t : Set β
ht : IsOpen[inst_1] t
htd : Dense t
⊢ t ∈ (map f (residual α)).sets

Tactic:
exact residual_of_dense_open (ht.preimage hc) (htd.preimage ho)

Premises used: residual_of_dense_open, IsOpen.preimage, Dense.preimage
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s : Set β
h : IsMeagre s
⊢ IsMeagre (f ⁻¹' s)

Tactic:
tendsto_residual_of_isOpenMap hc ho h

Premises used: IsMeagre, Set.Mem, setOf, tendsto_residual_of_isOpenMap, Set.preimage, Not
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s : Set β
h : BaireMeasurableSet s
rcases : ∀ (u : Set β) (hu : MeasurableSet u) (hsu : s =ᶠ[residual β] u), BaireMeasurableSet (f ⁻¹' s)
⊢ BaireMeasurableSet (f ⁻¹' s)

Tactic:
rcases h with ⟨u, hu, hsu⟩
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ BaireMeasurableSet (f ⁻¹' s)

Tactic:
⟨f ⁻¹' u, ?_, hsu.filter_mono <| tendsto_residual_of_isOpenMap hc ho⟩

Premises used: Filter.EventuallyEq.filter_mono, BaireMeasurableSet, MeasurableSet, tendsto_residual_of_isOpenMap, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
refine : MeasurableSet (f ⁻¹' u)
⊢ BaireMeasurableSet (f ⁻¹' s)

Tactic:
refine ⟨f ⁻¹' u, ?_, hsu.filter_mono <| tendsto_residual_of_isOpenMap hc ho⟩
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α β
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this :
  let this := borel α;
  BorelSpace α
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize α β
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
⊢ MeasurableSet (f ⁻¹' u)

Tactic:
hc.measurable hu

Premises used: Continuous.measurable
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
⊢ MeasurableSet (f ⁻¹' u)

Tactic:
exact hc.measurable hu

Premises used: Continuous.measurable
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
⊢ map (⇑h : (a : α) → β) (residual α) = residual β

Tactic:
le_antisymm (tendsto_residual_of_isOpenMap h.continuous h.isOpenMap) (le_map ?_)

Premises used: Homeomorph.continuous, tendsto_residual_of_isOpenMap, le_antisymm, Filter.le_map, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
refine : ∀ s ∈ residual α, (⇑h : (a : α) → β) '' s ∈ residual β
⊢ map (⇑h : (a : α) → β) (residual α) = residual β

Tactic:
refine le_antisymm (tendsto_residual_of_isOpenMap h.continuous h.isOpenMap) (le_map ?_)

Premises used: Homeomorph.continuous, tendsto_residual_of_isOpenMap, le_antisymm, Filter.le_map, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
simp_rw : ∀ s ∈ residual α, (⇑h.symm : (a : β) → α) ⁻¹' s ∈ residual β
⊢ ∀ s ∈ residual α, (⇑h : (a : α) → β) '' s ∈ residual β

Tactic:
simp_rw [← preimage_symm]

Premises used: Homeomorph.preimage_symm
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, (⇑h.symm : (a : β) → α) ⁻¹' s ∈ residual β

Tactic:
tendsto_residual_of_isOpenMap h.symm.continuous h.symm.isOpenMap

Premises used: Homeomorph.continuous, Set.Mem, setOf, tendsto_residual_of_isOpenMap, Set.preimage, Filter.Tendsto, Homeomorph.symm, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, (⇑h.symm : (a : β) → α) ⁻¹' s ∈ residual β

Tactic:
exact tendsto_residual_of_isOpenMap h.symm.continuous h.symm.isOpenMap

Premises used: Homeomorph.continuous, tendsto_residual_of_isOpenMap, Homeomorph.symm, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ BaireSpace X

Tactic:
⟨fun f ho hd => ?_⟩

Premises used: BaireSpace.mk
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
refine :
  ∀ (f : ℕ → Set X) (ho : ∀ (n : ℕ), IsOpen (f n)) (hd : ∀ (n : ℕ), Dense (f n)), Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
⊢ BaireSpace X

Tactic:
refine ⟨fun f ho hd => ?_⟩
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) 2 n ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
⊢ ∀ (n : ℕ), 0 < B n

Tactic:
have Bpos : ∀ n, 0 < B n := fun n ↦
    ENNReal.div_pos one_ne_zero <| by finiteness
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
⊢ x ∈ closure (f n)

Tactic:
have : x ∈ closure (f n) := hd n x
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
rcases :
  ∀ (y : X) (ys : y ∈ f n) (xy : edist x y < δ / 2),
    ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n

Tactic:
rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩

Premises used: HDiv.hDiv, ENNReal.half_pos, Iff.mp, EMetric.mem_closure_iff, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist x y < δ / 2
⊢ edist y x < δ / 2

Tactic:
rw [edist_comm] at xy

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
⊢ ∃ r > 0, closedEBall y r ⊆ f n

Tactic:
nhds_basis_closedEBall.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)

Premises used: Filter.HasBasis.mem_iff, Iff.mp, isOpen_iff_mem_nhds, Metric.nhds_basis_closedEBall
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
obtain :
  ∀ (r : ℝ≥0∞) (rpos : r > 0) (hr : closedEBall y r ⊆ f n),
    ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n

Tactic:
obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedEBall y r ⊆ f n :=
      nhds_basis_closedEBall.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)

Premises used: Filter.HasBasis.mem_iff, Iff.mp, isOpen_iff_mem_nhds, Metric.nhds_basis_closedEBall
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n

Tactic:
⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩

Premises used: HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Min.min
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
refine_1 : 0 < min (min (δ / 2) r) (B (n + 1))
refine_2 : min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
refine_3 : ∀ (z : X) (hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))), z ∈ closedEBall x δ
refine_4 : ∀ (z : X) (hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))), z ∈ f n
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n

Tactic:
refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ 0 < min (min (δ / 2) r) (B (n + 1))

Tactic:
lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))

Premises used: lt_min, HAdd.hAdd, ENNReal.half_pos, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ 0 < min (min (δ / 2) r) (B (n + 1))

Tactic:
exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))

Premises used: lt_min, HAdd.hAdd, ENNReal.half_pos, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)

Tactic:
min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)

Tactic:
exact min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ edist z x ≤ edist z y + edist y x

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ edist z y + edist y x ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2

Tactic:
add_le_add hz (le_of_lt xy)

Premises used: add_le_add, le_of_lt
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ min (min (δ / 2) r) (B (n + 1)) + δ / 2 ≤ δ / 2 + δ / 2

Tactic:
(add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)

Premises used: le_rfl, add_le_add, min_le_left, le_trans
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ δ / 2 + δ / 2 = δ

Tactic:
ENNReal.add_halves δ

Premises used: ENNReal.add_halves
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ closedEBall x δ

Tactic:
calc
        edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
        _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := add_le_add hz (le_of_lt xy)
        _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
        _ = δ := ENNReal.add_halves δ

Premises used: le_rfl, add_le_add, le_of_lt, HDiv.hDiv, min_le_left, HAdd.hAdd, ENNReal.add_halves, EDist.edist, OfNat.ofNat, Min.min, le_trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n

Tactic:
hr (calc
      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))

Premises used: Trans.trans, min_le_left, min_le_right, le_trans
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
z : X
hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))
⊢ z ∈ f n

Tactic:
exact hr (calc
      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))

Premises used: Trans.trans, min_le_left, min_le_right, le_trans