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

Goal state before:
pp: case refine_1
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ ∀ᶠ (i : C(↑(Icc a b), E) × C(↑(Icc b c), E)) in 𝓝[S] fg, i.1 ⊤ = i.2 ⊥

pp: case refine_2
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)

pp: case refine_3
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)

Tactic:
· exact eventually_nhdsWithin_of_forall (fun _ => id)

Goal state after:
case refine_2
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.fst (𝓝[S] fg) (𝓝 fg.1)

case refine_3
α : 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)
S : Set (C(↑(Icc a b), E) × C(↑(Icc b c), E)) := {fg | fg.1 ⊤ = fg.2 ⊥}
fg : C(↑(Icc a b), E) × C(↑(Icc b c), E)
hfg : fg ∈ S
⊢ Tendsto Prod.snd (𝓝[S] fg) (𝓝 fg.2)
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ ∀ (f : C(X, Y)) (x : X), ∀ V ∈ countableBasis Y, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V

Tactic:
· intro f x V hV hx
      apply hS
      exacts [isOpen_of_mem_countableBasis hV, hx]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a

Tactic:
by
  simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x : X
f : ↑(Ω^ N X x)
g : (N → ↑I) → X
h : g = ⇑f
⊢ { toFun := g, continuous_toFun := ⋯ } ∈ Ω^ N X x

Tactic:
by convert! f.2

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

Goal state before:
pp: case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
· simpa using (p.val (y ∘ Sum.inl)).property (y ∘ Sum.inr) hN

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

Goal state before:
pp: case succ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed (preCantorSet (n + 1))

Tactic:
refine IsClosed.union ?_ ?_

Goal state after:
case succ.refine_1
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x ↦ x / 3) '' preCantorSet n)

case succ.refine_2
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x ↦ (2 + x) / 3) '' preCantorSet n)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ x ∈ Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x ↦ ↑x) ⁻¹' s ↔ x ∈ S.domRestrict '' s

Tactic:
simp only [Homeomorph.preimageImageRestrict, Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk,
    mem_image, mem_preimage, Subtype.exists, exists_and_left, Prod.exists, Prod.mk.injEq,
    exists_and_right, exists_eq_right, Subtype.mk.injEq, exists_prop]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x) ↔
    ∃ x_1 ∈ s, S.domRestrict x_1 = x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ cantorSet
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i ≤ x

Tactic:
apply cantorSet_subset_unitInterval at h_mem

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ Set.Icc 0 1
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i ≤ x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ cantorSet
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
apply cantorSet_subset_unitInterval at h_mem

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ Set.Icc 0 1
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i
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
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ edist (logSizeBallSeq J hJ a c l).point s + edist s t ≤ ↑(logSizeBallSeq J hJ a c l).radius * c

Tactic:
apply le_of_le_of_eq (add_le_add h hst)

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
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
⊢ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c + c = ↑(logSizeBallSeq J hJ a c l).radius * c
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
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ = ⟦transAt i q p⟧

Tactic:
rw [transAt_indep (Classical.arbitrary N) q, ← fromLoop_trans_toLoop]

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p q : ↑(Ω^ N X x)
⊢ (fun x1 x2 ↦ x1 * x2) ⟦p⟧ ⟦q⟧ =
    ⟦fromLoop (Classical.arbitrary N)
        (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ coveringNumber 0 A = A.encard

Tactic:
refine le_antisymm (coveringNumber_le_encard_self A) ?_

Goal state after:
E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ A.encard ≤ coveringNumber 0 A
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ coveringNumber ε A ≤ coveringNumber ε (f '' A)

Tactic:
· simp only [coveringNumber, le_iInf_iff]
    intro C hC_subset hC_cover
    obtain ⟨C', hC'_subset, rfl⟩ : ∃ C', C' ⊆ A ∧ C = C'.image f := by
      have (x : C) : ∃ y ∈ A, f y = x := by simpa using hC_subset x.2
      choose g hg_mem hg using this
      refine ⟨Set.range g, ?_, ?_⟩
      · rwa [Set.range_subset_iff]
      · ext
        simp
        grind
    refine (iInf_le _ C').trans <| (iInf_le _ hC'_subset).trans ?_
    simp only [hf.isCover_image_iff] at hC_cover
    refine (iInf_le _ hC_cover).trans ?_
    rw [InjOn.encard_image]
    exact hf_inj.mono hC'_subset

Goal state after:
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 : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) ≤ diam univ + (diam univ + 1 + diam univ) + diam univ

Tactic:
by
          rw [DΦ, DΨ]
          gcongr

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

Goal state before:
pp: case left.left.right
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) := ⋯
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := ⋯
⊢ ∀ (x y z : X ⊕ Y), dist (f x) (f z) ≤ dist (f x) (f y) + dist (f y) (f z)

Tactic:
exact fun x y z => dist_triangle _ _ _

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

Goal state before:
pp: case e'_5
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
this : IndiscreteTopology ↑X
hne : U ≠ ⊥
⊢ s.arrows = ⊤

Tactic:
rw [Sieve.arrows_eq_top_iff, ← Sieve.id_mem_iff_eq_top]

Goal state after:
case e'_5
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
this : IndiscreteTopology ↑X
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
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
⊢ (skyscraperPresheaf p₀ A).IsSheaf

Tactic:
exact
    (Presheaf.isSheaf_iso_iff (eqToIso <| skyscraperPresheaf_eq_pushforward p₀ A)).mpr <|
      (Sheaf.pushforward_sheaf_of_sheaf _
        (Presheaf.isSheaf_on_punit_of_isTerminal _ (by
          dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · #adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1})))

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

Goal state before:
pp: X : TopCat
p₀ : ↑X
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : Abelian C
inst✝ : HasColimits C
⊢ (Presheaf.stalkFunctor C p₀).Additive

Tactic:
by
  dsimp [Presheaf.stalkFunctor]
  have : ((Functor.whiskeringLeft _ _ C).obj (OpenNhds.inclusion p₀).op).Additive := ⟨by cat_disch⟩
  infer_instance

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
⊢ ∀ (x_1 : ↑(base ⁻¹' ↑U)),
    ∀ᶠ (b : F.EtaleSpace) in 𝓝 ↑x_1,
      ∀ (a : ↑(base ⁻¹' ↑U)),
        ↑a = b →
          WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑a).germ)) =
            WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑x_1).germ))

Tactic:
rintro ⟨g, hg⟩

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
g : F.EtaleSpace
hg : g ∈ base ⁻¹' ↑U
⊢ ∀ᶠ (b : F.EtaleSpace) in 𝓝 ↑⟨g, hg⟩,
    ∀ (a : ↑(base ⁻¹' ↑U)),
      ↑a = b →
        WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑a).germ)) =
          WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑⟨g, hg⟩).germ))
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)
hF_bij : ∀ (x : ↑X), ∃ U, x ∈ U ∧ ∀ (y : ↑X) (hyU : y ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U y hyU))
⊢ IsCoveringMap base

Tactic:
by
  refine fun x ↦ .to_isEvenlyCovered_preimage (I := WithDiscreteTopology (ToType (F.stalk x))) ?_
  use inferInstance
  rcases hF_bij x with ⟨U, hxU, hU_bij⟩
  use U, hxU, U.isOpen, U.isOpen.preimage (continuous_base F), homeomorph U hU_bij x hxU
  simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
U : Opens X
S : Sieve U
hS :
  ∀ (Φ : (pointsGrothendieckTopology X).FullSubcategory) (x : Φ.obj.fiber.obj U),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : X
hx : x ∈ U
V : Opens X
f : V ⟶ U
hf : S.arrows f
hV : x ∈ V
h✝ :
  (ConcreteCategory.hom ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.map f))
      { down := { down := hV } } =
    { down := { down := hx } }
⊢ ∃ U_1 f, S.arrows f ∧ x ∈ U_1

Tactic:
exact ⟨V, f, hf, hV⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
x : X
K : Set X
hK : IsClosed K
hx : x ∉ K
O : Set (X × X)
hOu : O ∈ 𝓤 X
hOo : IsOpen O
hbO : ball x O ⊆ Kᶜ
u3 : SetRel X X
hu3u : u3 ∈ 𝓤 X
left✝ : u3.IsSymm
hu3O✝ : u3 ○ u3 ○ u3 ⊆ O
hu3O : u3 ○ interior u3 ○ u3 ⊆ O
⊢ closure (interior u3) ⊆ O

Tactic:
by
        simp_rw [closure_eq_inter_uniformity, ← comp_assoc]
        exact (iInter₂_subset u3 hu3u).trans hu3O

Goal state after: