mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : ProfiniteGrp.{?u.22}
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ ProfiniteGrp.{?u.22} GrpCat).obj Y✝
⊢ (homEquiv X'✝ Y✝).symm (f ≫ g) = profiniteCompletion.map f ≫ (homEquiv X✝ Y✝).symm g

Tactic:
apply lift_unique

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : ProfiniteGrp.{?u.22}
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ ProfiniteGrp.{?u.22} GrpCat).obj Y✝
⊢ eta X'✝ ≫ (forget₂ ProfiniteGrp.{?u.22} GrpCat).map ((homEquiv X'✝ Y✝).symm (f ≫ g)) =
    eta X'✝ ≫ (forget₂ ProfiniteGrp.{?u.22} GrpCat).map (profiniteCompletion.map f ≫ (homEquiv X✝ Y✝).symm g)
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
x✝ : A
a✝ : x✝ ∈ Set.univ
⊢ |(↑(1 x✝)).arg| < π / 2

Tactic:
simp [pi_pos]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (map C h) (↑a (op K)) ∈ {↑a (op J)}

Tactic:
← a.prop (homOfLE h).op

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (map C h) (↑a (op K)) ∈
    {(ConcreteCategory.hom (((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).map (homOfLE h).op)) (↑a (op K))}
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
j : cell C 0
⊢ cellFrontier 0 j = ∅

Tactic:
simp [cellFrontier, sphere_eq_empty_of_subsingleton]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
⊢ ⋃ n, ⋃ j, openCell n j = C

Tactic:
by
  simpa using RelCWComplex.union_iUnion_openCell_eq_complex (C := C)

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

Goal state before:
pp: 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
⊢ eval C ∘ (sum_equiv C hsC ho).toFun = Sum.elim (fun l ↦ Products.eval C ↑l) fun l ↦ Products.eval C ↑l

Tactic:
by
  ext ⟨_, _⟩ <;> [rfl; rfl]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case neg
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
· left
      simp_rw [← union, disjoint_union_left, disjoint_iUnion_left]
      exact ⟨disjointBase n j |>.symm, fun _ _ ↦ disjoint_openCell_of_ne (by aesop)⟩

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this✝ : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
this : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)
hV : finrank ℝ V = finrank ℝ ↥(ℝ ∙ v)ᗮ
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)

Tactic:
letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this✝ : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
this : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)
hV : finrank ℝ V = finrank ℝ ↥(ℝ ∙ v)ᗮ
e : V ≃ₜ ↥(ℝ ∙ v)ᗮ := ↑⋯.some
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ Finite (ConnectedComponents X)

Tactic:
refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ ∀ (i : ConnectedComponents Y), IsClopen (f ⁻¹' mk ⁻¹' {i})

case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ Pairwise (Disjoint on fun y ↦ f ⁻¹' mk ⁻¹' {y})

case refine_3
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ ⋃ i, f ⁻¹' mk ⁻¹' {i} = Set.univ
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ (w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.finsuppSum_mem
    intro q _
    rw [map_smul]
    apply Submodule.smul_mem
    apply Submodule.subset_span
    dsimp only [eval]
    rw [Products.eval_πs C (Products.prop_of_isGood _ _ q.prop)]
    refine ⟨q.val, ⟨?_, rfl⟩⟩
    simp only [Products.lt_iff_lex_lt, Set.mem_ofPred_eq]
    exact good_lt_maxProducts C hsC ho q l

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

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace

Tactic:
le_iInf_iff

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x ↦ x ∈ i) sierpinskiSpace
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α →CO β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y : X
ι : Type u_3
inst✝ : StronglyLocallyContractibleSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
refine contractible_basis x |>.to_hasBasis'
      (fun s ⟨hs, hs'⟩ ↦ ⟨s, ⟨hs, ?_⟩, le_rfl⟩) (fun s hs ↦ hs.1)
    rw [isPathConnected_iff_pathConnectedSpace]
    infer_instance

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
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊂ (logSizeBallSeq J hJ a c i).finset

Tactic:
apply ssubset_of_subset_not_subset

Goal state after:
case hab
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

case hba
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: a✝ : (𝓝 ∞).IsCountablyGenerated
this : (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated
⊢ False

Tactic:
OnePoint.comap_coe_nhds_infty,

Goal state after:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (coclosedCompact ℚ).IsCountablyGenerated
⊢ False
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos.hs
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ {(logSizeBallSeq J ⋯ a c i).point} ⊆ J

pp: case pos.ht
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ (logSizeBallSeq J ⋯ a c i).ball c ⊆ J

Tactic:
· exact Finset.singleton_subset_iff.mpr (point_mem_logSizeBallSeq_init hJ _)

Goal state after:
case pos.ht
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ (logSizeBallSeq J ⋯ a c i).ball c ⊆ J
Module: Mathlib.Topology.Instances.CantorSet

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

Tactic:
· simpa [g, f, div_eq_inv_mul] using g.isClosedEmbedding.isClosed_iff_image_isClosed.mp ih

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

Goal state before:
pp: y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y

Tactic:
apply ofDigits_zero_two_sequence_unique at this

Goal state after:
y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y

case ha
y : ℕ → Bool
x : ℝ := ⋯
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get n ≠ 1

case hb
y : ℕ → Bool
x : ℝ := ⋯
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (bif y n then 2 else 0) ≠ 1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
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
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
have hts : edist t s ≤ c := by rw [edist_comm]; exact hst

Goal state after:
case inr
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
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
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:
by
  rw [← not_iff_not]
  simp [not_nonempty_iff_eq_empty]

Goal state after:
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:
by
  rw [← not_iff_not]
  simp [not_nonempty_iff_eq_empty]

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:
by
  rw [← not_iff_not]
  simp [not_nonempty_iff_eq_empty]

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}
⊢ IsClosed (candidatesB X Y)

Tactic:
have I2 : ∀ x y, IsClosed { f : Cb X Y | f (inr x, inr y) = dist x y } := fun x y =>
    isClosed_eq (continuous_eval_const _) continuous_const

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}
⊢ IsClosed (candidatesB X Y)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ minimalCover ε A ⊆ A

Tactic:
by grind [minimalCover]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ (minimalCover ε A).Finite

Tactic:
by grind [minimalCover]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : coveringNumber ε A ≠ ⊤
⊢ IsCover ε A (minimalCover ε A)

Tactic:
by grind [minimalCover]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : coveringNumber ε A ≠ ⊤
⊢ (minimalCover ε A).encard = coveringNumber ε A

Tactic:
by grind [minimalCover]

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

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

Tactic:
simp_rw [iSup_subtype, iSup_and] at h_exists

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

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

Tactic:
by_cases! h_top : packingNumber ε A ≠ ⊤

Goal state after:
case pos
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A ≠ ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A

case neg
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A = ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A
Module: Mathlib.Topology.MetricSpace.Infsep

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

Tactic:
le_iInf_iff

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

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

Tactic:
le_iInf_iff

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Tactic:
have hb : BddBelow (uncurry dist '' s.offDiag) := by
      refine ⟨0, fun d h => ?_⟩
      simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
      rcases h with ⟨_, _, _, rfl⟩
      exact dist_nonneg

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

Goal state before:
pp: case refine_1
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p

Tactic:
rcases Setoid.symm h with ⟨e⟩

Goal state after:
case refine_1
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p
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)
this : ∀ (i : ι), ∃ r' < r i, v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
choose r' hlt hsub using this

Goal state after:
α : 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
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
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)
this : ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
choose r' hlt hsub using this

Goal state after:
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
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 ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
x : α × β
⊢ IsOpen[instTopologicalSpaceProd] (Ici x)ᶜ

Tactic:
exact (isClosed_Ici.prod isClosed_Ici).isOpen_compl

Goal state after: