mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
j : cell C n
x : X
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
this : x ∈ ↑(skeletonLT C 0) ∩ openCell n j
⊢ False

Tactic:
by
    rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)

Tactic:
have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
⊢ IsCompact A

Tactic:
refine TotallyBounded.isCompact_of_isClosed ?_ closed

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
⊢ TotallyBounded A
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a c : α
E : Type u_2
inst✝² : TopologicalSpace E
x : α
inst✝¹ : Fact (a ≤ x)
inst✝ : Fact (x ≤ c)
f : C(↑(Icc a x), E)
g : C(↑(Icc x c), E)
hb : f ⊤ = g ⊥
hx : x ∈ Icc x c
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩

Tactic:
simpa [concat, IccInclusionRight, IccExtendCM, projIccCM, inclusion, hb]

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

Goal state before:
pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : (x, y) ∈ {(e, e)}
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, 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))))
      (x, y)

Tactic:
replace h := Prod.mk_inj.mp h

Goal state after:
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : x = e ∧ y = e
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, 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))))
      (x, y)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : (x, y) ∈ {(e, e)}
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, y) =
    ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
      (x, y)

Tactic:
replace h := Prod.mk_inj.mp h

Goal state after:
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : x = e ∧ y = e
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, y) =
    ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
      (x, y)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ.left
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1)

pp: case succ.right
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
· -- goal: 1 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 3 / 4 ∈ preCantorSet n
      exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩

Goal state after:
case succ.right
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 3 / 4 ∈ preCantorSet (n + 1)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm b n1 + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False

Tactic:
replace h : ofDigitsTerm a n1 + (3⁻¹ ^ n1 * ofDigits fun i ↦ a (1 + n1 + i)) * (1 / 3) =
      (3⁻¹ ^ n1 * ofDigits fun i ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1 := by
    ring_nf at h
    linarith

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
h :
  ofDigitsTerm a n1 + (3⁻¹ ^ n1 * ofDigits fun i ↦ a (1 + n1 + i)) * (1 / 3) =
    (3⁻¹ ^ n1 * ofDigits fun i ↦ b (1 + n1 + i)) * (1 / 3) + ofDigitsTerm b n1
⊢ False
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
⊢ ∀ s ∈ traverse 𝓝 l, ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
s

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
as l : List α
s : Set (List α)
⊢ s ∈ traverse 𝓝 l → ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))

Tactic:
rw [nhds_cons, Tendsto, Filter.map_prod]; exact le_rfl

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

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ 1 ≤ ↑(maxVar X Y)

Tactic:
exact one_le_maxVar X Y

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

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ ↑(maxVar X Y)

Tactic:
exact one_le_maxVar X Y

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.einfsep < ∞
w✝¹ : α
hx : w✝¹ ∈ s
w✝ : α
hy : w✝ ∈ s
hxy : w✝¹ ≠ w✝
right✝ : edist w✝¹ w✝ < ∞
⊢ s.Nontrivial

Tactic:
exact ⟨_, hx, _, hy, hxy⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
cases nonempty_fintype s

Goal state after:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep

Tactic:
cases nonempty_fintype s

Goal state after:
case intro
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < s.einfsep
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

Tactic:
cases nonempty_fintype s

Goal state after:
case intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set X
⊢ IsBounded (⇑toSnowflaking '' s) ↔ IsBounded s

Tactic:
isBounded_image_toSnowflaking_iff

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set X
⊢ IsBounded s ↔ IsBounded s
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
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
⊢ ∃ y ∈ ↑q, dist (Φ xX) y < diam univ + 1 + diam univ

Tactic:
have : Φ xX ∈ (p : Set _) := Φrange ▸ (mem_range_self _)

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
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
this : Φ xX ∈ ↑p
⊢ ∃ y ∈ ↑q, dist (Φ xX) y < diam univ + 1 + diam univ
Module: Mathlib.Topology.Order.UpperLowerSetTopology

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

Tactic:
continuous_def,

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsOpen[inst✝²] s → IsOpen[inst✝³] (f ⁻¹' s)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

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

Tactic:
continuous_def,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsOpen[inst✝²] s → IsOpen[inst✝³] (f ⁻¹' s)
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ ∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t

Tactic:
apply SetRel.preimage_mono

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
⊢ PContinuous f

Tactic:
s

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
⊢ IsOpen[inst✝] s → IsOpen[inst✝¹] (f.preimage s)
Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology

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

Tactic:
exact lt_asymm hcst hsct

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
⊢ (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj U) then A else ⊤_ C)) ≫
      eqToHom ⋯ =
    eqToHom ⋯ ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc

Tactic:
dif_pos

Goal state after:
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
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc

case hc
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
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)
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
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U))) then eqToHom ⋯
          else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op ⊤)) then A else ⊤_ C)) ≫
          c.ι.app (op (unop U)) =
    c.ι.app U

Tactic:
dif_pos

Goal state after:
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
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ c.ι.app (op (unop U)) = c.ι.app U

case hc
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
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U)))
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case mpr
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 : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ (ConcreteCategory.hom (T.app (op W))) ((ConcreteCategory.hom (ℱ.map hWV.op)) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t

Tactic:
convert! h_eq using 1

Goal state after:
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 : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : CC (𝒢.stalk x) := (ConcreteCategory.hom (𝒢.germ U x hxU)) t
ht_x : t_x = (ConcreteCategory.hom (𝒢.germ U x hxU)) t
V : Opens ↑X
hxV : x ∈ V
s : ToType (ℱ.obj (op V))
hs_x : (ConcreteCategory.hom ((stalkFunctor C x).map T)) ((ConcreteCategory.hom (ℱ.germ V x hxV)) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq :
  (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s) =
    (ConcreteCategory.hom (𝒢.map hWU.op)) t
⊢ (ConcreteCategory.hom (T.app (op W))) ((ConcreteCategory.hom (ℱ.map hWV.op)) s) =
    (ConcreteCategory.hom (𝒢.map hWV.op)) ((ConcreteCategory.hom (T.app (op V))) s)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_1
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 : p.Rep
this : x ∈ ⋃ y ∈ s p, ball y (u n)
y : p.Rep
ys : y ∈ s p
hy : x ∈ ball y (u n)
⊢ ∃ y ∈ s p, dist x y ≤ ε

Tactic:
exact ⟨y, ys, le_trans (le_of_lt hy) u_le_ε⟩

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this : Presheaf.IsLocallySurjective S.g.hom
⊢ x ∈ unop (StructuredArrow.right t).fst

Tactic:
obtain ⟨W, Wle, ⟨t₁, ht₁⟩, hW⟩ := (isLocallySurjective_iff S.g.hom).mp this U s x hx

Goal state after:
X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
⊢ x ∈ unop (StructuredArrow.right t).fst
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op

Tactic:
have h' := h =≫ Pi.π _ (i, j)

Goal state after:
case op.op.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    (Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫
      Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j)
⊢ c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ smallInductiveDimension X < ↑0 ↔ smallInductiveDimension X < ↑0

Tactic:
Nat.cast_zero,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ smallInductiveDimension X < ↑0 ↔ smallInductiveDimension X < 0
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
this✝ : UniformSpace X := ⊤
this : ⊤.HasBasis (fun x ↦ True) fun x ↦ Set.univ
⊢ IsUltraUniformity X

Tactic:
← top_uniformity

Goal state after:
X : Type u_1
this✝ : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun x ↦ True) fun x ↦ Set.univ
⊢ IsUltraUniformity X