mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ⇑f '' K ⊆ ⋃ i ∈ {s | s ∈ T ∧ s ⊆ U}, i
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t

Tactic:
obtain ⟨t, ht, hfin, htK⟩ :=
        (hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU

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 : ⇑f '' K ⊆ ⋃ i ∈ {s | s ∈ T ∧ s ⊆ U}, i
t : Set (Set Y)
ht : t ⊆ {s | s ∈ T ∧ s ⊆ U}
hfin : t.Finite
htK : ⇑f '' K ⊆ ⋃ i ∈ t, i
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t
Module: Mathlib.Topology.Germ

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X✝
f✝ g✝ : X✝ → Y
A : Set X✝
x✝ : X✝
X : Type u_4
α : Type u_5
inst✝ : TopologicalSpace X
x : X
φ : (𝓝 x).Germ α
f g : X → α
h : ((𝓝 x).germSetoid α) f g
⊢ f x = g x

Tactic:
rw [Eventually.self_of_nhds h]

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

Goal state before:
pp: θ : ↑I
⊢ ↑θ + 1 ≤ 2

Tactic:
← one_add_one_eq_two

Goal state after:
θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: ⊢ Continuous toENNReal

Tactic:
refine OrderTopology.continuous_iff.mpr fun a ↦ ⟨?_, ?_⟩

Goal state after:
case refine_1
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Ioi a)

case refine_2
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n : ℕ
ih : 0 ∈ preCantorSet n
⊢ (fun x ↦ x / 3) 0 = 0

Tactic:
by simp only [zero_div]

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed ((fun x ↦ x i) '' s)

Tactic:
suffices IsClosed (Set.domRestrict {i} '' s) by
    have : Homeomorph.piUnique _ ∘ Set.domRestrict {i} = fun (x : Π j, α j) ↦ x i := rfl
    rwa [← this, image_comp, Homeomorph.isClosed_image (Homeomorph.piUnique _)]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed ({i}.domRestrict '' s)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
this : List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)

Tactic:
by
        simpa only [functor_norm] using! this

Goal state after:
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
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.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.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
⊢ (fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩)
      ((fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) p) =
    p

Tactic:
ext y

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
y : N → ↑I
⊢ ((fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩)
        ((fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) p))
      y =
    p y
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {x | edist x.2 x.1 ≤ δ} (s, t).1
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ

Tactic:
have {s t : Set α} (h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t) :
      ⨆ x ∈ s, infEDist x t ≤ δ := by
    rw [iSup₂_le_iff]
    intro x hx
    obtain ⟨y, hy, hxy⟩ := h hx
    exact iInf₂_le_of_le y hy hxy

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {x | edist x.2 x.1 ≤ δ} (s, t).1
this : ∀ {s t : Set α}, s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t → ⨆ x ∈ s, infEDist x t ≤ δ
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
⊢ LipschitzWith 2 fun p ↦ infDist p.1 ↑p.2

Tactic:
← one_add_one_eq_two

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
⊢ LipschitzWith (1 + 1) fun p ↦ infDist p.1 ↑p.2
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : TopologicalSpace α
inst✝¹ : IsLower α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, inst✝²] f ↔ ∀ (a : α), IsClosed[inst✝] (f ⁻¹' Ici a)

Tactic:
by
  obtain rfl := IsLower.topology_eq α
  simp [continuous_generateFrom_iff]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
⊢ Continuous[inst✝³, inst✝²] f → Monotone f

Tactic:
· intro hf a b hab
    rw [← mem_Iic, ← closure_singleton] at hab ⊢
    apply Continuous.closure_preimage_subset hf {f b}
    apply mem_of_mem_of_subset hab
    apply closure_mono
    rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]

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✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f g : EsakiaHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

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

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ (IsSuccPrelimit (ofLex (toLex (x, s))).1 → 0 ≤ (ofLex (toLex (x, s))).2) ∧
    (IsPredPrelimit (ofLex (toLex (x, s))).1 → (ofLex (toLex (x, s))).2 ≤ 0)

Tactic:
grind [ofLex_toLex]

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

Goal state before:
pp: α : Type ?u.3
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set ↑T
⊢ sInf (Subtype.val '' hull T (OrderDual.ofDual (sInf (Subtype.val '' S)))) ≤ OrderDual.ofDual (sInf (Subtype.val '' S))

Tactic:
exact sInf_le_sInf <| image_val_mono fun c hcS => by
      rw [hull, mem_preimage, mem_Ici]
      exact sInf_le (mem_image_of_mem Subtype.val hcS)

Goal state after:
Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ False

Tactic:
grewrite [

Goal state after:
case inr.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ False
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) = dist x y + dist y z

Tactic:
by rw [x.toGHSpace_rep, y.toGHSpace_rep, z.toGHSpace_rep]

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h✝ : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
h : C(X, ℝ) := { toFun := fun x ↦ ∑' (n : ℕ), (f n) x * (1 / 2 / 2 ^ n), continuous_toFun := ⋯ }
x : X
n : ℕ
⊢ 0 ≤ (f n) x * (1 / 2 / 2 ^ n)

Tactic:
simp [(hfr n x).1]

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

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)

pp: case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)

Tactic:
· have hV : p₀ ∈ unop V := leOfHom iWV.unop hW
      simp only [dif_pos hW, dif_pos hV, eqToHom_trans]

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)
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 + δ
xY : Y
h✝ : xY ∈ univ
xs' : ↑s
Dxs' : dist xY (Φ xs') ≤ ε₃
this : 0 ≤ ε₃
⊢ hausdorffDist (range Φ) univ ≤ ε₃

Tactic:
refine hausdorffDist_le_of_mem_dist this
      (fun x _ => ⟨x, mem_univ _, by simpa only [dist_self]⟩)
      fun x _ => ?_

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
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 + δ
xY : Y
h✝ : xY ∈ univ
xs' : ↑s
Dxs' : dist xY (Φ xs') ≤ ε₃
this : 0 ≤ ε₃
x : Y
x✝ : x ∈ univ
⊢ ∃ y ∈ range Φ, dist x y ≤ ε₃
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
⊢ ∀ (a : F.EtaleSpace),
    (∃ (hgU : a.base ∈ U), a.germ = (ConcreteCategory.hom (F.germ U a.base hgU)) f) →
      ∀ (a_2 : ↑(base ⁻¹' ↑U)),
        ↑a_2 = a →
          WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑a_2).germ)) =
            WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ g.germ))

Tactic:
rintro _ ⟨hgU, hgf⟩ g' rfl

Goal state after:
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
f : CC (F.obj (op U))
hf : (ConcreteCategory.hom (F.germ U g.base hg)) f = g.germ
g' : ↑(base ⁻¹' ↑U)
hgU : (↑g').base ∈ U
hgf : (↑g').germ = (ConcreteCategory.hom (F.germ U (↑g').base hgU)) f
⊢ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑g').germ)) =
    WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ g.germ))
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₂ ⊔ sq.X₃
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
obtain (hx | hx) := hx

Goal state after:
case inl
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ ↑sq.X₂
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

case inr
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ ↑sq.X₃
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2.refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)) (i : ↑(candidatesB X Y)), dist (↑i x) (↑i y) ≤ 2 * ↑(maxVar X Y) * dist x y

Tactic:
rintro x y ⟨f, hf⟩

Goal state after:
case refine_2.refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : f ∈ candidatesB X Y
⊢ dist (↑⟨f, hf⟩ x) (↑⟨f, hf⟩ y) ≤ 2 * ↑(maxVar X Y) * dist x y
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: case h.refine_1
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ W ⊓ (U' ⊓ V') ⟶ ↑U

Tactic:
exact Opens.infLERight _ _ ≫ Opens.infLELeft _ _ ≫ iU

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
⊢ x ∈ sublevelLeft X f b' ↑y

Tactic:
suffices sublevelLeft X f b' z' ⊆ sublevelLeft X f b' y from this hxz'

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
⊢ sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y
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 = ∅}
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'
⊢ False

Tactic:
have hZ_closed : IsClosed Z := isClosed_sInter fun b hb ↦ hb.2

Goal state after:
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
⊢ False
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ s : ↑I
⊢ (γ.subpath t₀ t₁).symm s = (γ.subpath t₁ t₀) s

Tactic:
simp [subpath]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t s : ↑I
⊢ (γ.subpath t t) s = (refl (γ t)) s

Tactic:
simp [subpath]

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
s : ↑I
⊢ (γ.subpath 0 1) s = (γ.cast ⋯ ⋯) s

Tactic:
simp [subpath]

Goal state after: