mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁹ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : HasWeakSheafify J AddCommGrpCat
inst✝⁷ : J.WEqualsLocallyBijective AddCommGrpCat
M✝¹ N P : SheafOfModules R
C' : Type u₁
inst✝⁶ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝⁵ : HasSheafify J' AddCommGrpCat
inst✝⁴ : J'.WEqualsLocallyBijective AddCommGrpCat
M✝ : SheafOfModules R
G✝ : M✝.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝³ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝² : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝¹ : HasBinaryProducts C
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
x✝ : C
⊢ Sieve.ofObjects id x✝ = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
⊢ ⊤ ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ f ≫ g ≫ h = (f ≫ g) ≫ h

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F : Sheaf J A
X Y : C
f : X ⟶ Y
⊢ ∀ {X_1 Y_1 : (Over X)ᵒᵖ} (f_1 : X_1 ⟶ Y_1),
    (((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.map f_1 ≫
        (Iso.refl
            ((((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.obj Y_1)).hom =
      (Iso.refl ((((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y)).obj.obj X_1)).hom ≫
        (F.over X).obj.map f_1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
X : D
x : P.obj X
Y : StructuredArrow X F := Classical.arbitrary (StructuredArrow X F)
⊢ F.colimitTypePrecomp P ((F ⋙ P).ιColimitType Y.right ((ConcreteCategory.hom (P.map Y.hom)) x)) = P.ιColimitType X x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : Simple 0
⊢ 0 ≫ 0 = 𝟙 0 ∧ 0 ≫ 0 = 𝟙 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).op.obj U = U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.OpenNhds

Goal state before:
pp: X : TopCat
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).op.obj U = U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ (map U.inclusion' ⋙ ⋯.functor).obj U = (𝟭 (Opens ↑X)).obj U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) → x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)

Tactic:
rintro ⟨x, hx, rfl⟩
    exact ⟨⟨x, trivial, rfl⟩, hx⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
⊢ (pretopology T).toGrothendieck = grothendieckTopology T

Tactic:
rw [← toPretopology_grothendieckTopology]

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology.toGrothendieck = grothendieckTopology T
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ ∀ (x : single i ⟶ single j), x ∈ if h : i = j then {eqToHom ⋯} else ∅

Tactic:
by rintro ⟨⟩; cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j k l : ι
⊢ ∀ (x : pair i j ⟶ pair k l), x ∈ if h : i = k ∧ j = l then {eqToHom ⋯} else ∅

Tactic:
by rintro ⟨⟩; cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F G : Sheaf C X
h : Opens.IsBasis (Set.range B)
φ : F ⟶ G
hi : ∀ (i : ι), IsIso (φ.hom.app (op (B i)))
this : (inducedFunctor B).IsCoverDense (Opens.grothendieckTopology ↑X)
⊢ IsIso ((inducedFunctor B).op.whiskerLeft φ.hom)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F G : Sheaf C X
h : Opens.IsBasis (Set.range B)
φ : F ⟶ G
hi : ∀ (i : ι), IsIso (φ.hom.app (op (B i)))
this : (inducedFunctor B).IsCoverDense (Opens.grothendieckTopology ↑X)
⊢ ∀ (X_1 : (InducedCategory (Opens ↑X) B)ᵒᵖ), IsIso (((inducedFunctor B).op.whiskerLeft φ.hom).app X_1)
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ({ hom := F.map (eqToHom ⋯), w := ⋯ } ≫ { hom := F.map (eqToHom ⋯), w := ⋯ }).hom =
    (𝟙 (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))).hom

Tactic:
simp [eqToHom_map]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ({ hom := F.map (eqToHom ⋯), w := ⋯ } ≫ { hom := F.map (eqToHom ⋯), w := ⋯ }).hom =
    (𝟙 (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)).hom

Tactic:
simp [eqToHom_map]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
P : M.Presentation
⊢ ((kernel P.generators.π).freeHomEquiv.symm P.relations.s ≫ kernel.ι P.generators.π) ≫ P.generators.π = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁴ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : HasSheafify J AddCommGrpCat
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ✝ : Type u
M N : SheafOfModules R
f : M ⟶ N
inst✝ : IsIso f
σ : M.Presentation
⊢ kernel (σ.generators.π ≫ f) = kernel (σ.generators.ofEpi f).π

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ (parallelPair ((kernel P.generators.π).freeHomEquiv.symm P.relations.s ≫ kernel.ι P.generators.π) 0 ⋙ F).map
        WalkingParallelPairHom.right ≫
      (mapFreeIso F P.generators.I η).symm.hom =
    (mapFreeIso F P.relations.I η).symm.hom ≫ (parallelPair (P.mapRelations F η) 0).map WalkingParallelPairHom.right

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ U i'

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ ((pairwiseToOpensLeCover U).obj (single i')).obj

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ ((pairwiseToOpensLeCover U).obj (single i)).obj

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ U i

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ ((pairwiseToOpensLeCover U).obj (single i)).obj

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ U i

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ U i'

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ ((pairwiseToOpensLeCover U).obj (single i')).obj

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
x✝¹ x✝ : CostructuredArrow (Opens.map f).op (op U)
i : x✝¹ ⟶ x✝
⊢ (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ F).map i ≫ F.germ (unop x✝.1) ((ConcreteCategory.hom f) x) ⋯ =
    F.germ (unop x✝¹.1) ((ConcreteCategory.hom f) x) ⋯ ≫
      ((Functor.const (CostructuredArrow (Opens.map f).op (op U))).obj (F.stalk ((ConcreteCategory.hom f) x))).map i

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
e : Inseparable x y
⊢ F.stalkSpecializes ⋯ ≫ F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
e : Inseparable x y
⊢ F.stalkSpecializes ⋯ ≫ F.stalkSpecializes ⋯ = 𝟙 (F.stalk y)

Tactic:
by simp

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

Goal state before:
pp: case op
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj
        (op ⟨V, m⟩)),
    (ConcreteCategory.hom
            (((forget C).mapCocone
                    (colimit.cocone
                      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
              (op ⟨V, m⟩)))
          s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
intro s e

Goal state after:
case op
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj (op ⟨V, m⟩)
e :
  (ConcreteCategory.hom
        (((forget C).mapCocone
                (colimit.cocone
                  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
          (op ⟨V, m⟩)))
      s =
    t
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ s = t

Tactic:
by
  fapply F.eq_of_locally_eq' fun t : Bool => if t then U₁ else U₂
  · exact fun i => if h : i then eqToHom (if_pos h) ≫ i₁ else eqToHom (if_neg h) ≫ i₂
  · refine le_trans hcover ?_
    rw [sup_le_iff]
    constructor
    · exact le_iSup (fun t : Bool => if t then U₁ else U₂) true
    · exact le_iSup (fun t : Bool => if t then U₁ else U₂) false
  · rintro ⟨_ | _⟩
    any_goals exact h₁
    any_goals exact h₂

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (ConcreteCategory.hom (F.map iWU₁.op)) s = (ConcreteCategory.hom (F.map iWU₂.op)) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t

Tactic:
convert! congr_arg (F.germ _ x hxW) heq using 1

Goal state after:
case e'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (ConcreteCategory.hom (F.map iWU₁.op)) s = (ConcreteCategory.hom (F.map iWU₂.op)) t
e_1✝ : CC ((stalkFunctor C x).obj F) = CC (F.stalk x)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s =
    (ConcreteCategory.hom (F.germ W x hxW)) ((ConcreteCategory.hom (F.map iWU₁.op)) s)

case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq : (ConcreteCategory.hom (F.map iWU₁.op)) s = (ConcreteCategory.hom (F.map iWU₂.op)) t
e_1✝ : CC ((stalkFunctor C x).obj F) = CC (F.stalk x)
⊢ (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t =
    (ConcreteCategory.hom (F.germ W x hxW)) ((ConcreteCategory.hom (F.map iWU₂.op)) t)
Module: Mathlib.Algebra.Category.ModuleCat.Tannaka

Goal state before:
pp: R : Type u
inst✝ : Ring R
x✝ : R
⊢ (fun φ ↦ (ConcreteCategory.hom (φ.hom.app (ModuleCat.of R R))) 1)
      ((fun r ↦
          ObjectProperty.homMk
            { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) r), naturality := ⋯ })
        x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
s : CC ((stalkFunctor C x).obj F)
⊢ ∀ ⦃a₂ : CC ((stalkFunctor C x).obj F)⦄,
    (ConcreteCategory.hom ((stalkFunctor C x).map α)) s = (ConcreteCategory.hom ((stalkFunctor C x).map α)) a₂ → s = a₂

Tactic:
t

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
s t : CC ((stalkFunctor C x).obj F)
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map α)) s = (ConcreteCategory.hom ((stalkFunctor C x).map α)) t → s = t
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
| ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t

Tactic:
t

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
| ∀ x ∈ U,
    ∃ V,
      ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t