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

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 : PresheafOfModules R₀
F : SheafOfModules R
g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F)
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm g) =
    ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
      ((toPresheaf R₀).map g)

Tactic:
obtain ⟨f, rfl⟩ := (sheafificationHomEquiv α).surjective g

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 : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f)) =
    ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm
      ((toPresheaf R₀).map ((sheafificationHomEquiv α) f))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

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 : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
⊢ N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) = N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i))

Tactic:
ext; simp [freeHomEquiv_comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.unop

Tactic:
apply +allowSynthFailures preservesColimitsOfShape_unop

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩
  · suffices IsFiltered (StructuredArrow X F)ᵒᵖ from isCofiltered_of_isFiltered_op _
    apply IsFiltered.of_equivalence (structuredArrowOpEquivalence _ _).symm
  · suffices IsCofiltered (CostructuredArrow F.op (op X))ᵒᵖ from isFiltered_of_isCofiltered_op _
    suffices IsCofiltered (StructuredArrow X F)ᵒᵖᵒᵖ from
      IsCofiltered.of_equivalence (structuredArrowOpEquivalence _ _).op
    apply IsCofiltered.of_equivalence (opOpEquivalence _)

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₁ :
  ∀ (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
h₂ : φ.app T.left ≫ (F.lanUnit.app G₂).app T.left = (F.lanUnit.app G₁).app T.left ≫ (F.lan.map φ).app (F.obj T.left)
⊢ ((F.leftKanExtensionUnit G₁).app T.left ≫ (F.leftKanExtension G₁).map T.hom) ≫
      (F.lan.map φ).app X ≫
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    ((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 ≫
        colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)

Tactic:
simp only [Category.assoc] at h₁ ⊢

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.lanUnit.app G₂).app T.left = (F.lanUnit.app G₁).app T.left ≫ (F.lan.map φ).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
⊢ (F.leftKanExtensionUnit G₁).app T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        (F.lan.map φ).app X ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    (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 ≫
          colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂

Tactic:
refine (H1 f).ext (fun Z g hg => ?_)

Goal state after:
case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ (ConcreteCategory.hom (P.map g.op)) t₁ = (ConcreteCategory.hom (P.map g.op)) t₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesLeftKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasLeftKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasLeftKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
x✝ : A
⊢ ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          L.whiskerLeft
              (whiskerRight
                ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
                  (η ≫ L.leftKanExtensionUnit F'))
                G) ≫
            L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F' L).hom).app
      x✝ =
    ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom ≫
            L.whiskerLeft
              ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
                (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G)))).app
      x✝

Tactic:
simp [← G.map_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
T : ↑(K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K (G.obj X)

Tactic:
exact LocallyCoverDense.functorPushforward_functorPullback_mem T

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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map m.op)) a) =
    (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map m.op)) b)

Tactic:
NatTrans.naturality_apply,

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom (G.map m.op)) ((ConcreteCategory.hom (f.app X)) a) =
    (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map m.op)) b)
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom (G.map m.op)) ((ConcreteCategory.hom (f.app X)) a) =
    (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map m.op)) b)

Tactic:
NatTrans.naturality_apply,

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom (G.map m.op)) ((ConcreteCategory.hom (f.app X)) a) =
    (ConcreteCategory.hom (G.map m.op)) ((ConcreteCategory.hom (f.app X)) b)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
⊢ (comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck

Tactic:
have : F.LocallyCoverDense K.toGrothendieck :=
    K.locallyCoverDense_of_map_functorPullback_mem F H

Goal state after:
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
⊢ (comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck
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
B : D✝
inst✝² : IsConnected J
inst✝¹ : HasColimitsOfShape J C
inst✝ : PreservesColimitsOfShape J K
D : J ⥤ StructuredArrow B K
⊢ PreservesColimit D (StructuredArrow.toUnder B K)

Tactic:
have : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B) :=
      inferInstanceAs <| PreservesColimit D (StructuredArrow.proj B K ⋙ K)

Goal state after:
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
B : D✝
inst✝² : IsConnected J
inst✝¹ : HasColimitsOfShape J C
inst✝ : PreservesColimitsOfShape J K
D : J ⥤ StructuredArrow B K
this : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B)
⊢ PreservesColimit D (StructuredArrow.toUnder B K)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ IsLimit (E.multifork G) ≃ IsLimit (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G))

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (E.multicospanIndex G).multicospan ≅ (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Tactic:
exact mem₁ _ _ _ _ _ pullback.condition

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ u ≫ Over.homMk (𝟙 Z) ⋯ = 𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom)))

Tactic:
by ext; simp [u]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ Over.homMk (𝟙 Z) ⋯ ≫ u = 𝟙 (Over.mk (g ≫ U.hom ≫ f))

Tactic:
by ext; simp [u]

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

Goal state before:
pp: case refine_1.of
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve Y
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ (Sieve.overEquiv { left := Z, right := right, hom := s }).symm (Sieve.generate S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }

Tactic:
rw [Sieve.overEquiv_symm_generate]
      exact .of _ _ (by simpa)

Goal state after:
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 s : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a b : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    (Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
          Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
by
    rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩
    obtain ⟨s, α, β, h₁, h₂, h₃⟩ := crown₃
      (leftToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V) (leftToMax U₁ (max U₂ V))
      (rightToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V) (leftToMax U₂ V ≫ rightToMax U₁ (max U₂ V))
      (rightToMax (max U₁ U₂) V) (rightToMax U₂ V ≫ rightToMax U₁ (max U₂ V))
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
    dsimp
    simp only [map_mul, ← ConcreteCategory.comp_apply, ← Functor.map_comp, mul_smul, *]

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)
inst✝³ : HasLimits C
inst✝² : PreservesLimits (forget C)
inst✝¹ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
unop✝ : Opens ↑X
⊢ IsIso (f.hom.app (op unop✝))

Tactic:
apply app_isIso_of_stalkFunctor_map_iso

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

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
use τ.induced e

Goal state after:
case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e.toHomeomorph.symm) (TopologicalSpace.induced (⇑e) τ) = τ
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
val✝ : ↑M.toModuleCat
hm : val✝ ∈ (↑(Hom.hom φ)).ker
⊢ (ConcreteCategory.hom (kerι φ ≫ φ)) ⟨val✝, hm⟩ = (ConcreteCategory.hom 0) ⟨val✝, hm⟩

Tactic:
exact hm

Goal state after: