mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∀ {X_1 Y : (Opens ↑X)ᵒᵖ ⥤ C} {f g : X_1 ⟶ Y},
    ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map (f + g) =
      ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map f +
        ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map g

Tactic:
cat_disch

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
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      (skyscraperPresheaf p₀ c).map inc

Tactic:
by
    dsimp
    by_cases hV : p₀ ∈ V.unop
    · have hU : p₀ ∈ U.unop := leOfHom inc.unop hV
      split_ifs
      rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]
    · split_ifs
      exact ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext ..

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Presheaf AddCommGrpCat X)
hS : S.Exact
s : ↑(S.X₂.obj (op U))
h : (ConcreteCategory.hom (S.g.app (op U))) s = 0
⊢ ∃ t, (ConcreteCategory.hom (S.f.app (op U))) t = s

Tactic:
dsimp [Presheaf] at S

Goal state after:
X : TopCat
U : Opens ↑X
S : ShortComplex ((Opens ↑X)ᵒᵖ ⥤ AddCommGrpCat)
hS : S.Exact
s : ↑(S.X₂.obj (op U))
h : (ConcreteCategory.hom (S.g.app (op U))) s = 0
⊢ ∃ t, (ConcreteCategory.hom (S.f.app (op U))) t = s
Module: Mathlib.Topology.Sheaves.AddCommGrpCat

Goal state before:
pp: X : TopCat
U V : Opens ↑X
F : Presheaf AddCommGrpCat X
h : V ≤ U
s t : ↑(F.obj (op U))
⊢ (ConcreteCategory.hom (F.map (homOfLE h).op)) (s + t) =
    (ConcreteCategory.hom (F.map (homOfLE h).op)) s + (ConcreteCategory.hom (F.map (homOfLE h).op)) t

Tactic:
cat_disch

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

Goal state before:
pp: 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
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T ↔
    ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
      ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V

Tactic:
refine ⟨fun h _ t x hx ↦ ?_, fun h => ⟨fun s x hx ↦ ?_⟩⟩

Goal state after:
case refine_1
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
T : ℱ ⟶ 𝒢
h : IsLocallySurjective T
x✝ : Opens ↑X
t : ToType (𝒢.obj (op x✝))
x : ↑X
hx : x ∈ x✝
⊢ ∃ V, ∃ (x_1 : V ≤ x✝), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V

case refine_2
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
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
t : ToType (F.obj.obj (op (iSup f)))
ht : IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) t
right✝ :
  ∀ (y : ToType (F.obj.obj (op (iSup f)))),
    (fun s_1 ↦ IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) s_1) y → y = t
le₁ : iSup f ≤ U
le₂ : ∀ i ∈ c, unop (StructuredArrow.right i).fst ≤ iSup f
i : Under g s
hi : i ∈ c
⊢ (StructuredArrow.mk
          (CategoryOfElements.homMk ⟨op U, s⟩
            ((NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).obj
              ⟨op (iSup f), t⟩)
            (homOfLE le₁).op ⋯)).hom ≫
      (NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).map
        (CategoryOfElements.homMk
          (StructuredArrow.mk
              (CategoryOfElements.homMk ⟨op U, s⟩
                ((NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).obj
                  ⟨op (iSup f), t⟩)
                (homOfLE le₁).op ⋯)).right
          (StructuredArrow.right i) (homOfLE ⋯).op ⋯) =
    StructuredArrow.hom i

Tactic:
cat_disch

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

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ Equicontinuous fun x ↦ ⇑↑x

Tactic:
refine equicontinuous_of_continuity_modulus (fun t => 2 * maxVar X Y * t) ?_ _ ?_
    · have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) :=
        tendsto_const_nhds.mul tendsto_id
      simpa using this
    · rintro x y ⟨f, hf⟩
      exact (candidates_lipschitz hf).dist_le_mul _ _

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
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
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
t₆ : Under S.g s :=
  StructuredArrow.mk
    (CategoryOfElements.homMk ⟨op U, s⟩
      ((NatTrans.mapElements (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat))).obj
        ⟨op (iSup f), t₅⟩)
      (homOfLE le).op ⋯)
⊢ StructuredArrow.hom t₆ ≫
      (NatTrans.mapElements (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat))).map
        (CategoryOfElements.homMk (StructuredArrow.right t₆) (StructuredArrow.right t) (homOfLE ⋯).op ⋯) =
    StructuredArrow.hom t

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
x : E
hx : x ∈ X
hx1 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y
hx2 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y'
⊢ ⟨x, hx⟩ ∈ ∅

Tactic:
apply hb.not_ge

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : b < max (f a ↑y) (f a ↑y')
x : E
hx : x ∈ X
hx1 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y
hx2 : ⟨x, hx⟩ ∈ sublevelLeft X f b ↑y'
⊢ max (f a ↑y) (f a ↑y') ≤ b