mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
⊢ a ∈ ↑J → ↑(etaFn G origin) a ∈ fJ a

Tactic:
a_in_J

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
a_in_J : a ∈ ↑J
⊢ ↑(etaFn G origin) a ∈ fJ a
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
V_mem : V ∈ 𝓝 0
H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂
o : ↑V := ⟨0, ⋯⟩
⊢ map Subtype.val (comap Subtype.val (𝓝 0)) = map Subtype.val (comap Subtype.val (𝓝 0))

Tactic:
show 0 = (o : E) from rfl,

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
V_mem : V ∈ 𝓝 0
H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂
o : ↑V := ⟨0, ⋯⟩
⊢ map Subtype.val (comap Subtype.val (𝓝 ↑o)) = map Subtype.val (comap Subtype.val (𝓝 ↑o))
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ Metric.ball 0 1
y : EuclideanSpace ℝ (Fin n)
hy : y ∈ Metric.ball 0 1
h :
  (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (ballInclusion n)) { down := ⟨y, hy⟩ }
⊢ { down := ⟨x, hx⟩ } = { down := ⟨y, hy⟩ }

Tactic:
obtain rfl : x = y := by simpa [ballInclusion, disk] using h

Goal state after:
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx hy : x ∈ Metric.ball 0 1
h :
  (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hy⟩ }
⊢ { down := ⟨x, hx⟩ } = { down := ⟨x, hy⟩ }
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (β.μ.app X.A ≫ X.a)) uux = X.str (Ultrafilter.map X.str uux)

Tactic:
Monad.Algebra.assoc

Goal state after:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (β.map X.a ≫ X.a)) uux = X.str (Ultrafilter.map X.str uux)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, _] (⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f ∘ ⇑g)

Tactic:
equiv_symm_comp_continuous_iff

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, tY] (⇑f ∘ ⇑g)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
⊢ IsClosed (cl A)

Tactic:
by
  rw [isClosed_iff]
  intro F hF
  exact cl_cl _ ⟨F, hF, rfl⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J : Finset ι
⊢ ∀ (Q₂ : Finset ι), J ⊆ Q₂ → ⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {↑a (op J)} ⊇ ⇑(π_app C fun x ↦ x ∈ Q₂) ⁻¹' {↑a (op Q₂)}

Tactic:
K

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
⊢ J ⊆ K → ⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {↑a (op J)} ⊇ ⇑(π_app C fun x ↦ x ∈ K) ⁻¹' {↑a (op K)}
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' sphere 0 1 ∪ openCell n i = closedCell n i

Tactic:
openCell,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' sphere 0 1 ∪ ↑(map n i) '' ball 0 1 = closedCell n i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ a ∈ s ∧ (if ↑x a = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) = 1 - e (π C fun x ↦ x ∈ s) a

Tactic:
simp only [hx]

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ a ∈ s ∧ (if false = true then e (π C fun x ↦ x ∈ s) a else 1 - e (π C fun x ↦ x ∈ s) a) = 1 - e (π C fun x ↦ x ∈ s) a
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ (LocallyConstant.evalMonoidHom y) (1 - e (π C fun x ↦ x ∈ s) a) = 0

Tactic:
rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
A : Set X.A
x✝ : X.A
F : Ultrafilter X.A
h1 : F ∈ basic A
h2 : X.str F = x✝
⊢ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

Tactic:
exact ⟨F, h1, le_nhds_of_str_eq _ _ h2⟩

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
⊢ c ∈ {fun x ↦ false}

Tactic:
ext x; exact Bool.eq_false_iff.mpr (fun ht ↦ not_lt_zero (hsC c hc x ht))

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

Goal state before:
pp: case hDA
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
hEC : E ⊆ C
⊢ IsClosed[t] (E ∩ D)

pp: case h
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
hEC : E ⊆ C
⊢ ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
· have : D ⊆ E := by
        rw [← union]
        exact subset_union_left
      rw [inter_eq_right.2 this]
      exact isClosedBase C

Goal state after:
case h
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
hEC : E ⊆ C
⊢ ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
x : X
⊢ x ∈ skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
by
  rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]

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
⊢ Disjoint (interior D) (⋃ n, ⋃ j, closedCell n j)

Tactic:
by
  simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
    iUnion_empty]

Goal state after:
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 ⊆ ⋃₀ {s | s ∈ T ∧ s ⊆ U}
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t

Tactic:
sUnion_eq_biUnion

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

Tactic:
sUnion_eq_biUnion

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
⊢ ⇑f '' K ⊆ ⋃ i ∈ t, i
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case pos
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
suffices ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x by aesop
      exact hfin.inter_of_left A |>.isCompact.exists_mapClusterPt_of_frequently <|
        hx.frequently.mp (by simp)

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃₀ S)

Tactic:
sUnion_eq_biUnion

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃ i ∈ S, i)
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l

Tactic:
simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← ofPred_forall, ← Filter.le_def]

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace] fun x i ↦ ↑x ↑i

Tactic:
rw [continuous_pi_iff]

Goal state after:
ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ ∀ (i : ↑S), Continuous[instTopologicalSpaceSubtype, inst✝ ↑i] fun a ↦ ↑a ↑i
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
a b : HomotopyGroup N X x
p q : ↑(Ω^ N X x)
⊢ (genLoopEquivOfUnique N) (transAt default q p) ≈ ((genLoopEquivOfUnique N) q).trans ((genLoopEquivOfUnique N) p)

Tactic:
simp [genLoopEquivOfUnique_transAt]

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

Goal state before:
pp: case a
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := ⋯
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ ¬2 * ↑ε < edist ↑x ↑y

