mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ closedCell m j = ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
by
  refine subset_antisymm ?_ (inter_subset_inter_right _ (cellFrontier_subset_closedCell _ _))
  rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
  apply union_subset (by rfl)
  rw [(disjoint_skeletonLT_openCell hnm).inter_eq]
  exact empty_subset _

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
m : ℕ
⊢ ↑m ≤ (f ⁻¹' {y}).encard

Tactic:
obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Infinite (ConnectedComponents X)
m : ℕ
U : Fin (m + 1) → Set X
hU1 : ∀ (i : Fin (m + 1)), IsClopen (U i)
hU2 : ∀ (i : Fin (m + 1)), (U i).Nonempty
hU3 : Pairwise (Disjoint on U)
hU4 : ⋃ i, U i = Set.univ
⊢ ↑m ≤ (f ⁻¹' {y}).encard
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
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
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
rw [h, max_eq_o_cons_tail C hsC ho l]
    exact List.Lex.nil

Goal state after:
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
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf : Tendsto F p (𝓝 f)
hg : Tendsto G p (𝓝 g)
⊢ Tendsto (fun i ↦ (F i).concat (G i)) p (𝓝 (f.concat g))

Tactic:
tendsto_nhds_compactOpen

Goal state after:
α : 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
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
⊢ ∀ (K : Set ↑(Icc a c)),
    IsCompact K →
      ∀ (U : Set E),
        IsOpen[inst✝] U → MapsTo (⇑(f.concat g)) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑((F a_4).concat (G a_4))) K U
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
⊢ IsCompact A

Tactic:
have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s
  let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M
  refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
      fun f hf => ?_
  · have : CompactSpace s := isCompact_iff_compactSpace.1 hs
    refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_
    rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff]
    exact H.comp (A.restrictPreimage F)
  · let g := codRestrict s f fun x => in_s f x hf
    rw [show f = F g by ext; rfl] at hf ⊢
    exact ⟨g, hf, rfl⟩

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact (f '' A)
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ A
⊢ ∃ a ∈ A, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
by
    obtain ⟨fa, hfa, ⟨φ, hφ⟩⟩ := hA (fun n => mem_image_of_mem f (hx n))
    choose a ha using hfa
    exact ⟨a, ha.1, φ, hφ.1, hf.tendsto_nhds_iff.2 (ha.2 ▸ hφ.2)⟩

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

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hB : IsCountablyCompact B
⊢ IsCountablyCompact (A ∪ B)

Tactic:
rw [isCountablyCompact_iff_countable_open_cover'] at hA hB ⊢
  intro U hUo hAU
  obtain ⟨t₁, ht₁, hA_sub⟩ : ∃ (t₁ : Set ℕ), t₁.Finite ∧ A ⊆ ⋃ k ∈ t₁, U k :=
    hA U hUo (subset_union_left.trans hAU)
  obtain ⟨t₂, ht₂, hB_sub⟩ : ∃ (t₂ : Set ℕ), t₂.Finite ∧ B ⊆ ⋃ k ∈ t₂, U k :=
    hB U hUo (subset_union_right.trans hAU)
  have h : (⋃ k ∈ t₁, U k) ∪ (⋃ k ∈ t₂, U k) = ⋃ k ∈ (t₁ ∪ t₂), U k := by ext; aesop
  exact ⟨t₁ ∪ t₂, ht₁.union ht₂, h ▸ union_subset_union hA_sub hB_sub⟩

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
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
x : X
hx : x ∈ A
⊢ ∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g

Tactic:
intro y hy

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

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x✝¹ : Option α
r✝ : ℝ≥0∞
x : α
s' : Set α
s'o : IsOpen[t] s'
y : Option α
z : α
s's : z ∈ s' ↔ edist z x < r✝
yh : edist (some z) (some x) < ∞
x✝ : ∃ x ∈ s', some x = some z
r : α
rh : r ∈ s'
rh' : some r = some z
⊢ edist (some z) (some x) < r✝

Tactic:
exact s's.1 <| h.injective rh' ▸ rh

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:
exact point_mem_finset_logSizeBallSeq hJ 0 hJ

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

Goal state before:
pp: case hba.refine_1
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).point ∈ ↑(logSizeBallSeq J hJ a c i).finset

pp: case hba.refine_2
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).point ∉ ↑(logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
· exact point_mem_finset_logSizeBallSeq hJ i h

Goal state after:
case hba.refine_2
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).point ∉ ↑(logSizeBallSeq J hJ a c (i + 1)).finset
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
n✝ : ℕ
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
t : T
i : ℕ
hiJ : i < #J
hJ : J.Nonempty
hn : 1 ≤ n
ht : t ∈ (logSizeBallSeq J ⋯ a c i).finset
hdist : edist (logSizeBallSeq J ⋯ a c i).point t ≤ ↑(logSizeBallSeq J ⋯ a c i).radius * c
h : ((logSizeBallSeq J ⋯ a c i).point, t) ∈ pairSet J a c
⊢ edist (logSizeBallSeq J ⋯ a c i).point t ≤ ↑n * c

Tactic:
hdist,

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
n✝ : ℕ
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
t : T
i : ℕ
hiJ : i < #J
hJ : J.Nonempty
hn : 1 ≤ n
ht : t ∈ (logSizeBallSeq J ⋯ a c i).finset
hdist : edist (logSizeBallSeq J ⋯ a c i).point t ≤ ↑(logSizeBallSeq J ⋯ a c i).radius * c
h : ((logSizeBallSeq J ⋯ a c i).point, t) ∈ pairSet J a c
⊢ ↑(logSizeBallSeq J ⋯ a c i).radius * c ≤ ↑n * c
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:
rw [cantorSequence_get_succ, ih, Finset.sum_range_succ]; ring

Goal state after:
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 <;> intro H
  · exact ⟨H.continuous, H.universally_closed _⟩
  · rw [isProperMap_iff_ultrafilter]
    refine ⟨H.1, fun 𝒰 y hy ↦ ?_⟩
    let F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
    have := H.2 F isClosed_closure
    have : (y, 𝒰) ∈ Prod.map f id '' F :=
      this.mem_of_tendsto (hy.prodMk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
        (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)
    rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
    refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
    rw [mem_closure_iff_nhds] at hx
    rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc))
      with ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩
    exact hy' hy

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
⊢ ∃ K ⊆ J ×ˢ J,
    ↑(#K) ≤ a * ↑(#J) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
rcases le_or_gt a 1 with ha1 | ha1
  · rcases isEmpty_or_nonempty J with hJ | hJ
    · simp only [Finset.isEmpty_coe_sort] at hJ
      simp [hJ]
    obtain ⟨x₀, rfl⟩ : ∃ x₀, J = {x₀} := by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]
    simp_all
  · exact ⟨pairSet J a c, pairSet_subset, card_pairSet_le ha1,
      fun _ _ ↦ edist_le_of_mem_pairSet ha1 hJ_card, iSup_edist_pairSet ha1⟩

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

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ edist x y ≤ edist (x, s) (y, t)

Tactic:
apply_rules [le_max_left, le_max_right]

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ hausdorffEDist ↑s ↑t ≤ edist (x, s) (y, t)

Tactic:
apply_rules [le_max_left, le_max_right]

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

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e

Tactic:
rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with ⟨n, hn⟩

Goal state after:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) + f (t, y) ≤ ↑(maxVar X Y) * dist x z + ↑(maxVar X Y) * dist t y

Tactic:
gcongr <;> apply candidates_dist_bound fA

Goal state after:
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, ⋯⟩
a : α
⊢ a ∈ s → f a = f_ext' a

Tactic:
hyp

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 : α
hyp : 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 ≠ ⊤
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

Tactic:
rcases Set.eq_empty_or_nonempty A with hA | hA

Goal state after:
case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A = ∅
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : MemHolder r f ∧ MemHolder r g
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : ¬(MemHolder r f ∧ MemHolder r g)
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
· obtain ⟨hf, hg⟩ := hfg
    rw [← hf.coe_nnHolderNorm_eq_eHolderNorm, ← hg.coe_nnHolderNorm_eq_eHolderNorm,
      ← (hf.add hg).coe_nnHolderNorm_eq_eHolderNorm, ← coe_add, ENNReal.coe_le_coe]
    exact hf.nnHolderNorm_add_le hg

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
hfg : ¬(MemHolder r f ∧ MemHolder r g)
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ‖c‖₊ = 0
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
nnnorm_eq_zero

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : c = 0
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : eHolderNorm r f = ∞
⊢ ¬MemHolder r f

Tactic:
nnnorm_eq_zero

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬c = 0
hf : eHolderNorm r f = ∞
⊢ ¬MemHolder r f
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
⊢ ⇑ofSnowflaking ⁻¹' ball x r = ball (toSnowflaking x) (r ^ α)

Tactic:
ext ⟨y⟩
  simp (disch := positivity) [Real.rpow_lt_rpow_iff]

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h : Inhabited X
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
inhabit Y

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
⊢ (∃ a, (Ici a)ᶜ = U) → ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
intro ⟨a, ha⟩

Goal state after:
case mp
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
convert isOpen_Iio (a := x)

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ ⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩ = Iio x
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
this : IndiscreteTopology ↑X
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows

Tactic:
· convert! Presieve.isSheafFor_top (F ⋙ coyoneda.obj (@op C c))
    rw [Sieve.arrows_eq_top_iff, ← Sieve.id_mem_iff_eq_top]
    have := U.eq_bot_or_top.resolve_left hne
    subst this
    obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
    · exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
    obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
    obtain rfl | rfl := U.eq_bot_or_top
    · cases hm
    · convert! hf

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
⊢ map' p₀ (𝟙 a) = 𝟙 (skyscraperPresheaf p₀ a)

Tactic:
ext U
  simp only [SkyscraperPresheafFunctor.map'_app]; split_ifs <;> cat_disch

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

Goal state before:
pp: case h
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
⊢ dist x (Φ z) ≤ ε

Tactic:
have C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩ := by
        rw [ihi_eq]; exact (E q).symm_apply_apply ⟨y, ys⟩

Goal state after:
case h
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
⊢ dist x (Φ z) ≤ ε