mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
let fsu := Finset (Set (Ultrafilter X))
  let ssu := Set (Set (Ultrafilter X))
  let ι : fsu → ssu := fun x ↦ ↑x
  let T0 : ssu := { S | ∃ A ∈ F, S = basic A }
  let AA := X.str ⁻¹' {x}
  let T1 := insert AA T0
  let T2 := finiteInterClosure T1
  intro cond
  -- If F contains a closed set A, then x is contained in A.
  have claim1 : ∀ A : Set X, IsClosed A → A ∈ F → x ∈ A := by
    intro A hA h
    by_contra H
    rw [le_nhds_iff] at cond
    specialize cond Aᶜ H hA.isOpen_compl
    rw [Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_notMem] at cond
    contradiction
  -- If A ∈ F, then x ∈ cl A.
  have claim2 : ∀ A : Set X, A ∈ F → x ∈ cl A := by
    intro A hA
    exact claim1 (cl A) (isClosed_cl A) (mem_of_superset hA (subset_cl A))
  -- T0 is closed under intersections.
  have claim3 : ∀ (S1) (_ : S1 ∈ T0) (S2) (_ : S2 ∈ T0), S1 ∩ S2 ∈ T0 := by
    rintro S1 ⟨S1, hS1, rfl⟩ S2 ⟨S2, hS2, rfl⟩
    exact ⟨S1 ∩ S2, inter_mem hS1 hS2, by simp [basic_inter]⟩
  -- For every S ∈ T0, the intersection AA ∩ S is nonempty.
  have claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty := by
    rintro S ⟨S, hS, rfl⟩
    rcases claim2 _ hS with ⟨G, hG, hG2⟩
    exact ⟨G, hG2, hG⟩
  -- Every element of T0 is nonempty.
  have claim5 : ∀ S ∈ T0, Set.Nonempty S := by
    rintro S ⟨S, hS, rfl⟩
    exact ⟨F, hS⟩
  -- Every element of T2 is nonempty.
  have claim6 : ∀ S ∈ T2, Set.Nonempty S := by
    suffices ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q by
      intro S hS
      rcases this _ hS with h | h
      · exact claim5 S h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim4 Q hQ
    intro S hS
    apply finiteInterClosure_insert
    · constructor
      · use Set.univ
        refine ⟨Filter.univ_sets _, ?_⟩
        ext
        refine ⟨?_, by tauto⟩
        · intro
          apply Filter.univ_sets
      · exact claim3
    · exact hS
  -- It suffices to show that the intersection of any finite subset of T1 is nonempty.
  suffices ∀ F : fsu, ↑F ⊆ T1 → (⋂₀ ι F).Nonempty by
    obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
    have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
    have c2 : G.map X.str = X.incl x := by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
    simp [← c1, c2]
  -- Finish...
  intro T hT
  refine claim6 _ (finiteInter_mem (.finiteInterClosure_finiteInter _) _ ?_)
  intro t ht
  exact finiteInterClosure.basic (@hT t ht)

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
⊢ (eval C l) x = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

Tactic:
by
  change LocallyConstant.evalMonoidHom x (l.eval C) = _
  rw [eval, map_list_prod]
  split_ifs with h
  · simp only [List.map_map]
    apply List.prod_eq_one
    simp only [List.mem_map, Function.comp_apply]
    rintro _ ⟨i, hi, rfl⟩
    exact if_pos (h i hi)
  · simp only [List.map_map, List.prod_eq_zero_iff, List.mem_map, Function.comp_apply]
    push Not at h
    convert! h with i
    dsimp [LocallyConstant.evalMonoidHom, e]
    simp only [ite_eq_right_iff, one_ne_zero]

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

Goal state before:
pp: case hi.inl
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
← cellFrontier_union_openCell_eq_closedCell,

Goal state after:
case hi.inl
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ (cellFrontier (n + 1) j ∪ openCell (n + 1) j))
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ (LinearIndependent ℤ fun (p : ↑(range (π C fun x ↦ ord I x < o))) ↦ ↑p) ↔
    LinearIndependent ℤ fun (p : ↑(smaller C o)) ↦ ↑p

Tactic:
← LinearMap.linearIndependent_iff (πs C o)
    (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)),

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent (ι := ↑(range (π C fun x ↦ ord I x < o))) ℤ (⇑(πs C o) ∘ fun p ↦ ↑p) ↔
    LinearIndependent ℤ fun (p : ↑(smaller C o)) ↦ ↑p
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
h : (fun C ↦ decide (a ∈ ↑C)) = fun C ↦ decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (a ∈ ↑⟨C, hC⟩) = true

Tactic:
exact decide_eq_true hh.1

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
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ closedCell m j ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
← cellFrontier_union_openCell_eq_closedCell,

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
⊢ ↑(skeletonLT C n) ∩ (cellFrontier m j ∪ openCell m j) ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
hy : (f ⁻¹' {y}).Finite
⊢ Finite (ConnectedComponents X)

Tactic:
rw [← ENat.card_lt_top]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
hy : (f ⁻¹' {y}).Finite
⊢ ENat.card (ConnectedComponents X) < ⊤
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : 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 ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = g ⟨↑t, ⋯⟩

Tactic:
nth_rewrite 2 [← concat_comp_IccInclusionRight hb]

Goal state after:
α : 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 ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionRight) ⟨↑t, ⋯⟩
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)

Tactic:
by
  simp only [nhds_eq]
  apply lift'_iInf_of_map_univ <;> simp

Goal state after:
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: case inr
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this : ∀ (s : Set ℚ), IsPreconnected s → ∀ x ∈ s, ∀ y ∈ s, x ≠ y → x < y → False
hlt : ¬x < y
⊢ False

Tactic:
apply this s hs y hy x hx H.symm <| H.lt_or_gt.resolve_left hlt

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

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
let l := Nat.findGreatest P (#J - 1)

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ True ∧ sequence [] ⊆ s

Tactic:
exact ⟨trivial, hus⟩

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

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

Tactic:
by
  -- The proof is basically the same as above.
  constructor <;> intro H
  · exact ⟨H.continuous, H.universally_closed _⟩
  · 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: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i f)) (2 * ↑(x✝ i))) fun j ↦ x✝ ↑j) =
    f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))

pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i g)) (2 * ↑(x✝ i) - 1)) fun j ↦ x✝ ↑j) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))

Tactic:
· change f _ = _; congr 1

Goal state after:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i g)) (2 * ↑(x✝ i) - 1)) fun j ↦ x✝ ↑j) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : x ∈ ⇑toSnowflaking ⁻¹' s
y : X
hy : y ∈ ⇑toSnowflaking ⁻¹' s
⊢ dist x y ≤ C ^ α⁻¹

Tactic:
← hC hx hy,

Goal state after:
case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
x : X
hx : x ∈ ⇑toSnowflaking ⁻¹' s
y : X
hy : y ∈ ⇑toSnowflaking ⁻¹' s
⊢ dist x y ≤ dist (toSnowflaking x) (toSnowflaking y) ^ α⁻¹
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

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
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 : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ∈ closure[inst✝³] {b}
⊢ closure[inst✝³] {b} ⊆ closure[inst✝³] (f ⁻¹' {f b})

Tactic:
apply closure_mono

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ∈ closure[inst✝³] {b}
⊢ {b} ⊆ f ⁻¹' {f b}
Module: Mathlib.Topology.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Topology.Order.HullKernel

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

Tactic:
mem_Ici

Goal state after:
α : Type ?u.3
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set ↑T
c : ↑T
hcS : c ∈ S
⊢ OrderDual.ofDual (sInf (Subtype.val '' S)) ≤ ↑c
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case 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))
⊢ 0 ≤ x

Tactic:
rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩

Goal state after:
case 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 : X
h : f x ∈ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))
⊢ 0 ≤ f x
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
⊢ Φ z = y

Tactic:
simp only [Φ, Ψ]

Goal state after:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this : x ∈ ⋃ y ∈ s q, ball y ε
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < Nat.card ↑(s q) := Fin.is_lt ((E q) ⟨y, ys⟩)
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
⊢ ↑((E q).symm (Fin.cast Npq ((E p) z))) = y
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op)

Tactic:
apply isLimit

Goal state after:
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))
hmem :
  { base := ↑y, germ := (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) } ∈
    {g | ∃ (h : g.base ∈ V), g.germ = (ConcreteCategory.hom (F.germ V g.base h)) 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:
simp only [mem_ofPred_eq] at hmem

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))
hmem : ∃ (h : ↑y ∈ V), (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) 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}
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

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

Tactic:
have : Φ z = y := by simp only [Ψ, Φ]; rw [C1, C2, C3]

Goal state after:
case h
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x : q.Rep
this✝ : x ∈ ⋃ y ∈ s q, ball y (u n)
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := ↑((E q) ⟨y, ys⟩)
hi : ↑((E q) ⟨y, ys⟩) < N q := ((E q) ⟨y, ys⟩).isLt
ihi_eq : ⟨i, hi⟩ = (E q) ⟨y, ys⟩
hiq : i < N q
hip : i < N p
z : ↑(s p) := (E p).symm ⟨i, hip⟩
C1 : (E p) z = ⟨i, hip⟩
C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩
C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩
this : Φ z = y
⊢ dist x (Φ z) ≤ ε
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ constructibleTopologySubbasis X ↔ s ∈ constructibleTopologySubbasis X

Tactic:
grind [constructibleTopologySubbasis, isClosed_compl_iff, compl_compl]

Goal state after: