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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
⊢ projectiveDimension M = projectiveDimension N

Tactic:
by
  refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot => simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₂ :
  φ.app T.left ≫ (F.leftKanExtensionUnit G₂).app T.left =
    (F.leftKanExtensionUnit G₁).app T.left ≫
      ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
            (φ ≫ F.leftKanExtensionUnit G₂)).app
        (F.obj T.left)
h₁ :
  ∀ (G : C ⥤ E),
    (F.leftKanExtensionUnit G).app T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))).hom =
      colimit.ι (CostructuredArrow.proj F X ⋙ G) T
⊢ φ.app T.left ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T =
    colimit.ι (CostructuredArrow.proj F X ⋙ G₁) T ≫ colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)

Tactic:
ι_colimMap,

Goal state after:
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₂ :
  φ.app T.left ≫ (F.leftKanExtensionUnit G₂).app T.left =
    (F.leftKanExtensionUnit G₁).app T.left ≫
      ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
            (φ ≫ F.leftKanExtensionUnit G₂)).app
        (F.obj T.left)
h₁ :
  ∀ (G : C ⥤ E),
    (F.leftKanExtensionUnit G).app T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))).hom =
      colimit.ι (CostructuredArrow.proj F X ⋙ G) T
⊢ φ.app T.left ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T =
    ((CostructuredArrow.proj F X).whiskerLeft φ).app T ≫ colimit.ι (CostructuredArrow.proj F X ⋙ G₂) T
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows (g ≫ f)

Tactic:
apply S.downward_closed

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
S T : Sieve X
h : S ≤ T
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ S.arrows f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
constructor
  · intro H _ _ _ _ hR
    apply H.isSheafFor
    rw [Sieve.generate_sieve]
    exact J.toGrothendieck.pullback_stable _ (Saturate.of _ _ hR)
  · intro H X S hS
    -- This is the key point of the proof:
    -- We must generalize the induction in the correct way.
    suffices ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f).arrows by
      simpa using this (f := 𝟙 _)
    induction hS with
    | of X S hS =>
      exact fun _ _ => H S hS
    | top =>
      simp [Presieve.isSheafFor_top P]
    | pullback X S hS _ f ih =>
      intro Y f
      rw [← S.pullback_comp]
      exact ih (f ≫ _)
    | transitive X R S hS h H1 H2 =>
      intro Y f
      simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
      choose H1 H1' using H1
      choose H2 H2' using H2
      refine ⟨?_, fun x hx => ?_⟩
      · intro x t₁ t₂ h₁ h₂
        refine (H1 f).ext (fun Z g hg => ?_)
        refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
        simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← op_comp, h₁, h₂]
        simpa only [Sieve.pullback_apply, Category.assoc] using hgg
      let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
        ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
        fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)
      have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible := by
        intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
        rw [hx]
        rw [reassoc_of% h]
      choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) =>
        H2' hg (𝟙 _) (y g) (hy g)
      let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
      have hq : q.Compatible := by
        intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
        apply (H2 h₁ g₁).ext
        intro ZZ gg hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
        · dsimp [y]; congr 1; simp only [Category.assoc, h]
        · simpa [reassoc_of% h] using hgg
        · simpa using hgg
      obtain ⟨t, ht⟩ := H1' f q hq
      refine ⟨t, fun Z g hg => ?_⟩
      refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
      rw [← comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
      on_goal 2 => simpa using hgg
      refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
      rw [← comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
      on_goal 2 => simpa using hggg
      refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
      rw [← comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
      apply hx
      simp

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

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
⊢ S ∈ J.toGrothendieck X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
refine ⟨fun hS ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩

Goal state after:
case refine_1
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
hS : S ∈ J.toGrothendieck X
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

case refine_2
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
x✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ S ∈ J.toGrothendieck X
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
g : X ⟶ Y
h : G.map g = f
⊢ G.map (𝟙 X) ≫ f = G.map g

Tactic:
simpa using h.symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id
  simpa using hh i j k

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: 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

pp: 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

Tactic:
· simpa using (c.w f).symm

Goal state after:
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.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
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
s : Cone (K✝ ⋙ proj K B)
m : s.pt ⟶ ((proj K B).mapCone c✝).pt
fac : ∀ (j : J), m ≫ ((proj K B).mapCone c✝).π.app j = s.π.app j
⊢ K.map m ≫ c✝.pt.hom = (CreatesConnected.raiseCone s).pt.hom

Tactic:
simp [← fac]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: case none
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

pp: case some
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
val✝ : J
⊢ F (some val✝) = F none

Tactic:
exacts [rfl, (H (.init _)).symm]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)

Tactic:
by
      have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
          (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
      simp only [op_id, F.map_id, types_id_apply] at h
      exact h.trans (hx.familyOfElements_apply _ _ _)

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

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P Q : PresheafOfModules R₀
f : P ⟶ Q
⊢ ((isomorphisms (Sheaf J Ab)).inverseImage (presheafToSheaf J Ab)).inverseImage (toPresheaf R₀) f ↔
    (isomorphisms (SheafOfModules R)).inverseImage (sheafification α) f

Tactic:
simp only [inverseImage_iff, isomorphisms.iff,
    ← isIso_iff_of_reflects_iso _ (SheafOfModules.toSheaf.{v} R)]

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
P Q : PresheafOfModules R₀
f : P ⟶ Q
⊢ IsIso ((presheafToSheaf J Ab).map ((toPresheaf R₀).map f)) ↔
    IsIso ((SheafOfModules.toSheaf R).map ((sheafification α).map f))
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Tactic:
ext
  simp

Goal state after:
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 : C✝ ⥤ D
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝⁴ : F.IsContinuous J✝ K
inst✝³ : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝² : Category.{v', u'} C
inst✝¹ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ overMap R f ⊣ overPullback R f

Tactic:
refine pushforwardPushforwardAdj (Over.mapPullbackAdj f) _ _ ?_ ?_
  · ext
    simp [Sheaf.pushforwardOverMapIso]
  · ext
    simp [← Functor.map_comp, ← op_comp, Sheaf.pushforwardOverMapIso]

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
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0))).symm
h' : Abelian.image f ≅ kernel (generatorsOfIsCokernelFree f g H H').π :=
  kernel.mapIso (cokernel.π f) (generatorsOfIsCokernelFree f g H H').π (Iso.refl (free σ)) h ⋯
comp_aux : Abelian.factorThruImage f ≫ h'.hom = kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯
⊢ Epi
    ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv.symm
      ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv (Abelian.factorThruImage f ≫ h'.hom)))

Tactic:
Equiv.symm_apply_apply

Goal state after:
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
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0))).symm
h' : Abelian.image f ≅ kernel (generatorsOfIsCokernelFree f g H H').π :=
  kernel.mapIso (cokernel.π f) (generatorsOfIsCokernelFree f g H H').π (Iso.refl (free σ)) h ⋯
comp_aux : Abelian.factorThruImage f ≫ h'.hom = kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯
⊢ Epi (Abelian.factorThruImage f ≫ h'.hom)
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op ⟨U, hxU⟩) ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op ⟨U, hxU⟩) ≫ f₂

Tactic:
exact ih U hxU

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 u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s) =
    (ConcreteCategory.hom (G.germ U x hx)) ((ConcreteCategory.hom (f.app (op U))) s)

Tactic:
by
  rw [← ConcreteCategory.comp_apply, ← stalkFunctor_map_germ, ConcreteCategory.comp_apply]
  rfl

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
F : Presheaf C X
x : ↑X
⊢ F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)

Tactic:
ext
  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
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
⊢ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes ⋯

Tactic:
ext
  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
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
⊢ F.stalkSpecializes h ≫ (stalkFunctor C x).map f = (stalkFunctor C y).map f ≫ G.stalkSpecializes h

Tactic:
ext
  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 : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
⊢ ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    stalkPushforward C f F y ≫ F.stalkSpecializes h

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
S : Submodule R M
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalAddGroup M
inst✝ : ContinuousSMul R M
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S] fun p ↦ p.1 • p.2

Tactic:
rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]
    exact continuous_quot_mk.comp continuous_smul

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_1
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U : C
a : (R ⋙ forget RingCat).obj U
V₁ : C
b₁ : (M ⋙ forget Ab).obj V₁
V₂ : C
f : V₁ ⟶ V₂
s : C
α : IsFiltered.max U V₁ ⟶ s
β : IsFiltered.max U V₂ ⟶ s
h₁ : leftToMax U V₁ ≫ α = leftToMax U V₂ ≫ β
h₂ : rightToMax U V₁ ≫ α = (f ≫ rightToMax U V₂) ≫ β
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)))
          ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.snd)

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_

Goal state after:
case refine_1
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U : C
a : (R ⋙ forget RingCat).obj U
V₁ : C
b₁ : (M ⋙ forget Ab).obj V₁
V₂ : C
f : V₁ ⟶ V₂
s : C
α : IsFiltered.max U V₁ ⟶ s
β : IsFiltered.max U V₂ ⟶ s
h₁ : leftToMax U V₁ ≫ α = leftToMax U V₂ ≫ β
h₂ : rightToMax U V₁ ≫ α = (f ≫ rightToMax U V₂) ≫ β
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map α))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map β))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)))
          ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.snd)
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_2
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U₁ : C
a₁ : (R ⋙ forget RingCat).obj U₁
U₂ V : C
b : (M ⋙ forget Ab).obj V
f : U₁ ⟶ U₂
s : C
α : IsFiltered.max U₁ V ⟶ s
β : IsFiltered.max U₂ V ⟶ s
h₁ : leftToMax U₁ V ≫ α = (f ≫ leftToMax U₂ V) ≫ β
h₂ : rightToMax U₁ V ≫ α = rightToMax U₂ V ≫ β
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨U₁, a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)))
          ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd)

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_

Goal state after:
case refine_2
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U₁ : C
a₁ : (R ⋙ forget RingCat).obj U₁
U₂ V : C
b : (M ⋙ forget Ab).obj V
f : U₁ ⟶ U₂
s : C
α : IsFiltered.max U₁ V ⟶ s
β : IsFiltered.max U₂ V ⟶ s
h₁ : leftToMax U₁ V ≫ α = (f ≫ leftToMax U₂ V) ≫ β
h₂ : rightToMax U₁ V ≫ α = rightToMax U₂ V ≫ β
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map α))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨U₁, a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map β))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)))
          ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd)