mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
      homMk (c.π.app Y) ⋯ =
    homMk (c.π.app X) ⋯ ≫ F.map f

Tactic:
apply CommaMorphism.ext

Goal state after:
case left
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        homMk (c.π.app Y) ⋯).left =
    (homMk (c.π.app X) ⋯ ≫ F.map f).left

case right
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        homMk (c.π.app Y) ⋯).right =
    (homMk (c.π.app X) ⋯ ≫ F.map f).right
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ CoverPreserving (J.over Y) (J.over X) (Over.pullback f)

Tactic:
rw [← (Over.mapPullbackAdj f).isCocontinuous_iff_coverPreserving]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ (Over.map f).IsCocontinuous (J.over X) (J.over Y)
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_1
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.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
⊢ (ConcreteCategory.hom (P.map f)) (val Y₁) = val Y₂

Tactic:
let X : CostructuredArrow F Y₁ := Classical.arbitrary _

Goal state after:
case refine_2.refine_1
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.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
X : CostructuredArrow F Y₁ := Classical.arbitrary (CostructuredArrow F Y₁)
⊢ (ConcreteCategory.hom (P.map f)) (val Y₁) = val Y₂
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
X : SheafOfModules S
U : Cᵒᵖ
x : ↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        ((((pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
                      (pushforwardCongr ⋯).hom) ≫
                    pushforwardNatTrans φ α.hom).app
                X).val.app
          U))
      x =
    (ModuleCat.Hom.hom
        (((𝟙 (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))).app X).val.app U))
      x

Tactic:
suffices X.val.presheaf.map (α.inv.app U.unop).op ≫
      X.val.presheaf.map (α.hom.app U.unop).op = 𝟙 _ from congr($this x)

Goal state after:
C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
X : SheafOfModules S
U : Cᵒᵖ
x : ↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U)
⊢ X.val.presheaf.map (α.inv.app (Opposite.unop U)).op ≫ X.val.presheaf.map (α.hom.app (Opposite.unop U)).op =
    𝟙 (X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop U))))
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✝ : Presheaf C X
F' F : Sheaf C X
U : Opens ↑X
h : U = ⊥
⊢ Limits.IsTerminal (F.obj.obj (op U))

Tactic:
convert! F.isTerminalOfEmpty

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)
⊢ ∀ (j : WalkingParallelPair),
    ((Cocone.precompose
                    (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                        ⋯).inv).obj
                (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose
                    (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                        ⋯).inv).obj
                (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
      (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app j

Tactic:
rintro (_ | _)
      <;> simp [Presentation.mapRelations, GeneratingSections.mapFreeHom, ← Functor.map_comp]

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

Goal state before:
pp: case single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
B : StructuredArrow V (pairwiseToOpensLeCover U)
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l).getLast ⋯ = B

Tactic:
rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩

Goal state after:
case single.single
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' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

case single.pair
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')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
B : StructuredArrow V (pairwiseToOpensLeCover U)
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ = B

Tactic:
rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩

Goal state after:
case pair.single
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')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

case pair.pair
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')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.left.single.left.id_single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ s.fst = s.fst ≫ F.presheaf.map (𝟙 (op (ι { down := WalkingPair.left })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.single.left.pair.left.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ s.fst ≫ F.obj.map (homOfLE ⋯).op = s.fst ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.single.left.pair.left.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ s.fst ≫ F.obj.map (homOfLE ⋯).op = s.fst ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ s.snd ≫ F.obj.map (homOfLE ⋯).op = s.fst ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

Goal state after:
case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.snd ≫ F.obj.map (homOfLE ⋯).op = s.fst ≫ F.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.right.single.right.id_single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ s.snd = s.snd ≫ F.presheaf.map (𝟙 (op (ι { down := WalkingPair.right })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.single.right.pair.left.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ s.fst ≫ F.obj.map (homOfLE ⋯).op = s.snd ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.single.right.pair.right.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ s.snd ≫ F.obj.map (homOfLE ⋯).op = s.snd ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.single.right.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ 𝟙 s.pt ≫ s.snd ≫ F.obj.map (homOfLE ⋯).op = s.snd ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.pair.left.pair.left.id_pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ s.fst ≫ F.obj.map (homOfLE ⋯).op =
    (s.fst ≫ F.obj.map (homOfLE ⋯).op) ≫ F.presheaf.map (𝟙 (op (ι { down := WalkingPair.left } ⊓ ι { down := down✝ })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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

Goal state before:
pp: case refine_2.pair.right.pair.right.id_pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
down✝ : WalkingPair
⊢ 𝟙 s.pt ≫ s.snd ≫ F.obj.map (homOfLE ⋯).op =
    (s.snd ≫ F.obj.map (homOfLE ⋯).op) ≫ F.presheaf.map (𝟙 (op (ι { down := WalkingPair.right } ⊓ ι { down := down✝ })))

Tactic:
simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]

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)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
t : CC (G.obj.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₀ :
  (ConcreteCategory.hom ((stalkFunctor C x).map f.hom)) ((ConcreteCategory.hom (F.presheaf.germ V₁ x hxV₁)) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t

Tactic:
rename' hs₀ => hs₁

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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
t : CC (G.obj.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom ((stalkFunctor C x).map f.hom)) ((ConcreteCategory.hom (F.presheaf.germ V₁ x hxV₁)) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) 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
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
x : ↑X
hx : x ∈ U
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))

Tactic:
apply (bijective_iff_isIso_ofHom _).mpr

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
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
x : ↑X
hx : x ∈ U
⊢ IsIso (↾⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom)))
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : ↑(RingCat.FilteredColimits.colimit R)
⊢ ∀ (a : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a • 0 = 0

Tactic:
rintro ⟨U, a⟩
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_
    dsimp
    simp only [map_zero, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
y : ColimitType F
a✝ : Prequotient F
⊢ descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝ * y) = descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝) * descFun F s y

Tactic:
induction y using Quot.inductionOn

Goal state after:
case h.h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : Prequotient F
⊢ descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝¹ * Quot.mk (⇑(colimitSetoid F)) a✝) =
    descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝¹) * descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
N : M₂ ≃L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (↑N ∘SL ↑M).IsInvertible

Tactic:
exact ⟨M.trans N, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
⊢ f ∘SL f.inverse = ContinuousLinearMap.id R M₂

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
⊢ ↑e ∘SL (↑e).inverse = ContinuousLinearMap.id R M₂
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
hf : f.IsInvertible
y : M₂
⊢ f (f.inverse y) = y

Tactic:
rcases hf with ⟨e, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
y : M₂
e : M ≃L[R] M₂
⊢ ↑e ((↑e).inverse y) = y