mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
⊢ ProjRestricts C hJK ∘ ProjRestricts C hKL = ProjRestricts C ⋯

Tactic:
ext x i
  simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]
  simp_all

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
⊢ WellFoundedLT (Products I)

Tactic:
have : (· < · : Products I → _ → _) = (fun l m ↦ List.Lex (· < ·) l.val m.val) := by
    ext; exact lt_iff_lex_lt _ _
  rw [WellFoundedLT, this]
  dsimp [Products]
  rw [(by rfl : (· > · : I → _) = flip (· < ·))]
  infer_instance

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
| hi n hn =>

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
hn : ∀ m ≤ n, ∀ (i : cell C m), ∃ I, cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell m_1 j
i : cell C (n + 1)
⊢ ∃ I, cellFrontier (n + 1) i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j

Tactic:
| hi n hn =>

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
⊢ E ⊆ C

Tactic:
simp_rw [← union, ← union_iUnion_openCell_eq_complex (C := C)]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, openCell n j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (sum_to C ho) = GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho

Tactic:
by
  have : Set.range (sum_to C ho) = _ ∪ _ := Set.Sum.elim_range _ _
  simp_all

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! < Order.succ o
⊢ ord I (↑↑l).head! = o

Tactic:
simp only [Order.lt_succ_iff] at this

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! ≤ o
⊢ ord I (↑↑l).head! = o
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
l : ℕ
hln : ↑l < n
⊢ ∀ (i : cell C l), Disjoint (openCell l i) (openCell m j)

Tactic:
i

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
l : ℕ
hln : ↑l < n
i : cell C l
⊢ Disjoint (openCell l i) (openCell m j)
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
h : α → E := fun t ↦ if t ≤ b then (IccExtendCM f) t else (IccExtendCM g) t
⊢ C(↑(Icc a c), E)

Tactic:
suffices Continuous h from ⟨fun t => h t, by fun_prop⟩

Goal state after:
case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
h : α → E := fun t ↦ if t ≤ b then (IccExtendCM f) t else (IccExtendCM g) t
⊢ Continuous[inst✝⁴, inst✝] h
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ x '' Ici (k + 1) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}

Tactic:
simp only [image_eq_iUnion, mem_Ici, iUnion_ge_eq_iUnion_nat_add _ (k + 1)]

Goal state after:
case refine_2
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ ⋃ i, {x (i + (k + 1))} ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
⊢ 𝓝 atTop = ⨅ x, 𝓟 (Iic (𝓟 (Ici x)))

Tactic:
simp only [atTop, Filter.nhds_iInf, nhds_principal]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y)))).HomotopyRel
    (ContinuousMap.id (X × Y)) {(e, e)}

Tactic:
let G : I × X × Y → X × Y := fun p => (HSpace.eHmul (p.1, p.2.1), HSpace.eHmul (p.1, p.2.2))
    have hG : Continuous G := by fun_prop
    use! ⟨G, hG⟩
    · rintro ⟨x, y⟩
      exact Prod.ext (HSpace.eHmul.1.2 x) (HSpace.eHmul.1.2 y)
    · rintro ⟨x, y⟩
      exact Prod.ext (HSpace.eHmul.1.3 x) (HSpace.eHmul.1.3 y)
    · rintro t ⟨x, y⟩ h
      replace h := Prod.mk_inj.mp h
      exact Prod.ext (HSpace.eHmul.2 t x h.1) (HSpace.eHmul.2 t y h.2)

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

Goal state before:
pp: ⊢ 0 ∈ cantorSet

Tactic:
by simp [cantorSet, zero_mem_preCantorSet]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ 𝓝 as = traverse 𝓝 as

Tactic:
refine nhds_mkOfNhds _ _ ?_ ?_
  · intro l
    induction l with
    | nil => exact le_rfl
    | cons a l ih =>
      suffices List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l by
        simpa only [functor_norm] using! this
      exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih
  · intro l s hs
    rcases (mem_traverse_iff _ _).1 hs with ⟨u, hu, hus⟩
    clear as hs
    have : ∃ v : List (Set α), l.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) v ∧ sequence v ⊆ s := by
      induction hu generalizing s with
      | nil =>
        exists []
        simp only [List.forall₂_nil_left_iff]
        exact ⟨trivial, hus⟩
      | cons ht _ ih =>
        rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩
        rcases ih _ Subset.rfl with ⟨v, hv, hvss⟩
        exact
          ⟨u::v, List.Forall₂.cons hu hv,
            Subset.trans (Set.seq_mono (Set.image_mono hut) hvss) hus⟩
    rcases this with ⟨v, hv, hvs⟩
    have : ∀ᶠ y in traverse 𝓝 l, y ∈ sequence v :=
      mem_traverse _ _ <| hv.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha
    refine Eventually.mono this fun u hu ↦ ?_
    have hu := (List.mem_traverse _ _).1 hu
    have : List.Forall₂ (fun a s => IsOpen s ∧ a ∈ s) u v := by
      refine List.Forall₂.flip ?_
      replace hv := hv.flip
      simp only [List.forall₂_and_left, Function.flip_def] at hv ⊢
      exact ⟨hv.1, hu.flip⟩
    grw [← hvs]
    exact mem_traverse _ _ (this.imp fun a s ⟨hs, ha⟩ => IsOpen.mem_nhds hs ha)

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)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Tactic:
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⟩)

Goal state after:
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)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun x ↦ x.eraseIdx 0) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
by rw [tendsto_cons_iff]; exact tendsto_snd

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x ↦ ↑(insertIdx x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨(↑⟨l, hl⟩).insertIdx (↑i) a, ⋯⟩)

Tactic:
simp only [insertIdx_val]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun x ↦ (↑x.2).insertIdx (↑i) x.1) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (l.insertIdx (↑i) a))
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ infEDist p.1 ↑p.2

Tactic:
refine continuous_of_le_add_edist 2 (by simp) ?_
  rintro ⟨x, s⟩ ⟨y, t⟩
  calc
    infEDist x s ≤ infEDist x t + hausdorffEDist (t : Set α) s :=
      infEDist_le_infEDist_add_hausdorffEDist
    _ ≤ infEDist y t + edist x y + hausdorffEDist (t : Set α) s := by
      gcongr; apply infEDist_le_infEDist_add_edist
    _ = infEDist y t + (edist x y + hausdorffEDist (s : Set α) t) := by
      rw [add_assoc, hausdorffEDist_comm]
    _ ≤ infEDist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = infEDist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]

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

Goal state before:
pp: case h
α : Type u
n✝ : ℕ
inst✝ : MetricSpace α
x : ℕ → α
a : α
n : ℕ
⊢ (fun i ↦ ‖dist a (x i) - dist (x 0) (x i)‖) n ≤ dist a (x 0)

Tactic:
exact abs_dist_sub_le _ _ _

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:
by
  simp only [packingNumber, ENNReal.coe_mul, ENNReal.coe_ofNat, externalCoveringNumber, le_iInf_iff,
    iSup_le_iff]
  intro C hC_cover D hD_subset hD_separated
  -- For each point in D, choose a point in C which is ε-close to it
  let f : D → C := fun x ↦
    ⟨(hC_cover (hD_subset x.2)).choose, (hC_cover (hD_subset x.2)).choose_spec.1⟩
  have hf' (x : D) : edist x.1 (f x) ≤ ε := (hC_cover (hD_subset x.2)).choose_spec.2
  -- `⊢ D.encard ≤ C.encard`
  -- It suffices to prove that `f` is injective
  simp only [← Set.toENat_cardinalMk]
  gcongr
  refine Cardinal.mk_le_of_injective (f := f) fun x y hxy ↦ Subtype.ext ?_
  apply Set.Pairwise.eq hD_separated x.2 y.2
  simp only [not_lt]
  calc
    edist (x : X) y ≤ edist (x : X) (f x) + edist (f x : X) y := edist_triangle ..
    _ ≤ 2 * ε := by
      rw [two_mul]
      gcongr
      · exact hf' x
      · simpa [edist_comm, hxy] using hf' y

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

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

Tactic:
by
  rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩
  exact ⟨_, hx, _, hy, hxy⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ ∀ x_1 ∈ insert x s,
    ∀ y ∈ insert x s, x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y

Tactic:
mem_insert_iff

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 ∈ s →
      ∀ (y : α), y = x ∨ y ∈ s → x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞

Tactic:
simp_rw [infsep, ENNReal.toReal_pos_iff]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : s.Nontrivial
⊢ d ≤ dist x y

Tactic:
exact hs.le_infsep_iff.1 hd x hx y hy hxy

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : ¬s.offDiag.Nonempty
⊢ (if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0) = 0

Tactic:
dif_neg hs

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : ¬s.offDiag.Nonempty
⊢ 0 = 0
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
⊢ ∃ y, (y.Nonempty ∧ IsOpen[inst✝²] y ∧ yᶜ ∈ 𝓝 x) ∧ ∀ x ∈ S, Disjoint x y

Tactic:
rcases t2_separation hyx with ⟨V, W, hVo, hWo, hyV, hxW, hVW⟩

Goal state after:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ ∃ y, (y.Nonempty ∧ IsOpen[inst✝²] y ∧ yᶜ ∈ 𝓝 x) ∧ ∀ x ∈ S, Disjoint x y
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

Goal state after:
case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
this : IsOpen (⋃ a ∈ c.left, Iio a)
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Iio c)
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝 a ⊔ 𝓝ˢ (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Tactic:
nhdsSet_Ioo

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝 a ⊔ 𝓟 (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝 b ⊔ 𝓝ˢ (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
nhdsSet_Ioo

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝 b ⊔ 𝓟 (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
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 + δ
⊢ hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃

Tactic:
rw [← @image_univ _ _ Fr, hausdorffDist_image Ir]

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 + δ
⊢ hausdorffDist (range Φ) univ ≤ ε₃
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case neg.refine_2.e_s.refine_2.a
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
x : ℝ
h : x ∈ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))
⊢ x ≤ 0

Tactic:
simp only [mem_iInter, mem_inter_iff, mem_Iio] at h

Goal state after:
case neg.refine_2.e_s.refine_2.a
X : Type u_1
inst✝ : TopologicalSpace X
h✝ : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
x : ℝ
h : ∀ (i : ℕ), x ∈ range ⇑f ∧ x < 1 / (↑i + 1)
⊢ x ≤ 0
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
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    { base := ↑a, germ := (ConcreteCategory.hom (F.germ U ↑a ⋯)) (surjInv ⋯ g) } ∈
      {g | ∃ (h : g.base ∈ V), g.germ = (ConcreteCategory.hom (F.germ V g.base h)) f}

Tactic:
filter_upwards [W.isOpen.preimage continuous_subtype_val |>.mem_nhds hyW] with z hz

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
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ ∃ (h : ↑z ∈ V), (ConcreteCategory.hom (F.germ U ↑z ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V (↑z) h)) f
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
j✝ : Discrete (ι × ι)
⊢ F.map (leSupr U j✝.as.1).op ≫ F.map ((U j✝.as.1).infLELeft (U j✝.as.2)).op =
    F.map (leSupr U j✝.as.2).op ≫ F.map ((U j✝.as.1).infLERight (U j✝.as.2)).op

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
j✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U j✝.as.1).op ≫ ((U j✝.as.1).infLELeft (U j✝.as.2)).op) =
    F.map (leSupr U j✝.as.2).op ≫ F.map ((U j✝.as.1).infLERight (U j✝.as.2)).op
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
j✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U j✝.as.1).op ≫ ((U j✝.as.1).infLELeft (U j✝.as.2)).op) =
    F.map (leSupr U j✝.as.2).op ≫ F.map ((U j✝.as.1).infLERight (U j✝.as.2)).op

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
j✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U j✝.as.1).op ≫ ((U j✝.as.1).infLELeft (U j✝.as.2)).op) =
    F.map ((leSupr U j✝.as.2).op ≫ ((U j✝.as.1).infLERight (U j✝.as.2)).op)