awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inst_2 : TopologicalSpace β
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ closedBall a r \ ball a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z

Tactic:
(isCompact_closedBall a r).exists_isLocalMin_mem_open ball_subset_closedBall hf hz hf1
    isOpen_ball

Premises used: Metric.ball_subset_closedBall, Metric.isOpen_ball, IsCompact.exists_isLocalMin_mem_open, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inst_2 : TopologicalSpace β
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ closedBall a r \ ball a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z

Tactic:
exact (isCompact_closedBall a r).exists_isLocalMin_mem_open ball_subset_closedBall hf hz hf1
    isOpen_ball

Premises used: Metric.ball_subset_closedBall, Metric.isOpen_ball, IsCompact.exists_isLocalMin_mem_open, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ Continuous (dist x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
⊢ ProperSpace α ↔ ∀ (x : α), IsProperMap (dist x)

Tactic:
⟨fun _ ↦ isProperMap_dist, fun H ↦ ⟨fun x r ↦ ?_⟩⟩

Premises used: isProperMap_dist, Iff.intro, ProperSpace.mk
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
refine : ∀ (H : ∀ (x : α), IsProperMap (dist x)) (x : α) (r : ℝ), IsCompact (closedBall x r)
⊢ ProperSpace α ↔ ∀ (x : α), IsProperMap (dist x)

Tactic:
refine ⟨fun _ ↦ isProperMap_dist, fun H ↦ ⟨fun x r ↦ ?_⟩⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
⊢ IsCompact (dist x ⁻¹' closedBall 0 r)

Tactic:
(H x).isCompact_preimage (isCompact_closedBall 0 r)

Premises used: IsProperMap.isCompact_preimage, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
h : closedBall x r = dist x ⁻¹' closedBall 0 r
⊢ IsCompact (closedBall x r)

Tactic:
convert! (H x).isCompact_preimage (isCompact_closedBall 0 r)

Premises used: IsProperMap.isCompact_preimage, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
h : ∀ (x_1 : α), x_1 ∈ closedBall x r ↔ x_1 ∈ dist x ⁻¹' closedBall 0 r
⊢ closedBall x r = dist x ⁻¹' closedBall 0 r

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
H : ∀ (x : α), IsProperMap (dist x)
x : α
r : ℝ
x_1 : α
⊢ x_1 ∈ closedBall x r ↔ x_1 ∈ dist x ⁻¹' closedBall 0 r

Tactic:
simp [dist_comm, Real.dist_eq]

Premises used: dist_comm, Real.dist_eq
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ IsClosedMap (dist x)

Tactic:
(isProperMap_dist x).isClosedMap

Premises used: IsProperMap.isClosedMap, isProperMap_dist
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ Continuous (nndist x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ Continuous NNReal.toReal

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ IsClosedMap (nndist x)

Tactic:
(isProperMap_nndist _).isClosedMap

Premises used: IsProperMap.isClosedMap, isProperMap_nndist
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Real
Goal:
⊢ SecondCountableTopology EReal

Tactic:
have : SeparableSpace EReal := ⟨⟨_, countable_range _, denseRange_ratCast⟩⟩
  .of_separableSpace_orderTopology _

Premises used: SecondCountableTopology.of_separableSpace_orderTopology, EReal, Rat.cast, Set.countable_range, And.intro, Exists.intro, Set.range, TopologicalSpace.SeparableSpace.mk, EReal.denseRange_ratCast, Real.toEReal
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Real
Goal:
⊢ SecondCountableTopology ℝ≥0

Tactic:
inferInstanceAs (SecondCountableTopology { x : ℝ | 0 ≤ x })

Premises used: _private.0.NNReal.instSecondCountableTopology._proof_1
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Real
Goal:
x : ℝ≥0
r : ℝ
⊢ IsClosedEmbedding toReal

Tactic:
have emb : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := Isometry.isClosedEmbedding fun _ ↦ congrFun rfl
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Real
Goal:
x : ℝ≥0
r : ℝ
emb : IsClosedEmbedding toReal
⊢ IsCompact (Metric.closedBall x r)

Tactic:
emb.isCompact_preimage (K := Metric.closedBall x r) (isCompact_closedBall _ _)

Premises used: Set.Mem, setOf, Set.preimage, Topology.IsClosedEmbedding.isCompact_preimage, ProperSpace.isCompact_closedBall, Metric.closedBall, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Real
Goal:
x : ℝ≥0
r : ℝ
emb : IsClosedEmbedding toReal
⊢ IsCompact (Metric.closedBall x r)

Tactic:
exact emb.isCompact_preimage (K := Metric.closedBall x r) (isCompact_closedBall _ _)

Premises used: Topology.IsClosedEmbedding.isCompact_preimage, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace.Real
Goal:
⊢ SecondCountableTopology ℝ≥0∞

Tactic:
orderIsoUnitIntervalBirational.toHomeomorph.isEmbedding.secondCountableTopology

Premises used: Topology.IsEmbedding.secondCountableTopology, ENNReal.orderIsoUnitIntervalBirational, Homeomorph.isEmbedding, OrderIso.toHomeomorph
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u_3
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
⊢ IsCompact (sphere x r)

Tactic:
(isCompact_closedBall x r).of_isClosed_subset isClosed_sphere sphere_subset_closedBall

Premises used: IsCompact.of_isClosed_subset, Metric.isClosed_sphere, ProperSpace.isCompact_closedBall, Metric.sphere_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
⊢ CompactSpace.{u_3} (↑(closedBall x r) : Type u_3)

Tactic:
isCompact_iff_compactSpace.mp (isCompact_closedBall _ _)

Premises used: isCompact_iff_compactSpace, Iff.mp, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
r : ℝ
⊢ CompactSpace.{u_3} (↑(sphere x r) : Type u_3)

Tactic:
isCompact_iff_compactSpace.mp (isCompact_sphere _ _)

Premises used: isCompact_iff_compactSpace, isCompact_sphere, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
suffices : SigmaCompactSpace α
⊢ SecondCountableTopology α

Tactic:
suffices SigmaCompactSpace α from EMetric.secondCountable_of_sigmaCompact α
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inl : ∀ (x : α), SigmaCompactSpace α
inr : ∀ (hn : ¬Nonempty α), SigmaCompactSpace α
⊢ SigmaCompactSpace α

Tactic:
rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn)

Premises used: em, Nonempty
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ SigmaCompactSpace α

Tactic:
⟨⟨fun n => closedBall x n, fun n => isCompact_closedBall _ _, iUnion_closedBall_nat _⟩⟩

Premises used: SigmaCompactSpace.mk, Nat.cast, And.intro, Exists.intro, ProperSpace.isCompact_closedBall, Metric.closedBall, Metric.iUnion_closedBall_nat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ SigmaCompactSpace α

Tactic:
exact ⟨⟨fun n => closedBall x n, fun n => isCompact_closedBall _ _, iUnion_closedBall_nat _⟩⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hn : ¬Nonempty α
⊢ SigmaCompactSpace α

Tactic:
⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, False.elim, SigmaCompactSpace.mk, Nonempty.intro, And.intro, Exists.intro, EmptyCollection.emptyCollection, isCompact_empty
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hn : ¬Nonempty α
⊢ SigmaCompactSpace α

Tactic:
exact ⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
inst : PseudoMetricSpace α
R : ℝ
h : ∀ (x : α) (r : ℝ), R ≤ r → IsCompact (closedBall x r)
⊢ ProperSpace α

Tactic:
⟨fun x r => IsCompact.of_isClosed_subset (h x (max r R) (le_max_right _ _)) isClosed_closedBall
    (closedBall_subset_closedBall <| le_max_left _ _)⟩

Premises used: le_max_right, Metric.isClosed_closedBall, IsCompact.of_isClosed_subset, Max.max, ProperSpace.mk, Metric.closedBall_subset_closedBall, le_max_left
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : CompactSpace α
⊢ ProperSpace α

Tactic:
⟨fun _ _ => isClosed_closedBall.isCompact⟩

Premises used: Metric.isClosed_closedBall, IsClosed.isCompact, ProperSpace.mk
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ LocallyCompactSpace α

Tactic:
.of_hasBasis (fun _ => nhds_basis_closedBall) fun _ _ _ =>
    isCompact_closedBall _ _

Premises used: LocallyCompactSpace.of_hasBasis, ProperSpace.isCompact_closedBall, Metric.nhds_basis_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
⊢ ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1

Tactic:
(Metric.cauchy_iff.1 hf).2 1 zero_lt_one

Premises used: zero_lt_one, And.right, Metric.cauchy_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
obtain : ∀ (t : Set α) (t_fset : t ∈ f) (ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1), ∃ (x : α), f ≤ nhds x
⊢ ∃ (x : α), f ≤ nhds x

Tactic:
obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 :=
      (Metric.cauchy_iff.1 hf).2 1 zero_lt_one

Premises used: zero_lt_one, And.right, Metric.cauchy_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
rcases : ∀ (x : α) (xt : x ∈ t), ∃ (x : α), f ≤ nhds x
⊢ ∃ (x : α), f ≤ nhds x

Tactic:
rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩

Premises used: And.left, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
⊢ closedBall x 1 ∈ f

Tactic:
have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
this : closedBall x 1 ∈ f
rcases : ∀ (y : α) (hy : f ≤ nhds y), ∃ (x : α), f ≤ nhds x
⊢ ∃ (x : α), f ≤ nhds x

Tactic:
rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf
        (le_principal_iff.2 this) with
      ⟨y, -, hy⟩

Premises used: Iff.mpr, Filter.le_principal_iff, isCompact_iff_totallyBounded_isComplete, And.right, Iff.mp, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
this : closedBall x 1 ∈ f
y : α
hy : f ≤ nhds y
⊢ ∃ (x : α), f ≤ nhds x

Tactic:
⟨y, hy⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
this : closedBall x 1 ∈ f
y : α
hy : f ≤ nhds y
⊢ ∃ (x : α), f ≤ nhds x

Tactic:
exact ⟨y, hy⟩
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
⊢ SecondCountableTopology ℝ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
β : Type u_4
inst_1 : PseudoMetricSpace α
inst_2 : PseudoMetricSpace β
inst_3 : ProperSpace α
inst_4 : ProperSpace β
x : α
y : β
r : ℝ
rw : IsCompact (closedBall x r ×ˢ closedBall y r)
⊢ IsCompact (closedBall (x, y) r)

Tactic:
rw [← closedBall_prod_same x y]

Premises used: closedBall_prod_same
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
β : Type u_4
inst_1 : PseudoMetricSpace α
inst_2 : PseudoMetricSpace β
inst_3 : ProperSpace α
inst_4 : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall x r ×ˢ closedBall y r)

Tactic:
(isCompact_closedBall x r).prod (isCompact_closedBall y r)

Premises used: IsCompact.prod, setOf, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α_1 : Type u
β_1 : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
β : Type u_4
inst_1 : PseudoMetricSpace α
inst_2 : PseudoMetricSpace β
inst_3 : ProperSpace α
inst_4 : ProperSpace β
x : α
y : β
r : ℝ
⊢ IsCompact (closedBall x r ×ˢ closedBall y r)

Tactic:
exact (isCompact_closedBall x r).prod (isCompact_closedBall y r)

Premises used: IsCompact.prod, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
⊢ ProperSpace ((b : β) → X b)

Tactic:
.of_isCompact_closedBall_of_le 0 fun x r hr => ?_

Premises used: OfNat.ofNat, ProperSpace.of_isCompact_closedBall_of_le
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
refine : ∀ (x : (b : β) → X b) (r : ℝ) (hr : 0 ≤ r), IsCompact (closedBall x r)
⊢ ProperSpace ((b : β) → X b)

Tactic:
refine .of_isCompact_closedBall_of_le 0 fun x r hr => ?_
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
rw : IsCompact (X := (b : β) → X b) (Set.pi (α := X) univ fun (b : β) ↦ closedBall (x b) r)
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_pi _ hr]

Premises used: closedBall_pi
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (X := (b : β) → X b) (Set.pi (α := X) univ fun (b : β) ↦ closedBall (x b) r)

Tactic:
isCompact_univ_pi fun _ => isCompact_closedBall _ _

Premises used: isCompact_univ_pi, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace.{u_3} (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (X := (b : β) → X b) (Set.pi (α := X) univ fun (b : β) ↦ closedBall (x b) r)

Tactic:
exact isCompact_univ_pi fun _ => isCompact_closedBall _ _

Premises used: isCompact_univ_pi, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.ProperSpace
Goal:
X : Type u_3
inst : PseudoMetricSpace X
inst_1 : ProperSpace X
s : Set X
hs : IsClosed s
⊢ ProperSpace.{u_3} (↑s : Type u_3)

Tactic:
⟨fun x r ↦ Topology.IsEmbedding.subtypeVal.isCompact_iff.mpr
    ((isCompact_closedBall x.1 r).of_isClosed_subset
    (hs.isClosedMap_subtype_val _ isClosed_closedBall) (Set.image_subset_iff.mpr subset_rfl))⟩

Premises used: Iff.mpr, Metric.isClosed_closedBall, Topology.IsEmbedding.isCompact_iff, IsCompact.of_isClosed_subset, IsClosed.isClosedMap_subtype_val, ProperSpace.mk, Set.image_subset_iff, ProperSpace.isCompact_closedBall, Metric.closedBall, Topology.IsEmbedding.subtypeVal, Subtype.val, subset_rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
base : dist (f m) (f m) ≤ ∑ i ∈ ∅, dist (f i) (f (i + 1))
base₁ : dist (f m) (f m) ≤ 0
base₂ base₃ : LE.le (α := ℝ) 0 0
⊢ dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))

Tactic:
rw [Finset.Ico_self, Finset.sum_empty, dist_self]

Premises used: Finset.Ico_self, dist_self, Finset.sum_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1))

Tactic:
dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f m) (f n) + dist (f n) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1))

Tactic:
add_le_add ihn le_rfl

Premises used: le_rfl, add_le_add
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
rw : n ∉ Finset.Ico m n
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]

Premises used: add_comm, Finset.insert_Ico_right_eq_Ico_add_one, Finset.sum_insert
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n_1 n : ℕ
hle : m ≤ n
ihn : Dist.dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, Dist.dist (f i) (f (i + 1))
dist :
  ∑ i ∈ Finset.Ico m n, Dist.dist (f i) (f (i + 1)) + Dist.dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), Dist.dist (f i) (f (i + 1))
⊢ Dist.dist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), Dist.dist (f i) (f (i + 1))

Tactic:
calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

Premises used: dist_triangle, le_rfl, add_le_add, Finset.Ico, HAdd.hAdd, Dist.dist, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
base : dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))
succ :
  ∀ (n : ℕ) (hle : m ≤ n) (ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))),
    dist (f m) (f (n + 1)) ≤ ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))
⊢ dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))

Tactic:
induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
  | succ n hle ihn =>
    calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

Premises used: dist_triangle, Finset.Ico_self, Finset.Ico, dist_self, HAdd.hAdd, Finset.sum_empty, Dist.dist, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
n : ℕ
⊢ dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, dist (f i) (f (i + 1))

Tactic:
Nat.Ico_zero_eq_range n ▸ dist_le_Ico_sum_dist f (Nat.zero_le n)

Premises used: Nat.zero_le, Eq.rec, Nat.Ico_zero_eq_range, dist_le_Ico_sum_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
hmn : m ≤ n
d : ℕ → ℝ
hd : ∀ {k : ℕ}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k
⊢ dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i

Tactic:
le_trans (dist_le_Ico_sum_dist f hmn) <|
    Finset.sum_le_sum fun _k hk => hd (Finset.mem_Ico.1 hk).1 (Finset.mem_Ico.1 hk).2

Premises used: And.right, And.left, Iff.mp, Finset.sum_le_sum, dist_le_Ico_sum_dist, Finset.mem_Ico, le_trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
n : ℕ
d : ℕ → ℝ
hd : ∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k
⊢ dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i

Tactic:
Nat.Ico_zero_eq_range n ▸ dist_le_Ico_sum_of_dist_le zero_le fun _ => hd

Premises used: zero_le, Eq.rec, Nat.Ico_zero_eq_range, dist_le_Ico_sum_of_dist_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ),
      0 < i' → ∃ (i : ℝ), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | dist p.1 p.2 < i} ⊆ {p : α × α | dist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod.map_apply, mem_setOf]

Premises used: Set.subset_def, Set.mem_setOf, Set.preimage_setOf_eq, gt_iff_lt, Prod.map_apply, Prod.forall