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

Goal state before:
pp: case a
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
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

Tactic:
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]

Goal state after:
case a
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
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : ⇑f '' K ⊆ ⋃₀ t
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
s : Set ι
f : ι → Set E
hs : s.Finite
hf : ∀ i ∈ s, IsCountablyCompact (f i)
s' : Finset ι := hs.toFinset
⊢ ⋃ i ∈ s, f i = ⋃ i ∈ s', f i

Tactic:
simp [s']

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

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
x : Option α
⊢ none ∈ Metric.eball none r → none = none

Tactic:
tauto

Goal state after:
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✝ : edist (some z) (some x) < r
⊢ z ∈ s' ∧ some z = some z

Tactic:
tauto

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

Goal state before:
pp: t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2

Tactic:
tauto

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

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

Tactic:
linarith

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 : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
this : #(logSizeBallSeq J hJ a c i).finset = 0
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - (i + 1)

Tactic:
simp [this]

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

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hM : y ∘ Sum.inl ∈ Cube.boundary M
this : p (y ∘ Sum.inl) = const
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
simp [this]

Goal state after:
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
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this✝ :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
this : s = t
⊢ edist s t ≤ ↑n * c

Tactic:
simp [this]

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

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
h :
  ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm a n1 + (3⁻¹ ^ n1 * ofDigits fun i ↦ a (1 + n1 + i)) * (1 / 3) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + (3⁻¹ ^ n1 * ofDigits fun i ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1
⊢ ofDigitsTerm a n1 + (3⁻¹ ^ n1 * ofDigits fun i ↦ a (1 + n1 + i)) * (1 / 3) =
    (3⁻¹ ^ n1 * ofDigits fun i ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1

Tactic:
linarith

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

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

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

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

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
h :
  ((3 ^ n1)⁻¹ * ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ =
    ((3 ^ n1)⁻¹ * ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * (3⁻¹ * (3 ^ n1)⁻¹)
⊢ (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹) =
    (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * 3⁻¹)

Tactic:
linarith

Goal state after:
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₂

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ a₂ : ↑(Ω^ N X x)
⊢ (Homotopic.setoid N x) a₁ a₂ ↔
    (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A = A.encard

Tactic:
refine le_antisymm (externalCoveringNumber_le_encard_self A) ?_
  refine le_iInf fun C ↦ le_iInf fun hC₁ ↦ ?_
  rw [isCover_zero] at hC₁
  exact encard_le_encard hC₁

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
let KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH

Goal state after:
X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
⊢ ∃ f, Continuous f ∧ Function.Surjective f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.Nontrivial → 0 < s.einfsep

Tactic:
exact fun _ => einfsep_pos_of_finite

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
f : ℕ → X
hf : ∀ (n : ℕ), f n ∈ U n
⊢ ∃ f, IsEmbedding f

Tactic:
refine ⟨f, IsInducing.isEmbedding ⟨Eq.symm (eq_bot_of_singletons_open fun n ↦ ⟨U n, hUo n, ?_⟩)⟩⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
f : ℕ → X
hf : ∀ (n : ℕ), f n ∈ U n
n : ℕ
⊢ f ⁻¹' U n = {n}
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
⊢ ∃ s, s.Infinite ∧ DiscreteTopology ↑s

Tactic:
rcases exists_topology_isEmbedding_nat X with ⟨f, hf⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ ∃ s, s.Infinite ∧ DiscreteTopology ↑s
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

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

Tactic:
· intro ⟨a, ha⟩
    use {U}
    constructor
    · apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)
      use a
    · rw [sUnion_singleton]

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

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsClosed[t] s ↔ DirSupClosedOn D s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_dirSupInaccOn hDL, dirSupInaccOn_compl]

Goal state after:
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Iio c)

Tactic:
have : IsOpen (⋃ a ∈ c.left, Iio a) := isOpen_biUnion fun _ _ ↦ isOpen_Iio
    convert this
    ext
    simp [principal_lt_iff]

Goal state after:
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1
α : 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
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

Tactic:
obtain hq | hq := le_or_gt 0 q

Goal state after:
case refine_1.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 : 0 ≤ q
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

case refine_1.inr
α : 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 ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)
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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this : 0 ≤ ε₂
p q : ↑s
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)

Tactic:
linarith

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ↑⊥.openNhds
⊢ ⊥ ≤ x✝

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝¹ : ↑⊥.openNhds
x✝ : ⊥ ⟶ x✝¹
⊢ ∀ {Z : ↑⊥.openNhds} (h : Z ⟶ ⊥), h ≫ x✝ = h ≫ homOfLE ⋯

Tactic:
tauto

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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this✝ : 0 ≤ ε₂
this : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
⊢ 0 < ε₂ / 2 + δ

Tactic:
linarith

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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁴ : 0 ≤ ε₂
this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
⊢ 0 ≤ ε₂ / 2 + δ

Tactic:
linarith

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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁶ : 0 ≤ ε₂
this✝⁵ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝⁵
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝⁴ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝³ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝² :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this✝¹ : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this✝ : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
this : hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
linarith

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

Goal state before:
pp: case refine_3
δ : ℝ
δ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 y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
have hjq : j < N q := by rwa [Npq] at hjp

Goal state after:
case refine_3
δ : ℝ
δ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 y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
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 y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε

Tactic:
have hjq : j < N q := by rwa [Npq] at hjp

Goal state after:
case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
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 y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ IsEmpty X

Tactic:
cases h

Goal state after:
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsEmpty X
⊢ IsEmpty X
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
this : ∃ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅
⊢ 𝒮.Nonempty

Tactic:
tauto

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : HasSmallInductiveDimensionLT X n
⊢ smallInductiveDimension X < ↑n

Tactic:
by
    cases n with
    | zero =>
      rw [smallInductiveDimension, csInf_eq_bot_of_bot_mem]
      · simp
      · exact fun _ _ ↦ h.mono zero_le
    | succ n =>
      apply (smallInductiveDimension_le_iff.2 h).trans_lt
      exact_mod_cast n.lt_add_one

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompareReals

Goal state before:
pp: ⊢ IsUniformInducing Rat.cast

Tactic:
rw [Rat.uniformSpace_eq]

Goal state after:
⊢ IsUniformInducing Rat.cast
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)

Tactic:
· dsimp
    rintro _ ⟨_, _, _⟩
    infer_instance

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' id i)

Tactic:
· dsimp
    rintro _ ⟨_, _, _⟩
    infer_instance

Goal state after: