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

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∃ n, s n = ∅
⊢ ∃ n, dissipate s n = ∅

pp: case neg
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ n, dissipate s n = ∅

Tactic:
· use g.choose
    rw [← subset_empty_iff] at hd ⊢
    exact (dissipate_subset le_rfl).trans g.choose_spec.le

Goal state after:
case neg
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ n, dissipate s n = ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty

Tactic:
simp_rw [IsCompactSystem.iff_nonempty_iInter]
  refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_biInter_lt ▸ (h' (n + 1))),
    fun h C hi h' ↦ h C hi ?_⟩
  simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢
  refine fun n g ↦ h' n ?_
  simp_rw [← subset_empty_iff, dissipate] at g ⊢
  exact le_trans (fun x ↦ by simp; grind) g

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.IsChain (fun x1 x2 ↦ x1 > x2) ↑↑l
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
rw [max_eq_o_cons_tail C hsC ho l, List.isChain_iff_pairwise] at this

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this✝ : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
this : List.Pairwise (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑(↑l).Tail)
⊢ (↑(↑l).Tail).head! < term I ho
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ compactOpen = generateFrom (image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T})

Tactic:
by
  apply le_antisymm
  · apply_rules [generateFrom_anti, image2_subset_iff.mpr]
    intro K hK t ht
    exact mem_image2_of_mem (hS₁ K hK) (isOpen_sUnion fun _ h ↦ hT.isOpen <| ht.2 h)
  · refine le_of_nhds_le_nhds fun f ↦ ?_
    simp only [nhds_compactOpen, le_iInf_iff, le_principal_iff]
    intro K (hK : IsCompact K) U (hU : IsOpen U) hfKU
    simp only [TopologicalSpace.nhds_generateFrom]
    obtain ⟨t, htT, htf, hTU, hKT⟩ : ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ f '' K ⊆ ⋃₀ t := by
      rw [hT.open_eq_sUnion' hU, mapsTo_iff_image_subset, sUnion_eq_biUnion] at hfKU
      obtain ⟨t, ht, hfin, htK⟩ :=
        (hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU
      refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
      rwa [sUnion_eq_biUnion]
    rw [image_subset_iff] at hKT
    obtain ⟨s, hsS, hsf, hKs, hst⟩ : ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo f (⋃₀ s) (⋃₀ t) := by
      have : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo f L (⋃₀ t) := by
        intro x hx
        rcases hKT hx with ⟨V, hVt, hxV⟩
        rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
        exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
      choose! L hLS hLmem hLt using this
      rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩
      refine ⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _,
        by rwa [sUnion_image], ?_⟩
      rw [mapsTo_sUnion, forall_mem_image]
      exact fun x hx ↦ hLt x <| hsK x hx
    have hsub : (⋂ L ∈ s, {g : C(X, Y) | MapsTo g L (⋃₀ t)}) ⊆ {g | MapsTo g K U} := by
      simp only [← ofPred_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]
      exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)
    refine mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub
    refine mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_principal_self _
    exact ⟨hst.mono_left (subset_sUnion_of_mem hL), mem_image2_of_mem (hsS hL) ⟨htf, htT⟩⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ 𝓝 ↑x

Tactic:
rw [← map_nhds_subtype_coe_eq_nhds x.2]

Goal state after:
case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ map Subtype.val (𝓝 ⟨↑x, ⋯⟩)

case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ ∀ᶠ (x : X) in 𝓝 ↑x, x ∈ ↑U
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ 𝓝 ⊤ = ⊤

Tactic:
simp [nhds_eq]

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ᶠ (y : X) in 𝓝 x, P y ↑g

Tactic:
apply ((hf hx).and <| (eventually_nhdsSet_iff_forall.mp h x hx).eventually_nhds).mono

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] V

Tactic:
obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ U ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' V)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ 1 ≤ logSizeRadius t V a c

Tactic:
rw [logSizeRadius, dif_pos ha]

Goal state after:
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ 1 ≤ Nat.find ⋯
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ ↑(#({x ∈ V | edist t x ≤ ↑(logSizeRadius t V a c) * c})) ≤ a ^ logSizeRadius t V a c

Tactic:
rw [logSizeRadius, dif_pos ha]

Goal state after:
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ ↑(#({x ∈ V | edist t x ≤ ↑(Nat.find ⋯) * c})) ≤ a ^ Nat.find ⋯
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c i).finset = 0

Tactic:
← not_ne_iff,

Goal state after:
case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬#(logSizeBallSeq J hJ a c i).finset ≠ 0
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
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset = 0

Tactic:
← Nat.le_zero,

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ 0
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1) ∧ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
n : ℕ
ih : 0 ∈ preCantorSet n
⊢ 0 ∈ preCantorSet (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed (preCantorSet (n + 1))

Tactic:
| succ n ih =>

Goal state after:
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
h : ∀ (n : ℕ), a n ≠ 1
⊢ (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i ∧ (ofDigits fun i ↦ a (i + 1)) / 3 = ofDigits a ∨
    (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i ∧ (2 + ofDigits fun i ↦ a (i + 1)) / 3 = ofDigits a

Tactic:
have : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i := ih (by solve_by_elim)

Goal state after:
case h
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
⊢ (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i ∧ (ofDigits fun i ↦ a (i + 1)) / 3 = ofDigits a ∨
    (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i ∧ (2 + ofDigits fun i ↦ a (i + 1)) / 3 = ofDigits a
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: 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

Tactic:
rintro ⟨y, _, z, hz_mem, _, hzx⟩

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
y : (a : ↑Sᶜ) → α ↑a
left✝¹ : ∃ x ∈ s, Sᶜ.domRestrict x = y
z : (a : ι) → α a
hz_mem : z ∈ s
left✝ : (∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict z) ∧ Sᶜ.domRestrict z = y
hzx : (fun i ↦ z ↑i) = x
⊢ ∃ x_1 ∈ s, S.domRestrict x_1 = x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x

Tactic:
by
    rw [cantorSet_eq_union_halves] at hx
    grind

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
x : ℝ
hx : x ∈ cantorSet
n : ℕ
ih : (cantorSequence x).get n ∈ cantorSet
⊢ (cantorSequence x).get (n + 1) ∈ cantorSet

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
S : Set ι
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), CompactSpace (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this : S.domRestrict = Prod.fst ∘ ⇑(Homeomorph.piEquivPiSubtypeProd (fun x ↦ x ∈ S) α)
⊢ IsClosed (Prod.fst '' ⇑(Homeomorph.piEquivPiSubtypeProd (fun x ↦ x ∈ S) α) '' s)

Tactic:
exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
x : ℝ
n : ℕ
ih : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
⊢ (cantorSequence x).get (n + 1) =
    (x - ∑ i ∈ Finset.range (n + 1), ofDigitsTerm (cantorToTernary x).get i) * 3 ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
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
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ #(logSizeBallSeq J hJ a c (l + 1)).finset = 0

Tactic:
← Nat.le_zero,

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 := 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
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ #(logSizeBallSeq J hJ a c (l + 1)).finset ≤ 0
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 : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
⊢ {
        toFun := fun x_1 ↦
          { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun (t, x_1),
        continuous_toFun := ⋯ }
      y =
    ↑p y

Tactic:
erw [homotopyFrom_apply]

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 : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (t, y)) =
    ↑p 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:
intro a₁ a₂
      constructor <;> rintro ⟨H⟩
      exacts
        [⟨{ toFun := fun t ↦ H ⟨t, isEmptyElim⟩
            source' := (H.apply_zero _).trans (congr_arg a₁ <| Subsingleton.elim _ _)
            target' := (H.apply_one _).trans (congr_arg a₂ <| Subsingleton.elim _ _) }⟩,
        ⟨{  toFun := fun t0 ↦ H t0.fst
            map_zero_left := fun _ ↦ H.source.trans (congr_arg a₁ <| Subsingleton.elim _ _)
            map_one_left := fun _ ↦ H.target.trans (congr_arg a₂ <| Subsingleton.elim _ _)
            prop' := fun _ _ ⟨i, _⟩ ↦ isEmptyElim i }⟩]

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: 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)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ (Homotopic.setoid N x) a₁ a₂

Tactic:
refine
      ⟨⟨⟨⟨fun tx ↦ H (tx.fst, tx.snd default), H.continuous.comp ?_⟩, fun y ↦ ?_, fun y ↦ ?_⟩, ?_⟩⟩

Goal state after:
case mpr.refine_1
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)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ Continuous fun tx ↦ (tx.1, tx.2 default)

case mpr.refine_2
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)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
y : N → ↑I
⊢ { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯ }.toFun (0, y) = ↑a₁ y

case mpr.refine_3
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)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
y : N → ↑I
⊢ { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯ }.toFun (1, y) = ↑a₂ y

case mpr.refine_4
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)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 ↦
              { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑a₁ x_1
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ uniformity (Set α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | hausdorffEDist p.1 p.2 < ε}

Tactic:
refine le_antisymm
      (le_iInf₂ fun ε hε => Filter.le_principal_iff.mpr ?_)
      (uniformity_basis_edist.lift' monotone_hausdorffEntourage |>.ge_iff.mpr fun ε hε =>
        Filter.mem_iInf_of_mem ε <| Filter.mem_iInf_of_mem hε fun _ =>
        mem_hausdorffEntourage_of_hausdorffEDist_lt)

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | hausdorffEDist p.1 p.2 < ε} ∈ uniformity (Set α)
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 : A = ∅
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
← externalCoveringNumber_eq_zero (ε := ε)

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.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : Compacts α
h : edist s t = 0
⊢ ↑s = ↑t

Tactic:
have : closure (s : Set α) = closure t := hausdorffEDist_zero_iff_closure_eq_closure.1 h
    rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
⊢ ↑s = ↑t

Tactic:
have : closure (s : Set α) = closure t := hausdorffEDist_zero_iff_closure_eq_closure.1 h
    rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

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

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

Tactic:
← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top,

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

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite
us : s ⊆ ⋃ i, ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i < r i
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
exact ⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ (ediam (⇑ofSnowflaking ⁻¹' s) ^ α⁻¹) ^ α = ediam s ^ α

Tactic:
← ediam_preimage_toSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ ediam (⇑toSnowflaking ⁻¹' ⇑ofSnowflaking ⁻¹' s) ^ α = ediam s ^ α