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

Goal state before:
pp: X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ { toFun := fun f ↦ X'.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    completionFunctor.map f ≫
      { toFun := fun f ↦ X.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by
        ext x
        dsimp [-Function.comp_apply]
        erw [Completion.extension_map (γ := Y) g.hom.2 f.hom.2]
        rfl

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty

Tactic:
by
  simp_rw [IsCompactSystem.iff_nonempty_iInter]
  refine ⟨fun h C hi h'↦ h C hi (fun n ↦ dissipate_eq_biInter_lt ▸ (h' (n + 1))),
    fun h C hi h' ↦ h C hi ?_⟩
  simp_rw [Set.nonempty_iff_ne_empty] at h' ⊢
  refine fun n g ↦ h' n ?_
  simp_rw [← subset_empty_iff, dissipate] at g ⊢
  exact le_trans (fun x ↦ by simp; grind) g

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
⊢ f ∈ comp Subtype.val M '' F ⁻¹' A

Tactic:
show f = F g by ext; rfl

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
hf : F g ∈ A
⊢ F g ∈ comp Subtype.val M '' F ⁻¹' A
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 : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ K ⊆ ⋃₀ (L '' ↑s)

Tactic:
sUnion_image

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 : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ K ⊆ ⋃ a ∈ ↑s, L a
Module: Mathlib.Topology.ContinuousMap.Sigma

Goal state before:
pp: X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g : C(X, Y i)
i' : ι
g' : C(X, Y i')
h : (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i', g'⟩
⊢ ⟨i, g⟩ = ⟨i', g'⟩

Tactic:
obtain ⟨rfl, hg⟩ : i = i' ∧ ⇑g ≍ ⇑g' :=
      Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h

Goal state after:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h : (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g ↦ (sigmaMk g.fst).comp g.snd) ⟨i, g'⟩
hg : ⇑g ≍ ⇑g'
⊢ ⟨i, g⟩ = ⟨i, g'⟩
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ f a ∈ s

Tactic:
exact ha

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

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y

Tactic:
rw [congr(@edist _ $h_edist x y)] at xy

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∈ Cube.boundary (M ⊕ N) ↔ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
constructor
  · rintro ⟨i | i, hi⟩
    · exact Or.inl ⟨i, hi⟩
    · exact Or.inr ⟨i, hi⟩
  · rintro (⟨m, hm⟩ | ⟨n, hn⟩)
    · exact ⟨Sum.inl m, hm⟩
    · exact ⟨Sum.inr n, hn⟩

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

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

Tactic:
by
  induction n with
  | zero => simp [cantorSequence]
  | succ n ih => rw [cantorSequence_get_succ, ih, Finset.sum_range_succ]; ring

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

Goal state before:
pp: ⊢ Function.LeftInverse (fun y ↦ ⟨ofDigits fun i ↦ bif y i then 2 else 0, ⋯⟩) fun x ↦
    match (motive := ↑cantorSet → ℕ → Bool) x with
    | ⟨x, h⟩ => (cantorToBinary x).get

Tactic:
intro ⟨x, hx⟩
    simp only [Fin.isValue, Subtype.mk.injEq]
    exact ofDigits_cantorToTernary hx

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)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd✝), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
hy✝ : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
y : X
hy : y ∈ U
hy' : Uᶜ ∈ pure y
⊢ False

Tactic:
exact hy' hy

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist x y = dist (inl x) (inl y)

Tactic:
@Sum.dist_eq X Y

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist x y = Sum.dist (inl x) (inl y)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = dist (inr x) (inr y)

Tactic:
@Sum.dist_eq X Y

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = Sum.dist (inr x) (inr y)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ (↑C).encard = coveringNumber ε A

Tactic:
· rw [hC]
    simp_rw [iInf_subtype, iInf_and]
    rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
exact fun _ hx _ hy hxy => (hxy <| hs hx hy).elim

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

Goal state before:
pp: case refine_2
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
⊢ (∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p) → IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)

Tactic:
rintro ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩

Goal state after:
case refine_2
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
⊢ IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.infsep = 0 ↔ s.Subsingleton

Tactic:
rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.einfsep = 0 → s.Subsingleton
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Topology.IsUpperSet Prop

Tactic:
by
  simp [Topology.isUpperSet_iff_nhds, Prop.forall]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ closure[inst✝¹] {a} = Ici a

Tactic:
closure_eq_upperClosure,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(upperClosure {a}) = Ici a
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst✝ : Preorder α
s t : Set α
hs :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
ht :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
ha : a ∈ s ∩ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t

Tactic:
obtain ⟨b₁, hb₁d, hb₁ds⟩ := hs hd₀ hd₁ hd₂ hd₃ ha.1
    obtain ⟨b₂, hb₂d, hb₂dt⟩ := ht hd₀ hd₁ hd₂ hd₃ ha.2
    obtain ⟨c, hcd, hc⟩ := hd₂ b₁ hb₁d b₂ hb₂d
    exact ⟨c, hcd, fun e ⟨hce, hed⟩ ↦ ⟨hb₁ds ⟨hc.1.trans hce, hed⟩, hb₂dt ⟨hc.2.trans hce, hed⟩⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ IsTopologicalBasis (lawsonBasis α)

Tactic:
have lawsonBasis_image2 : lawsonBasis α =
      (image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1)
        (IsLower.lowerBasis (WithLower α)) {U | IsOpen[scott α univ] U}) := by
    rw [lawsonBasis, image2, IsLower.lowerBasis]
    simp_rw [sdiff_eq_compl_inter]
    aesop
  rw [lawsonBasis_image2]
  convert!
    IsTopologicalBasis.inf_induced IsLower.isTopologicalBasis
      (isTopologicalBasis_opens (α := WithScott α)) WithLower.toLower WithScott.toScott
  rw [@topology_eq_lawson α _ _ _, lawson]
  apply (congrArg₂ min _) _
  · let _ := lower α
    exact (@IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩).isInducing.eq_induced
  · let _ := scott α univ
    exact (@IsScott.withScottHomeomorph α _ (scott α univ) ⟨rfl⟩).isInducing.eq_induced

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

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
⊢ ∀ (m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt),
    (∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
        m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j) →
      m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)

Tactic:
m

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
⊢ (∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
      m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j) →
    m = limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case neg
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 ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : N ≤ K n
hN : #↑s = ↑N
this : #↑s = #(Fin N)
E : ↑s ≃ Fin N
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
use s, N, scard, E

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
ε : ℝ := ⋯
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
scard : N ≤ K n
hN : #↑s = ↑N
this : #↑s = #(Fin N)
E : ↑s ≃ Fin N
⊢ p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
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
⊢ x ∈ unop (StructuredArrow.right t).fst

Tactic:
have := (isLocallySurjective_iff_epi S.g).mpr hS.epi_g

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
⊢ x ∈ unop (StructuredArrow.right t).fst
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case zero
X : Type u_1
inst✝ : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ ⊥ ∈ {n | ∀ (i : ℕ), n < ↑i → HasSmallInductiveDimensionLT X i}

Tactic:
· exact fun _ _ ↦ h.mono zero_le

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ : ℕ
γ : Path a b
n : ℕ
ih :
  (t : Fin (n + 1) → ↑I) →
    (concat (⇑γ ∘ t) fun k ↦ γ.subpath (t k.castSucc) (t k.succ)).Homotopy (γ.subpath (t 0) (t (last n)))
t : Fin (n + 1 + 1) → ↑I
⊢ ((concat ((⇑γ ∘ t) ∘ castSucc) fun k ↦ γ.subpath (t k.castSucc.castSucc) (t k.castSucc.succ)).trans
        (γ.subpath (t (last n).castSucc) (t (last n).succ))).Homotopy
    (γ.subpath (t 0) (t (last (n + 1))))

Tactic:
exact trans ((ih (t ∘ castSucc)).hcomp (refl _)) (subpathTransSubpath γ _ _ _)

Goal state after:
Module: Mathlib.Util.SleepHeartbeats

Goal state before:
pp: ⊢ 1 = 1

Tactic:
sleep_heartbeats 1000
  rfl

Goal state after: