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

Goal state before:
pp: case zero
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ IsClosed sᵈ[0]

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ perfectKernel s ⊆ perfectKernel t

Tactic:
simpa [perfectKernel] using Set.iInter_mono'' (iteratedDerivedSet_mono hst)

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
q : X.A
h✝ : q ∈ Q
⊢ (X.str ⁻¹' Q).Nonempty

Tactic:
use X.incl q

Goal state after:
case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
C0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
C1 : ssu := ⋯
C2 : Set (Set (Ultrafilter X.A)) := ⋯
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
Q : Set X.A
hQ : Q ∈ F
q : X.A
h✝ : q ∈ Q
⊢ X.incl q ∈ X.str ⁻¹' Q
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
U : Set (WithGeneratedByTopology X Z)
hU : IsOpen U
⊢ IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' U)

Tactic:
WithGeneratedByTopology.isOpen_iff

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
U : Set (WithGeneratedByTopology X Z)
hU : ∀ ⦃i : ι⦄ (f : C(X i, Z)), IsOpen[inst✝² i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' U)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : IsOpen U
⊢ IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
WithGeneratedByTopology.isOpen_iff

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : ∀ ⦃i_1 : ι⦄ (f : C(X i_1, X i)), IsOpen[inst✝¹ i_1] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU : IsOpen U
⊢ IsOpen (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
WithGeneratedByTopology.isOpen_iff

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
h : ∀ (J : Finset ι), (π_app C fun x ↦ x ∈ J) a = (π_app C fun x ↦ x ∈ J) b
⊢ a = b

Tactic:
by
  ext i
  specialize h ({i} : Finset ι)
  rw [Subtype.ext_iff] at h
  simp only [π_app, ContinuousMap.precomp, ContinuousMap.coe_mk] at h
  exact congr_fun h ⟨i, Finset.mem_singleton.mpr rfl⟩

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
⊢ Injective (openCell 0)

Tactic:
by
  intro x y h
  rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
  exact injective_map_zero C h

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

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
rw [hx, ne_eq, Bool.not_eq_false] at ha

Goal state after:
case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Tactic:
exact Submodule.subset_span ⟨a, h', rfl⟩

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
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
⊢ ∀ a ∈ ↑l, ord I a < o

Tactic:
intro a

Goal state after:
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 : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
a : I
⊢ a ∈ ↑l → ord I a < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
⊢ Function.Injective (ι S)

Tactic:
intro a

Goal state after:
case hf
S : Profinite
a : ↑S.toTop
⊢ ∀ ⦃a₂ : ↑S.toTop⦄, ι S a = ι S a₂ → a = a₂
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case h
α : 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 = ∅
⊢ dissipate s g.choose = ∅

Tactic:
← subset_empty_iff

Goal state after:
case h
α : 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 = ∅
⊢ dissipate s g.choose ⊆ ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
h₃ : ∀ (v : ℕ), n ≤ v → dissipate s v = dissipate s' v
⊢ dissipate s' (max j n) = ∅

Tactic:
← subset_empty_iff

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j ⊆ ∅
h₃ : ∀ (v : ℕ), n ≤ v → dissipate s v = dissipate s' v
⊢ dissipate s' (max j n) ⊆ ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ x, dissipate C x).Nonempty

Tactic:
refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (Set.dissipate C)
    (fun n ↦ ?_) h_nonempty ?_ (fun n ↦ isClosed_biInter (fun i _ ↦ (hC_cc i).2))

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
n : ℕ
⊢ dissipate C (n + 1) ⊆ dissipate C n

case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ IsCompact (dissipate C 0)
Module: Mathlib.Topology.Connected.CardComponents

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

Tactic:
rw [Set.iUnion_eq_univ_iff]

Goal state after:
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}))
⊢ ∀ (x : X), ∃ i, x ∈ f ⁻¹' mk ⁻¹' {i}
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
⊢ Finite (ConnectedComponents X)

Tactic:
suffices h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents (f ⁻¹' mk ⁻¹' {y})) by
    refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
    · exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)
    · exact fun i j hij ↦ (Disjoint.preimage mk (by simpa)).preimage f
    · rw [Set.iUnion_eq_univ_iff]
      exact fun x ↦ ⟨mk (f x), rfl⟩
  intro y
  obtain ⟨y, rfl⟩ := surjective_coe y
  have := isConnected_iff_connectedSpace.mp (isConnected_connectedComponent (x := y))
  rw [connectedComponents_preimage_singleton]
  refine IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace
    (hf₁.restrictPreimage (connectedComponent y)) (hf₂.restrictPreimage (connectedComponent y))
    (y := ⟨y, mem_connectedComponent⟩) ?_
  rw [← Set.finite_image_iff Subtype.val_injective.injOn]
  convert! h y
  aesop (add safe mem_connectedComponent)

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
⊢ (range x ∩ A).Infinite

Tactic:
eventually_iff,

Goal state after:
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : {x_1 | x x_1 ∈ A} ∈ cofinite
hfin : (range x).Infinite
⊢ (range x ∩ A).Infinite
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
⊢ SecondCountableTopology C(X, Y)

Tactic:
apply secondCountableTopology

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
⊢ ∃ S,
    S.Countable ∧
      (∀ K ∈ S, IsCompact K) ∧
        ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝³] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
x : ↑(Icc a c)
hx : ↑x ≤ b
fg : { fg // fg.1 ⊤ = fg.2 ⊥ }
⊢ (concatCM fg) x = (↑fg).1 ⟨↑x, ⋯⟩

Tactic:
by
  exact concat_left fg.2 hx

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x

Tactic:
intro a

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
⊢ a ∈ f ⁻¹' s → f ⁻¹' s ∈ 𝓝 a
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
r : ℕ
hr : ∀ (b : ℕ), r ≤ b → ↑(#V) < a ^ b
⊢ ∃ r, 1 ≤ r ∧ ↑(#({x ∈ V | edist t x ≤ ↑r * c})) ≤ a ^ r

Tactic:
exact ⟨max r 1, le_max_right r 1,
    le_trans (mod_cast Finset.card_filter_le V _) (hr (max r 1) (le_max_left r 1)).le⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

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

Tactic:
have := ENNReal.tendsto_nhds_top_iff_nat.1
    ((ENNReal.tendsto_rpow_atTop_of_one_lt_base ha).comp tendsto_natCast_atTop_atTop) #V
  simp only [Function.comp_apply, ENNReal.rpow_natCast, Filter.eventually_atTop] at this
  obtain ⟨r, hr⟩ := this
  exact ⟨max r 1, le_max_right r 1,
    le_trans (mod_cast Finset.card_filter_le V _) (hr (max r 1) (le_max_left r 1)).le⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case zero
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
⊢ (logSizeBallSeq J hJ a c 0).point ∈ J

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case zero
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
⊢ ↑(#(pairSetSeq J a c 0)) ≤
    (if (logSizeBallSeq J hJ a c 0).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c 0).radius

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ 1 / 4 ∈ preCantorSet 0 ∧ 3 / 4 ∈ preCantorSet 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ 0 ∈ preCantorSet 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ofDigits a ∈ preCantorSet 0

Tactic:
| zero =>

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

Goal state before:
pp: a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
n0 : ℕ := Nat.find h
h1 : ∀ n < n0, a n = b n
⊢ a n0 ≠ b n0

Tactic:
simpa using Nat.find_spec h

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

Goal state before:
pp: case zero
x : ℝ
hx : x ∈ cantorSet
⊢ (cantorSequence x).get 0 ∈ cantorSet

Tactic:
| zero =>

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

Goal state before:
pp: case zero
x : ℝ
⊢ (cantorSequence x).get 0 = (x - ∑ i ∈ Finset.range 0, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
Y : Type u_3
f : Y → PseudoMetric X R
s : Finset Y
hs : s.Nonempty
⊢ ⇑(s.sup f) = ⇑(s.sup' hs fun x ↦ f x)

Tactic:
simpa using (Finset.sup'_eq_sup hs (f ·)).symm

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

Goal state before:
pp: case inr.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
⊢ LipschitzWith K f_ext'

pp: case inr.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
⊢ EqOn f f_ext' s

Tactic:
· rw [LipschitzWith.coordinate]
      exact hgl

Goal state after:
case inr.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
⊢ EqOn f f_ext' s
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case inr.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
⊢ EqOn f f_ext' s

Tactic:
intro a

Goal state after:
case inr.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
a : α
⊢ a ∈ s → f a = f_ext' a
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

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

Tactic:
by
  intro x hxA
  by_contra! h_dist
  let C := {x} ∪ maximalSeparatedSet ε A
  have hx_not_mem : x ∉ maximalSeparatedSet ε A := by simpa using h_dist x
  suffices C ⊆ A ∧ IsSeparated ε C by
    refine absurd (encard_le_of_isSeparated this.1 this.2 h) ?_
    simp [C, encard_insert_of_notMem hx_not_mem,
      ENat.lt_add_one_iff (encard_maximalSeparatedSet h ▸ h)]
  constructor
  · simp [C, hxA, maximalSeparatedSet_subset, Set.insert_subset]
  · exact isSeparated_insert_of_notMem hx_not_mem |>.mpr
      ⟨isSeparated_maximalSeparatedSet, by simpa using h_dist⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
eHolderNorm_eq_zero

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ (∀ (x₁ x₂ : X), f x₁ = f x₂) ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
by_cases hxy : x = y
  · rw [hxy]
    simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.toReal_zero]
  · rw [infsep, einfsep_pair hxy]

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

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

Tactic:
image_toSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ ⇑ofSnowflaking ⁻¹' eball x r = eball (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

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

Tactic:
image_toSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ ⇑ofSnowflaking ⁻¹' closedEBall x r = closedEBall (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C
x : X
hx : { val := x } ∈ s
y : X
hy : { val := y } ∈ s
⊢ dist { val := x } { val := y } ≤ C ^ α

Tactic:
mk_eq_toSnowflaking,

Goal state after:
case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C
x : X
hx : { val := x } ∈ s
y : X
hy : { val := y } ∈ s
⊢ dist (toSnowflaking x) (toSnowflaking y) ≤ C ^ α
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑toSnowflaking '' ball x r = ball (toSnowflaking x) (r ^ α)

Tactic:
image_toSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑ofSnowflaking ⁻¹' ball x r = ball (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑toSnowflaking '' closedBall x r = closedBall (toSnowflaking x) (r ^ α)

Tactic:
image_toSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑ofSnowflaking ⁻¹' closedBall x r = closedBall (toSnowflaking x) (r ^ α)