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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)
⊢ reorderRestrictProd S s (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i) = ↑x

Tactic:
ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)
x✝ : ι
⊢ reorderRestrictProd S s (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i) x✝ = ↑x x✝
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case h
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
x : Fin 3
h : x ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑x + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑x + ofDigits fun i ↦ a (i + 1)

Tactic:
fin_cases x

Goal state after:
case h.«0»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨0, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨0, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

case h.«1»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨1, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨1, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

case h.«2»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨2, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨2, ⋯⟩) + ofDigits fun i ↦ a (i + 1)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)
⊢ (fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) ((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) x) = x

Tactic:
ext

Goal state after:
ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)
x✝ : ι
⊢ ↑((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) ((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) x)) x✝ = ↑x x✝
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
⊢ (fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p) = p

Tactic:
ext

Goal state after:
case fst
ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑Sᶜ
⊢ ↑((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).1 x✝ = ↑p.1 x✝

case snd
ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑S
⊢ ((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).2 x✝ = p.2 x✝
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x) ↔
    ∃ x_1 ∈ s, S.domRestrict x_1 = x

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x) →
    ∃ x_1 ∈ s, S.domRestrict x_1 = x

case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ x_1 ∈ s, S.domRestrict x_1 = x) →
    ∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
⊢ { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (0, x✝) = (toLoop i p).toContinuousMap x✝

pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
ext

Goal state after:
case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ({ toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (0, x✝)) y✝ =
    ((toLoop i p).toContinuousMap x✝) y✝

case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
⊢ { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x✝) = (toLoop i q).toContinuousMap x✝

pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
ext

Goal state after:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ({ toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x✝)) y✝ =
    ((toLoop i q).toContinuousMap x✝) y✝

case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
rcases (mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
s : Set (List α)
hs : s ∈ traverse 𝓝 l
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: y : ℕ → Bool
⊢ (fun x ↦
        match (motive := ↑cantorSet → ℕ → Bool) x with
        | ⟨x, h⟩ => (cantorToBinary x).get)
      ((fun y ↦ ⟨ofDigits fun i ↦ bif y i then 2 else 0, ⋯⟩) y) =
    y

Tactic:
simp only [Fin.isValue]

Goal state after:
y : ℕ → Bool
⊢ (cantorToBinary (ofDigits fun i ↦ bif y i then 2 else 0)).get = y
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
⊢ {
        toFun := fun x_1 ↦
          { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                map_one_left := ⋯ }.toFun
            (t, x_1),
        continuous_toFun := ⋯ }
      y =
    (toLoop i p).toContinuousMap y

Tactic:
ext

Goal state after:
case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ ({
          toFun := fun x_1 ↦
            { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                  map_one_left := ⋯ }.toFun
              (t, x_1),
          continuous_toFun := ⋯ }
        y)
      y✝ =
    ((toLoop i p).toContinuousMap y) y✝
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)

Tactic:
constructor

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)

case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f
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
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
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
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
⊢ P = fun l ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset

Tactic:
ext

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
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
x✝ : ℕ
⊢ P x✝ ↔ t ∈ (logSizeBallSeq J hJ a c x✝).finset ∧ s ∈ (logSizeBallSeq J hJ a c x✝).finset
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

Tactic:
constructor

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)) → IsProperMap f
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
⊢ (d ⊔ d').IsUltra

Tactic:
constructor

Goal state after:
X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
⊢ ∀ (x y z : X), (d ⊔ d') x z ≤ (d ⊔ d') x y ⊔ (d ⊔ d') y z
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
⊢ (s.sup f).IsUltra

Tactic:
constructor

Goal state after:
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
⊢ ∀ (x y z : X), (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)
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)
⊢ transAt i (transAt j a b) (transAt j c d) = transAt j (transAt i a c) (transAt i b d)

Tactic:
ext

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✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
f : ↑(Ω^ N X x)
⊢ (fun y ↦ ⟨ContinuousMap.const (N → ↑I) y, ⋯⟩) ((fun f ↦ f 0) f) = f

Tactic:
ext

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.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ ↔
    (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

Tactic:
constructor

Goal state after:
case mp
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
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

case mpr
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
a₁ a₂ : ↑(Ω^ N X x)
⊢ (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂) →
    (Homotopic.setoid N x) a₁ a₂
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
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ ↔
    (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)

Tactic:
constructor

Goal state after:
case mp
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ →
    (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂)

case mpr
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Path.Homotopic.setoid { as := x }.as { as := x }.as) ((genLoopEquivOfUnique N) a₁) ((genLoopEquivOfUnique N) a₂) →
    (Homotopic.setoid N x) a₁ a₂
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)

Tactic:
refine Isometry.of_dist_eq fun a b => ?_
  refine (embeddingOfSubset_dist_le x a b).antisymm (le_of_forall_pos_le_add fun e epos => ?_)
  -- First step: find n with dist a (x n) < e
  rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with ⟨n, hn⟩
  -- Second step: use the norm control at index n to conclude
  have C : dist b (x n) - dist a (x n) = embeddingOfSubset x b n - embeddingOfSubset x a n := by
    simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
  have :=
    calc
      dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
      _ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
      _ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by grw [← le_abs_self]
      _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
        rw [C]
        gcongr
      _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
        gcongr
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n
      _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
  simpa [dist_comm] using this

Goal state after:
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)}
⊢ 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)}

Tactic:
ext

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)}
x✝ : Cb X Y
⊢ x✝ ∈ candidatesB X Y ↔
    x✝ ∈
      (((((⋂ 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.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ C ⊆ A ∧ IsSeparated (↑ε) C

Tactic:
constructor

Goal state after:
case left
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := ⋯
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ C ⊆ A

case right
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ y ∈ maximalSeparatedSet ε A, (x, y) ∉ {x | edist x.1 x.2 ≤ ↑ε}
C : Set X := ⋯
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ IsSeparated (↑ε) C
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 Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : ↑C → X
hg_mem : ∀ (x : ↑C), g x ∈ A
hg : ∀ (x : ↑C), f (g x) = ↑x
⊢ C = f '' range g

Tactic:
ext

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 Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : ↑C → X
hg_mem : ∀ (x : ↑C), g x ∈ A
hg : ∀ (x : ↑C), f (g x) = ↑x
x✝ : Y
⊢ x✝ ∈ C ↔ x✝ ∈ f '' range g