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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ HasCompactSupport ⇑(ofCompactSupport (⇑g * ⇑↑f) ⋯ ⋯)

Tactic:
rw [ofCompactSupport]

Goal state after:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ HasCompactSupport ⇑{ toFun := ⇑g * ⇑↑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
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 : K ⊆ ⇑f ⁻¹' ⋃₀ t
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : f x ∈ V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)

Tactic:
rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩

Goal state after:
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 : K ⊆ ⇑f ⁻¹' ⋃₀ t
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : f x ∈ V
L : Set X
hLS : L ∈ S
hLx : L ∈ 𝓝 x
hLV : MapsTo (⇑f) L V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)
Module: Mathlib.Topology.EMetricSpace.Weak

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

Tactic:
match x with
  | (_ : α) => simp
  | none => tauto

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

Goal state before:
pp: H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ False

Tactic:
rw [tendsto_inf] at hx

Goal state after:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False
Module: Mathlib.Topology.EMetricSpace.PairReduction

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

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

Tactic:
· have := card_finset_logSizeBallSeq_add_one_lt hJ i h
      lia

Goal state after:
case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)
Module: Mathlib.Topology.EMetricSpace.PairReduction

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

Tactic:
suffices #(logSizeBallSeq J hJ a c i).finset = 0 by simp [this]

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

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = ⋂ i, (fun x ↦ x / 3) '' preCantorSet i ∪ (fun x ↦ (2 + x) / 3) '' preCantorSet i

Tactic:
← preCantorSet_succ

Goal state after:
⊢ ⋂ n, preCantorSet n = ⋂ i, preCantorSet (i + 1)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (((toLoop i p) (x✝ i)) fun j ↦ x✝ ↑j) = ↑p x✝

Tactic:
first
    | apply congr_arg p
    | apply congr_arg q

Goal state after:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑(Cube.insertAt i) (x✝ i, fun j ↦ x✝ ↑j) = x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (((toLoop i q) (x✝ i)) fun j ↦ x✝ ↑j) = ↑q x✝

Tactic:
first
    | apply congr_arg p
    | apply congr_arg q

Goal state after:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑(Cube.insertAt i) (x✝ i, fun j ↦ x✝ ↑j) = x✝
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ∀ i ⊆ A, IsSeparated (↑ε) i → i = ∅
x : X
hx : x ∈ A
⊢ False

Tactic:
simpa using h {x} (by simp [hx]) (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
⊢ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))

Tactic:
apply mem_iInter.1 xt0 n

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
simp only [packingNumber, ENNReal.coe_mul, ENNReal.coe_ofNat, externalCoveringNumber, le_iInf_iff,
    iSup_le_iff]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ (i : Set X), IsCover ε A i → ∀ i_2 ⊆ A, IsSeparated (2 * ↑ε) i_2 → i_2.encard ≤ i.encard
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

Tactic:
simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.einfsep = min (min (edist x y) (edist x z)) (edist y z)

Tactic:
simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
    ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]

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

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

Tactic:
by
  rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedBall _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : PseudoEpimorphism α β
f' : α → β
h : f' = ⇑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄, (f.copy f' h).toFun a ≤ b → ∃ c, a ≤ c ∧ (f.copy f' h).toFun c = b

Tactic:
by simpa only [h.symm, toFun_eq_coe] using! f.exists_map_eq_of_map_le'

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
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑p
hz : dist z (f (inr y)) < r
⊢ z ∈ range Φ

Tactic:
← Φrange

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
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ range Φ
hz : dist z (f (inr y)) < r
⊢ z ∈ range Φ
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen[inst✝] s✝
x : X
y : Y
ys : y ∈ s✝
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
⊢ f.preimage s ∈ 𝓝 x

Tactic:
have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen[inst✝] s✝
x : X
y : Y
ys : y ∈ s✝
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ f.preimage s ∈ 𝓝 x
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
L : ↑K.compactNhds
U : Opens α
h1 : ↑K ⊆ ↑U
h2 : ↑U ⊆ ↑↑L
⊢ ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ L

Tactic:
have h3 : closure (U : Set α) ⊆ L := (IsClosed.closure_subset_iff
    (IsCompact.isClosed L.1.isCompact') ).2 h2

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
L : ↑K.compactNhds
U : Opens α
h1 : ↑K ⊆ ↑U
h2 : ↑U ⊆ ↑↑L
h3 : closure ↑U ⊆ ↑↑L
⊢ ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ L
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_1
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) ≤ ε₁
⊢ ∀ x ∈ Fl '' s, ∃ y ∈ Fr '' range Φ, dist x y ≤ ε₂ / 2 + δ

Tactic:
intro x'

Goal state after:
case refine_1
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) ≤ ε₁
x' : X ⊕ Y
⊢ x' ∈ Fl '' s → ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_2
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) ≤ ε₁
⊢ ∀ x ∈ Fr '' range Φ, ∃ y ∈ Fl '' s, dist x y ≤ ε₂ / 2 + δ

Tactic:
intro x'

Goal state after:
case refine_2
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) ≤ ε₁
x' : X ⊕ Y
⊢ x' ∈ Fr '' range Φ → ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
b : ι
⊢ (α.hom.app (op (iSup U)) ≫
        ((Cone.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)).π.app WalkingParallelPair.zero) ≫
      Pi.π (fun i ↦ F.obj (op (U i))) b =
    res F U ≫ Pi.π (fun i ↦ F.obj (op (U i))) b

Tactic:
simp [res, diagram.isoOfIso]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ f.hom ≫ (coneEquivFunctorObj F U c').π.app WalkingParallelPair.zero =
    (coneEquivFunctorObj F U c).π.app WalkingParallelPair.zero

Tactic:
dsimp
            ext
            simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ f.hom ≫ (coneEquivFunctorObj F U c').π.app WalkingParallelPair.one =
    (coneEquivFunctorObj F U c).π.app WalkingParallelPair.one

Tactic:
dsimp
            ext
            simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (((((∀ (x y : X), dist (inl x) (inl y) = dist x y) ∧ ∀ (x y : Y), dist (inr x) (inr y) = dist x y) ∧
          ∀ (x y : X ⊕ Y), True) ∧
        ∀ (x y z : X ⊕ Y), dist x z ≤ dist x y + dist y z) ∧
      ∀ (x : X ⊕ Y), dist x x = 0) ∧
    ∀ (x y : X ⊕ Y), dist x y ≤ ↑(maxVar X Y)

Tactic:
dist_triangle,

Goal state after:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
⊢ (((((∀ (x y : X), dist (inl x) (inl y) = dist x y) ∧ ∀ (x y : Y), dist (inr x) (inr y) = dist x y) ∧
          ∀ (x y : X ⊕ Y), True) ∧
        ∀ (x x y : X ⊕ Y), True) ∧
      ∀ (x : X ⊕ Y), dist x x = 0) ∧
    ∀ (x y : X ⊕ Y), dist x y ≤ ↑(maxVar X Y)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ x, ⨅ y, (optimalGHDist X Y) (inl x, inr y) < r
I2 : ⨅ y, (optimalGHDist X Y) (inl z, inr y) ≤ ⨆ x, ⨅ y, (optimalGHDist X Y) (inl x, inr y)
I : ⨅ y, (optimalGHDist X Y) (inl z, inr y) < r
⊢ ∃ y ∈ range (optimalGHInjr X Y), dist (optimalGHInjl X Y z) y ≤ r

Tactic:
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩

Goal state after:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ x, ⨅ y, (optimalGHDist X Y) (inl x, inr y) < r
I2 : ⨅ y, (optimalGHDist X Y) (inl z, inr y) ≤ ⨆ x, ⨅ y, (optimalGHDist X Y) (inl x, inr y)
I : ⨅ y, (optimalGHDist X Y) (inl z, inr y) < r
z' : Y
hr' : (fun y ↦ (optimalGHDist X Y) (inl z, inr y)) z' < r
⊢ ∃ y ∈ range (optimalGHInjr X Y), dist (optimalGHInjl X Y z) y ≤ r
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
I1 : ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y) < r
I2 : ⨅ x, (optimalGHDist X Y) (inl x, inr z) ≤ ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y)
I : ⨅ x, (optimalGHDist X Y) (inl x, inr z) < r
⊢ ∃ y ∈ range (optimalGHInjl X Y), dist (optimalGHInjr X Y z) y ≤ r

Tactic:
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
I1 : ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y) < r
I2 : ⨅ x, (optimalGHDist X Y) (inl x, inr z) ≤ ⨆ y, ⨅ x, (optimalGHDist X Y) (inl x, inr y)
I : ⨅ x, (optimalGHDist X Y) (inl x, inr z) < r
z' : X
hr' : (fun x ↦ (optimalGHDist X Y) (inl x, inr z)) z' < r
⊢ ∃ y ∈ range (optimalGHInjl X Y), dist (optimalGHInjr X Y z) y ≤ r
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case neg.refine_2
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 = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub✝ : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
F : Set (Set X)
hsub : F ⊆ B'
hF : F.Finite
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ ⋂₀ F).Nonempty

Tactic:
· rw [← Set.sInter_union]
      refine hB.prop.2.1 (_ ∪ F) ?_ <| (hA₁'.sdiff.union hA₂'.sdiff).union hF
      grind [Set.sdiff_singleton_subset_iff, Set.union_subset_iff]

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ closure uc ⊆ ds ○ uc ○ ds

Tactic:
closure_eq_inter_uniformity

Goal state after:
case refine_1
X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ⋂ d ∈ 𝓤 X, d ○ (uc ○ d) ⊆ ds ○ uc ○ ds