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

Goal state before:
pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ 𝓝 ↑x

Tactic:
← map_nhds_subtype_coe_eq_nhds x.2

Goal state after:
case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ map Subtype.val (𝓝 ⟨↑x, ⋯⟩)

case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ ∀ᶠ (x : X) in 𝓝 ↑x, x ∈ ↑U
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i : ι), LocallyCompactSpace (X i)
g : Z → ContinuousMapGeneratedBy X Y T
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)),
      Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
        match x with
        | (x₁, x₂) => (g (f₁ x₁)) (f₂ x₂)

Tactic:
by
  simp only [continuousGeneratedBy_def, continuous_iff]
  exact forall_congr' (fun i₁ ↦ forall_congr' (fun f₁ ↦
    forall_congr' (fun i₂ ↦ forall_congr' (fun f₂ ↦
      ⟨fun h ↦ ContinuousMap.continuous_uncurry_of_continuous ⟨_, h⟩,
        fun h ↦ (ContinuousMap.curry ⟨_, h⟩).continuous⟩))))

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable x1 x2

Tactic:
← IsInducing.inseparable_iff (productOfMemOpens_isInducing X),

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable ((productOfMemOpens X) x1) ((productOfMemOpens X) x2)
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
⊢ StronglyLocallyContractibleSpace (X × Y)

Tactic:
refine .of_bases (ι := Set X × Set Y)
    (p := fun (x, y) (Ux, Uy) =>
      (Ux ∈ 𝓝 x ∧ ContractibleSpace Ux) ∧ (Uy ∈ 𝓝 y ∧ ContractibleSpace Uy))
    (s := fun _ (Ux, Uy) => Ux ×ˢ Uy) ?_ ?_
  · intro (x, y)
    rw [nhds_prod_eq]
    exact (contractible_basis x).prod (contractible_basis y)
  · intro (x, y) (Ux, Uy) ⟨hUx, hUy⟩
    have : ContractibleSpace Ux := hUx.2
    have : ContractibleSpace Uy := hUy.2
    exact (Homeomorph.Set.prod Ux Uy).contractibleSpace

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

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ (s.sup f) x z ≤ max ((s.sup f) x y) ((s.sup f) y z)

Tactic:
simp_rw [finsetSup_apply hs]

Goal state after:
case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i) x z) ≤ max (s.sup' hs fun i ↦ (f i) x y) (s.sup' hs fun i ↦ (f i) y z)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
⊢ D ⊆ A → IsSeparated (2 * ↑ε) D → D.encard ≤ C.encard

Tactic:
hD_subset

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
⊢ IsSeparated (2 * ↑ε) D → D.encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist t s

Tactic:
exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ s.einfsep = ∞

Tactic:
by
  rw [einfsep_top]
  exact fun _ hx _ hy hxy => (hxy <| hs hx hy).elim

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Tactic:
have h₁ : edist x₁ x₂ ^ (r : ℝ) ≠ 0 :=
    (Ne.symm <| ne_of_lt <| ENNReal.rpow_pos (edist_pos.2 hx) (edist_lt_top x₁ x₂).ne)

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.infsep ≤ (min (edist x y) (edist y x)).toReal

Tactic:
simp_rw [infsep, einfsep_pair_eq_inf hxy]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ {x, y}.infsep = dist x y

Tactic:
rw [infsep_pair_eq_toReal, edist_dist]

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ (ENNReal.ofReal (dist x y)).toReal = dist x y
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
this : TopologicalSpace α := upperSet α
⊢ Topology.IsUpperSet α

Tactic:
exact ⟨rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
this : TopologicalSpace α := lowerSet α
⊢ Topology.IsLowerSet α

Tactic:
exact ⟨rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure[inst✝¹] s = ↑(lowerClosure s)

Tactic:
rw [subset_antisymm_iff]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure[inst✝¹] s ⊆ ↑(lowerClosure s) ∧ ↑(lowerClosure s) ⊆ closure[inst✝¹] s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ U ∈ {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
use a

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

Goal state before:
pp: case mp.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ ∃ a, (Iic a)ᶜ = U

Tactic:
use sSup Uᶜ

Goal state after:
case h
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ (Iic (sSup Uᶜ))ᶜ = U
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
h : PContinuous f
⊢ IsOpen[inst✝¹] f.Dom

Tactic:
← PFun.preimage_univ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst✝¹] (f.preimage Set.univ)
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 ≤ ε₂
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
have : ∀ p q : s, |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ) := fun p q =>
    calc
      |dist p q - dist (Φ p) (Φ q)| ≤ ε₂ := H p q
      _ ≤ 2 * (ε₂ / 2 + δ) := by linarith

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 + δ)
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
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) ≤ ε₁
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
have : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ := by
    refine hausdorffDist_le_of_mem_dist (by linarith) ?_ ?_
    · intro x' hx'
      rcases (Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩
      rw [← xx']
      use Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)
      exact le_of_eq (glueDist_glued_points (fun x : s => (x : X)) Φ (ε₂ / 2 + δ) ⟨x, x_in_s⟩)
    · intro x' hx'
      rcases (Set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩
      rcases mem_range.1 y_in_s' with ⟨x, xy⟩
      use Fl x, mem_image_of_mem _ x.2
      rw [← yx', ← xy, dist_comm]
      exact le_of_eq (glueDist_glued_points (Z := s) Subtype.val Φ (ε₂ / 2 + δ) 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 + δ
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
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
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ 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:
by
    by_cases hW : p₀ ∈ unop W
    · have hV : p₀ ∈ unop V := leOfHom iWV.unop hW
      simp only [dif_pos hW, dif_pos hV, eqToHom_trans]
    · dsimp; rw [dif_neg hW]; apply ((if_neg hW).symm.ndrec terminalIsTerminal).hom_ext

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.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map inc ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc

Tactic:
by
        change dite _ _ _ ≫ _ = _; rw [dif_pos]
        swap
        · exact h.mem_open V.unop.1.2 V.unop.2
        · simp only [Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, unop_op,
            Functor.const_obj_obj, eqToHom_trans, Functor.const_obj_map, Category.comp_id]

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

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : ToType (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
h_eq : (ConcreteCategory.hom (T.app (op V))) s = (ConcreteCategory.hom (𝒢.map ι.op)) t
⊢ ∃ a, (ConcreteCategory.hom ((stalkFunctor C x).map T)) a = (ConcreteCategory.hom (𝒢.germ U x hxU)) t

Tactic:
use ℱ.germ _ x hxV s

Goal state after:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : ToType (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
h_eq : (ConcreteCategory.hom (T.app (op V))) s = (ConcreteCategory.hom (𝒢.map ι.op)) t
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) =
    (ConcreteCategory.hom (𝒢.germ U x hxU)) t
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case refine_1
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
s : PullbackCone sq.f₂₄ sq.f₃₄
⊢ s.pt ≤ sq.X₂ ∧ s.pt ≤ sq.X₃

Tactic:
exact ⟨leOfHom s.fst, leOfHom s.snd⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ ∀ {X_1 : Opens X},
    ∀ R ∈ (grothendieckTopology X) X_1,
      ∀
        (x_1 :
          { obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)), map := fun {X_2 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } },
                map_id := ⋯, map_comp := ⋯ }.obj
            X_1),
        ∃ Y f,
          ∃ (_ : R.arrows f),
            ∃ y,
              (ConcreteCategory.hom
                    ({ obj := fun U ↦ ULift.{u, 0} (PLift (x ∈ U)),
                          map := fun {X_2 Y} f ↦ ↾fun h ↦ { down := { down := ⋯ } }, map_id := ⋯, map_comp := ⋯ }.map
                      f))
                  y =
                x_1

Tactic:
rintro U R hR ⟨⟨hU⟩⟩
    obtain ⟨V, f, hf, hV⟩ := hR x hU
    exact ⟨_, _, hf, ⟨⟨hV⟩⟩, rfl⟩

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

Goal state before:
pp: 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'
j : WalkingParallelPair
⊢ f.hom ≫ (coneEquivFunctorObj F U c').π.app j = (coneEquivFunctorObj F U c).π.app j

Tactic:
cases j

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

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
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ ∀ (j : WalkingParallelPair),
    𝟙 ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).pt ≫
        (SheafConditionEqualizerProducts.fork F U).π.app j =
      ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app j

Tactic:
by
            rintro ⟨⟩
            · simp
              rfl
            · dsimp
              ext
              dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]
              simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
              rw [← F.map_comp]
              rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ ∀ (j : WalkingParallelPair),
    𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
        ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app j =
      (SheafConditionEqualizerProducts.fork F U).π.app j

Tactic:
by
            rintro ⟨⟩
            · simp
              rfl
            · dsimp
              ext
              dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                SheafConditionEqualizerProducts.leftRes]
              simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                Category.assoc]
              rw [← F.map_comp]
              rfl

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → ∃ i', (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id i)

pp: case refine_2
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i' : Set X), x ∈ i' ∧ IsClopen i' → id i' ∈ 𝓝 x

Tactic:
· intro V ⟨hV, h_symm, h_trans⟩
    exact ⟨ball x V, ⟨mem_ball_self _ hV,
      isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity _ hV⟩, le_rfl⟩

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i' : Set X), x ∈ i' ∧ IsClopen i' → id i' ∈ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
u : Set X
hx : x ∈ u
hu : IsClopen u
⊢ id u ∈ 𝓝 x

Tactic:
simp [hu.right.mem_nhds_iff, hx]

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

Goal state before:
pp: case h
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := ⋯
this✝¹ : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := ⋯
Y : (n : ℕ) → AuxGluingStruct (X n) := ⋯
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := ⋯
Z : Type := ⋯
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := ⋯
coeZ : Z0 → UniformSpace.Completion Z0 := ⋯
X2 : ℕ → Set (UniformSpace.Completion Z0) := ⋯
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := ⋯
this✝ : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
this : ∀ (n : ℕ), (NonemptyCompacts.toGHSpace ∘ X3) n = u n
⊢ Tendsto u atTop (𝓝 L.toGHSpace)

Tactic:
apply Filter.Tendsto.congr this

Goal state after:
case h
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := ⋯
this✝¹ : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := ⋯
Y : (n : ℕ) → AuxGluingStruct (X n) := ⋯
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := ⋯
Z : Type := ⋯
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := ⋯
coeZ : Z0 → UniformSpace.Completion Z0 := ⋯
X2 : ℕ → Set (UniformSpace.Completion Z0) := ⋯
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := ⋯
this✝ : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
this : ∀ (n : ℕ), (NonemptyCompacts.toGHSpace ∘ X3) n = u n
⊢ Tendsto (NonemptyCompacts.toGHSpace ∘ X3) atTop (𝓝 L.toGHSpace)