Tactic:
simp only [not_lt]

Goal state after:
case a
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := fun x ↦ ⟨⋯.choose, ⋯⟩
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
x y : ↑D
hxy : f x = f y
⊢ edist ↑x ↑y ≤ 2 * ↑ε
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ packingNumber ε A = packingNumber (2 * (ε / 2)) A

Tactic:
by ring_nf

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ⨅ d, uncurry edist ↑d

Tactic:
refine eq_of_forall_le_iff fun _ => ?_
  simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep = edist x y

Tactic:
by
  nth_rw 1 [← min_self (edist x y)]
  convert! einfsep_pair_eq_inf hxy using 2
  rw [edist_comm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_
    simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ ediam (⇑toSnowflaking ⁻¹' s) = ediam s ^ α⁻¹

Tactic:
rw [← image_ofSnowflaking_eq_preimage, ediam_image_ofSnowflaking]

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

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[inst✝¹] s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Tactic:
rw [isOpen_iff_isUpperSet_and_scottHausdorff_open (D := D)]
  refine and_congr_right fun h ↦
    ⟨IsScottHausdorff.dirSupInaccOn_of_isOpen (t := scottHausdorff α D),
      fun h' d d₀ d₁ d₂ _ d₃ ha ↦ ?_⟩
  obtain ⟨b, hbd, hbu⟩ := h' d₀ d₁ d₂ d₃ ha
  exact ⟨b, hbd, Subset.trans inter_subset_left (h.Ici_subset hbu)⟩

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: case h
L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x | x (f t a)} = t
⊢ ⋃ i ∈ S, i = ⋃₀ S

Tactic:
sUnion_eq_biUnion

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

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : IsOpen[instTopologicalSpaceSubtype] S
⊢ ∃ a, S = (hull T a)ᶜ

Tactic:
let R := {a : α | (hull T a)ᶜ ⊆ S}

Goal state after:
case mp
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : IsOpen[instTopologicalSpaceSubtype] S
R : Set α := {a | (hull T a)ᶜ ⊆ S}
⊢ ∃ a, S = (hull T a)ᶜ
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact ↔ ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact

Tactic:
constructor
  · intro h x
    have := (forget C X ⋙ stalkFunctor C x).exact_tfae.out 2 1
    exact this.mp inferInstance S h
  intro h
  simp_rw [ShortComplex.exact_iff_isZero_homology] at h
  rw [ShortComplex.exact_iff_isZero_homology, isZero_iff_stalkFunctor_obj_isZero S.homology]
  exact fun x => (h x).of_iso
    (ShortComplex.mapHomologyIso S (forget C X ⋙ stalkFunctor C x)).symm

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

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ ∀ (f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) (x : (X ⊕ Y) × (X ⊕ Y)), f ∈ candidatesB X Y → f x ∈ Icc 0 ↑(maxVar X Y)

Tactic:
rintro f ⟨x1, x2⟩ hf

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : f ∈ candidatesB X Y
⊢ f (x1, x2) ∈ Icc 0 ↑(maxVar X Y)
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: 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')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = fV ⟨x, ⋯⟩
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')
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
wVx : fV ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
wVx

Goal state after:
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
wVx : fV ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
Module: Mathlib.Topology.Sion

Goal state before:
pp: case insert
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
hrec :
  ∀ {X : Set E},
    X.Nonempty →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y) →
            (∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y) →
              (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y) →
                Convex ℝ X → s ⊆ Y → (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
have hb : (b ∈ Y) := hsY (mem_insert b s)
    let X' := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
    rcases Set.eq_empty_or_nonempty X' with X'_e | X'_ne
    · -- When `X'` is empty, we may set `y0 := b`
      use b, hb
      simpa [X', Set.eq_empty_iff_forall_notMem] using X'_e
    -- the nonempty case
    have hX'X : X' ⊆ X := inter_subset_left
    have kX' : IsCompact X' := (hfy b hb).isCompact_inter_preimage_Iic kX t
    have cX' : Convex ℝ X' := hfy' b hb t
    specialize hrec X'_ne kX'
      (fun y hy ↦ LowerSemicontinuousOn.mono (hfy y hy) hX'X)
      (fun y hy ↦ cX'.quasiconvexOn_restrict (hfy' y hy) hX'X)
      (fun x hx' ↦ hfx x (hX'X hx'))
      (fun x hx' ↦ hfx' x (hX'X hx'))
      cX'
    have ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y := by
        /- otherwise, if  infi x ∈ X', supr y ∈ s f x y ≤ t
          then for every t' > t, there is x ∈ X' such that supr y ∈ s f x y ≤ t',
          since x ∈ X' and t ≤ t', we have supr y ∈ insert b s f x y  ≤ t',
          hence infi x ∈ X, supr y ∈ insert b s, f x y ≤ t',
          so that infi x ∈ X, supr y ∈ insert b s, f x y ≤ t. -/
      intro x hx
      obtain ⟨y, hy, h⟩ := ht x hx.1
      rcases hy with rfl | hy
      · simp [h.not_ge hx.2]
      · exact ⟨y, hy, h⟩
    obtain ⟨y1, hy1, hty1⟩ := hrec (by grw [subset_insert b s, hsY]) ht_lt
    refine exists_lt_iInf_of_lt_iInf_of_sup ne_X kX hfy hfy' cY hfx hfx' hb hy1 fun x hx ↦ ?_
    by_cases hx' : x ∈ X'
    · exact (hty1 x hx').trans_le (le_sup_right)
    · apply lt_of_lt_of_le _ (le_sup_left)
      rw [← not_le]
      exact fun h ↦ hx' ⟨hx, h⟩

Goal state after: