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

Goal state before:
pp: case neg.e_6
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
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Tactic:
;

Goal state after:
case neg.e_6
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
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i
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✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
f : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ ((fun y ↦ ⟨ContinuousMap.const (N → ↑I) y, ⋯⟩) ((fun f ↦ f 0) f)) y✝ = f y✝

Tactic:
;

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
f : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ ((fun y ↦ ⟨ContinuousMap.const (N → ↑I) y, ⋯⟩) ((fun f ↦ f 0) f)) y✝ = f 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✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
y : N → ↑I
⊢ ((fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩)
        ((fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) p))
      y =
    p y

Tactic:
;

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
y : N → ↑I
⊢ ((fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩)
        ((fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) p))
      y =
    p y
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) i) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t))

Tactic:
;

Goal state after:
case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) i) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) default) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t))

Tactic:
;

Goal state after:
case refine_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default))) default) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) i) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1))

Tactic:
;

Goal state after:
case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) i) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1))
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x ↑t ≤ infEDist y ↑t + edist x y

Tactic:
;

Goal state after:
case h₁
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x ↑t ≤ infEDist y ↑t + edist x y
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) default) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1))

Tactic:
;

Goal state after:
case refine_2
X : Type u_2
inst✝² : TopologicalSpace X
x : X
N : Type u_3
inst✝¹ : DecidableEq N
inst✝ : Unique N
p q : ↑(Ω^ N X x)
t : ↑I
x✝ : ¬↑t ≤ 2⁻¹
i : N
⊢ ↑(Function.update (fun x ↦ t) default (Set.projIcc 0 1 transAt._proof_3 (2 * ↑((fun x ↦ t) default) - 1)) default) =
    ↑(Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑t - 1))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i = j
⊢ auxGroup i = auxGroup j

pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j

Tactic:
;

Goal state after:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i = j
⊢ auxGroup i = auxGroup j

case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j
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)
⊢ ⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧

Tactic:
let inv := fun (G) (_ : Group G) ↦ ((·⁻¹) : G → G)

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)
inv : (G : Type ?u.31) → Group G → G → G := fun G x x_1 ↦ x_1⁻¹
⊢ ⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧
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
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ (genLoopEquivOfUnique (Fin 1)) (transAt 0 q p) ≈
    ((genLoopEquivOfUnique (Fin 1)) q).trans ((genLoopEquivOfUnique (Fin 1)) p)

Tactic:
rw [Unique.eq_default 0, genLoopEquivOfUnique_transAt]

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

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ 1 ≤ ↑(maxVar X Y)

Tactic:
;

Goal state after:
case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ 1 ≤ ↑(maxVar X Y)
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Tactic:
;

Goal state after:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ 1 ≤ dist (inl x) (inr y)

Tactic:
;

Goal state after:
case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ 1 ≤ dist (inl x) (inr y)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ 1 ≤ dist (inl x) (inr y)

Tactic:
;

Goal state after:
case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ 1 ≤ dist (inl x) (inr y)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ ↑(maxVar X Y)

Tactic:
;

Goal state after:
case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ ↑(maxVar X Y)
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x ↦ 0

Tactic:
;

Goal state after:
case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x ↦ 0
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x ↦ 0) x) ((fun x ↦ 0) x2) = edist x x2

Tactic:
;

Goal state after:
case h
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x ↦ 0) x) ((fun x ↦ 0) x2) = edist x x2
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ ⨅ (_ : IsCover ε A C), (f '' C).encard ≤ C.encard

Tactic:
refine (iInf_le _ hC_cover).trans ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ (f '' C).encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ ⨅ (_ : IsCover ε A C'), C'.encard ≤ (f '' C').encard

Tactic:
refine (iInf_le _ hC_cover).trans ?_

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ C'.encard ≤ (f '' C').encard
Module: Mathlib.Topology.MetricSpace.Infsep

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {y, x}.einfsep ≤ edist y x
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Tactic:
rw [← ENNReal.div_le_iff h₁ h₂]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C
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.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ (↑(range Ψ) ≃ᵢ ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))

Tactic:
;

Goal state after:
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ (↑(range Ψ) ≃ᵢ ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ (↑↑p ≃ᵢ ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))

Tactic:
;

Goal state after:
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ (↑↑p ≃ᵢ ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))

Tactic:
;

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
⊢ (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) =
    (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ })

Tactic:
;

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
⊢ (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) =
    (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ })
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ ⇑ofSnowflaking ⁻¹' closedEBall x r = closedEBall (toSnowflaking x) (r ^ α)

Tactic:
by
  ext ⟨y⟩
  simp (disch := positivity) [ENNReal.rpow_le_rpow_iff]

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ 0 ≤ dist x y

Tactic:
;

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ 0 ≤ dist x y
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ 0 ≤ dist (toSnowflaking x✝) y

Tactic:
;

Goal state after:
case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ 0 ≤ dist (toSnowflaking x✝) y
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist (toSnowflaking x✝¹) (toSnowflaking x✝)

Tactic:
;

Goal state after:
case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist (toSnowflaking x✝¹) (toSnowflaking x✝)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist x✝¹ x✝ ^ α

Tactic:
;

Goal state after:
case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist x✝¹ x✝ ^ α
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y = ENNReal.ofReal (dist x y)

Tactic:
;

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y = ENNReal.ofReal (dist x y)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ edist (toSnowflaking x✝) y = ENNReal.ofReal (dist (toSnowflaking x✝) y)

Tactic:
;

Goal state after:
case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ edist (toSnowflaking x✝) y = ENNReal.ofReal (dist (toSnowflaking x✝) y)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ dist (ofSnowflaking (toSnowflaking x✝)) (ofSnowflaking y) = dist (toSnowflaking x✝) y ^ α⁻¹

Tactic:
;

Goal state after:
case toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
y : Snowflaking X α hα₀ hα₁
x✝ : X
⊢ dist (ofSnowflaking (toSnowflaking x✝)) (ofSnowflaking y) = dist (toSnowflaking x✝) y ^ α⁻¹
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h : Inhabited X
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
;

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h : Inhabited X
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ ∃ s, s.Infinite ∧ DiscreteTopology ↑s

Tactic:
refine ⟨range f, infinite_range_of_injective hf.injective, ?_⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ DiscreteTopology ↑(range f)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIciTopology α
a : WithLower α
⊢ IsOpen[inst✝¹] (⇑toLower ⁻¹' (Ici a)ᶜ)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIciTopology α
a : WithLower α
⊢ IsOpen[inst✝¹] (⇑toLower ⁻¹' (Ici a)ᶜ)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : Set αᵒᵈ
⊢ IsOpen[OrderDual.instTopologicalSpace] x✝ ↔ IsOpen[lowerSet αᵒᵈ] x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : Set αᵒᵈ
⊢ IsOpen[OrderDual.instTopologicalSpace] x✝ ↔ IsOpen[lowerSet αᵒᵈ] x✝
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen[inst✝¹] (⇑toUpper ⁻¹' (Iic a)ᶜ)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen[inst✝¹] (⇑toUpper ⁻¹' (Iic a)ᶜ)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsOpen[lower α] s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsOpen[lower α] s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case basic
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ

Tactic:
;

Goal state after:
case basic
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : α
⊢ x✝ ∈ nhdsKer s ↔ x✝ ∈ ↑(upperClosure s)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : α
⊢ x✝ ∈ nhdsKer s ↔ x✝ ∈ ↑(upperClosure s)