mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝

Tactic:
[

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦transAt i f g⟧ = ⟦transAt j f g⟧

Tactic:
[

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦transAt i f g⟧ = ⟦transAt j f g⟧
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
⊢ ⟦symmAt i f⟧ = ⟦symmAt j f⟧

Tactic:
[

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
⊢ ⟦symmAt i f⟧ = ⟦symmAt j f⟧
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
⊢ ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n

Tactic:
intro n x hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
⊢ ∃ y ∈ t0, edist x y ≤ 2 * B n
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ packingNumber ε A = 0 ↔ A = ∅

Tactic:
by
  simp only [packingNumber, ENat.iSup_eq_zero, encard_eq_zero]
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  by_contra!
  obtain ⟨x, hx⟩ := this
  simpa using h {x} (by simp [hx]) (by simp)

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ externalCoveringNumber δ A ≤ externalCoveringNumber ε A

Tactic:
[

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ externalCoveringNumber δ A ≤ externalCoveringNumber ε A
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ coveringNumber δ A ≤ coveringNumber ε A

Tactic:
[

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ coveringNumber δ A ≤ coveringNumber ε A
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖swap g a₀ i‖ ≤ ‖f a₀‖

Tactic:
[

Goal state after:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖swap g a₀ i‖ ≤ ‖f a₀‖
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ (↑C).Finite

Tactic:
refine Set.encard_lt_top_iff.mp ?_
    simp only [hC, iInf_lt_top, encard_lt_top_iff, Subtype.exists, exists_prop]
    exact ⟨C', ⟨hC'_subset, hC'_cover⟩, hC'_fin⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ ⨅ x, (↑x).encard = coveringNumber ε A

Tactic:
[

Goal state after:
case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ ⨅ x, (↑x).encard = coveringNumber ε A
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

Tactic:
[

Goal state after:
case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard

Tactic:
[

Goal state after:
case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (candidatesB X Y)

Tactic:
this

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    ((((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)})
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ∞
⊢ MemHolder r f

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ∞
⊢ MemHolder r f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hf : ∃ C, HolderOnWith C r f A
hs : s ≤ r
hA : Bornology.IsBounded A
⊢ ∃ C, HolderOnWith C s f A

Tactic:
[

Goal state after:
Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hf : ∃ C, HolderOnWith C r f A
hs : s ≤ r
hA : Bornology.IsBounded A
⊢ ∃ C, HolderOnWith C s f A
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hf : ∃ C, HolderOnWith C r f A
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
⊢ ∃ C, HolderOnWith C s f A

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hf : ∃ C, HolderOnWith C r f A
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
⊢ ∃ C, HolderOnWith C s f A
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s t : ℝ≥0
hf₁ : MemHolder r f
hf₂ : MemHolder t f
hrs : r ≤ s
hst : s ≤ t
⊢ MemHolder s f

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s t : ℝ≥0
hf₁ : MemHolder r f
hf₂ : MemHolder t f
hrs : r ≤ s
hst : s ≤ t
⊢ MemHolder s f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
⊢ min (edist x y) (edist y x) ≤ {x, y}.einfsep

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
x y : α
⊢ min (edist x y) (edist y x) ≤ {x, y}.einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⨅ d, uncurry edist ↑d

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⨅ d, uncurry edist ↑d
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ s.offDiag.toFinset.inf (uncurry edist)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ s.offDiag.toFinset.inf (uncurry edist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ ⋯.toFinset.inf (uncurry edist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Finset α
⊢ (↑s).einfsep = s.offDiag.inf (uncurry edist)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Finset α
⊢ (↑s).einfsep = s.offDiag.inf (uncurry edist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
[

Goal state after:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
[

Goal state after:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep ≤ (insert x s).einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.einfsep = min (min (edist x y) (edist x z)) (edist y z)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.einfsep = min (min (edist x y) (edist x z)) (edist y z)
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg.inl
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
h : eHolderNorm r f = ∞
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

pp: case neg.inr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
h : eHolderNorm r g = ∞
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
all_goals simp [h]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.infsep ≤ (min (edist x y) (edist y x)).toReal

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.infsep ≤ (min (edist x y) (edist y x)).toReal
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : ¬s.Nontrivial
⊢ d ≤ dist x y

Tactic:
rw [not_nontrivial_iff] at hs
    rw [hs.infsep_zero] at hd
    exact le_trans hd dist_nonneg

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : d ∈ uncurry dist '' s.offDiag
⊢ 0 ≤ d

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : d ∈ uncurry dist '' s.offDiag
⊢ 0 ≤ d
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⨅ d, uncurry dist ↑d

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⨅ d, uncurry dist ↑d
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)

Tactic:
have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
    nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
  rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with
    ⟨ι, c, r', hr', hsub', hfin⟩
  rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs
      (fun x _ => hfin.point_finite x) hsub' with
    ⟨r, hsub, hlt⟩
  exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⋯.toFinset.inf' ⋯ (uncurry dist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
H : (↑s).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

Tactic:
[

Goal state after:
case intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y

Tactic:
[

Goal state after:
case intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y