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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x ↦ ↑(insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨(↑⟨l, hl⟩).insertIdx (↑i) a, ⋯⟩)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x ↦ ↑(insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨(↑⟨l, hl⟩).insertIdx (↑i) a, ⋯⟩)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case e_a
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑(logSizeBallSeq J hJ a c l).radius = ↑(logSizeBallSeq J hJ a c l).radius

pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ ↑(logSizeBallSeq J hJ a c l).radius

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ 1 ≤ ↑(logSizeBallSeq J hJ a c l).radius
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x ↦ ↑(eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑⟨l.eraseIdx ↑i, ⋯⟩)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x ↦ ↑(eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑⟨l.eraseIdx ↑i, ⋯⟩)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑1 ≤ ↑(logSizeBallSeq J hJ a c l).radius

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ ↑1 ≤ ↑(logSizeBallSeq J hJ a c l).radius
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 < δ}
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 < δ} (s, t).1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 < δ} (s, t).1
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 ≤ δ} (s, t).1
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 ≤ δ} (s, t).1
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f (logSizeBallSeq J hJ a c l).point) (f ↑⟨s, hs⟩) +
      edist (f (logSizeBallSeq J hJ a c l).point) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤
    (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
sup_bound : ∀ {x y : T}, (x, y) ∈ pairSetSeq J a c l → edist (f x) (f y) ≤ ⨆ p, edist (f (↑p).1) (f (↑p).2)
⊢ edist (f (logSizeBallSeq J hJ a c l).point) (f ↑⟨s, hs⟩) +
      edist (f (logSizeBallSeq J hJ a c l).point) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤
    (⨆ p, edist (f (↑p).1) (f (↑p).2)) + ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ #J = 1

Tactic:
]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ #J = 1
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s✝ t✝ : Set α
δ : ℝ≥0∞
h✝ :
  (s✝, t✝).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s✝, t✝).2 ∧
    (s✝, t✝).2 ⊆ SetRel.image {x | edist x.2 x.1 ≤ δ} (s✝, t✝).1
s t : Set α
h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t
⊢ ∀ i ∈ s, infEDist i t ≤ δ

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s✝ t✝ : Set α
δ : ℝ≥0∞
h✝ :
  (s✝, t✝).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s✝, t✝).2 ∧
    (s✝, t✝).2 ⊆ SetRel.image {x | edist x.2 x.1 ≤ δ} (s✝, t✝).1
s t : Set α
h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t
⊢ ∀ i ∈ s, infEDist i t ≤ δ
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ Nonempty ↥J

Tactic:
]

Goal state after:
case refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ Nonempty ↥J
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)) 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.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t) = infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + 2 * edist (x, s) (y, t) = infEDist y ↑t + 2 * edist (x, s) (y, t)

Tactic:
]

Goal state after:
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 j = auxGroup j

Tactic:
]

Goal state after:
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
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧

Tactic:
]

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < coveringNumber ε A ↔ ¬A.Nonempty

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < coveringNumber ε A ↔ ¬A.Nonempty
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
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧

Tactic:
]

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦fromLoop (Classical.arbitrary N) (Path.symm (toLoop (Classical.arbitrary N) p))⟧
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ = diam univ

Tactic:
]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < packingNumber ε A ↔ ¬A.Nonempty

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < packingNumber ε A ↔ ¬A.Nonempty
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ packingNumber ε A ≤ A.encard

Tactic:
simp only [packingNumber, iSup_le_iff]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ i ⊆ A, IsSeparated (↑ε) i → i.encard ≤ A.encard
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ + dist (inl default) (inr default) + diam univ =
    diam univ + (dist default default + 1 + dist default default) + diam univ

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
x y : X ⊕ Y
inst✝³ : CompactSpace X
inst✝² : Nonempty X
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ diam univ + dist (inl default) (inr default) + diam univ =
    diam univ + (dist default default + 1 + dist default default) + diam univ
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 : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ hausdorffEDist ↑(s (n + l)) ↑(s (n + l + 1)) < 2⁻¹ ^ (n + l)

Tactic:
]

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
l : ℕ
z : ↥(s (n + l))
⊢ hausdorffEDist ↑(s (n + l)) ↑(s (n + l + 1)) < 2⁻¹ ^ (n + l)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A C : Set E
hC₁ : A ⊆ C
⊢ A.encard ≤ C.encard

Tactic:
]

Goal state after:
E : Type u_3
inst✝ : EMetricSpace E
A C : Set E
hC₁ : A ⊆ C
⊢ A.encard ≤ C.encard
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)
⊢ Path.trans ((genLoopEquivOfUnique (Fin 1)) q) ((genLoopEquivOfUnique (Fin 1)) p) ≈
    ((genLoopEquivOfUnique (Fin 1)) q).trans ((genLoopEquivOfUnique (Fin 1)) p)

Tactic:
]

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

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A ≤ coveringNumber 0 A

Tactic:
]

Goal state after:
E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A ≤ coveringNumber 0 A
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist x y = Sum.dist (inl x) (inl y)

Tactic:
]

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

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

Tactic:
by ring

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

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b

Tactic:
]

Goal state after:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b
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
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Tactic:
]

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

Goal state before:
pp: case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_eq_empty : externalCoveringNumber ε A = 0
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
]

Goal state after:
case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_eq_empty : externalCoveringNumber ε A = 0
⊢ externalCoveringNumber ε A ≤ 1
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
⊢ 2 * dist a (x n) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) 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
⊢ 2 * dist a (x n) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n|
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = Sum.dist (inr x) (inr y)

Tactic:
]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = Sum.dist (inr x) (inr y)