mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁵ : Category.{u', v'} J
C : Type u
inst✝⁴ : Category.{v, u} C
D✝ : Type u''
inst✝³ : Category.{v'', u''} D✝
X✝ Y✝ : C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : HasBinaryCoproducts C
F : C ⥤ D
inst✝ : PreservesPullbacksOfInclusions F
X Y Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f coprod.inr) F

Tactic:
by
  apply preservesLimit_of_iso_diagram (K₁ := cospan (f ≫ (coprod.braiding X Y).hom) coprod.inl)
  apply cospanExt (Iso.refl _) (Iso.refl _) (coprod.braiding X Y).symm <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
⊢ ∀ {X' Y' : Type u} (αX : X' ⟶ PUnit.{u + 1}) (αY : Y' ⟶ PUnit.{u + 1})
    (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))

Tactic:
intro _ _ _ _ f hαX hαY
    constructor
    · refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · simp
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾(l), ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm
    · refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · simp
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨↾l, ?_, Types.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ?_⟩
      · ext x
        exact (hl x).symm
      · ext x
        exact hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    m ≫
      Multiequalizer.lift ((unop W).index (F.obj j)) (multiequalizer ((unop W).index (limit F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (limit F)) x ≫ (limit.π F j).app (op x.Y)) ⋯ ≫
        Multiequalizer.ι ((unop W).index (F.obj j)) a

Tactic:
limit.lift_π

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{t, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W)
m : E.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt
hm :
  ∀ (j : K),
    m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = E.π.app j
a : (unop W).shape.L
j : K
⊢ m ≫ Multiequalizer.ι ((unop W).index (limit F)) a ≫ (limit.π F j).app (op a.Y) =
    m ≫
      (Multifork.ofι ((unop W).index (F.obj j)) (multiequalizer ((unop W).index (limit F)))
              (fun x ↦ Multiequalizer.ι ((unop W).index (limit F)) x ≫ (limit.π F j).app (op x.Y)) ⋯).π.app
        (WalkingMulticospan.left a)
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)
m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt
hm : ∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j
k✝ : K
k : (J.Cover (unop X))ᵒᵖ
⊢ (limit.lift (F ⋙ J.diagramFunctor D (unop X)) ((J.diagramFunctor D (unop X)).mapCone (limit.cone F)) ≫
            limit.π (F ⋙ J.diagramFunctor D (unop X)) k✝).app
        k ≫
      colimit.ι ((F ⋙ J.diagramFunctor D (unop X)).flip ⋙ (evaluation K D).obj k✝) k =
    (J.diagramNatTrans (limit.π F k✝) (unop X)).app k ≫ colimit.ι (J.diagram (F.obj k✝) (unop X)) k

Tactic:
limit.lift_π

Goal state after:
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : Cᵒᵖ
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X)
m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt
hm : ∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j
k✝ : K
k : (J.Cover (unop X))ᵒᵖ
⊢ (((J.diagramFunctor D (unop X)).mapCone (limit.cone F)).π.app k✝).app k ≫
      colimit.ι ((F ⋙ J.diagramFunctor D (unop X)).flip ⋙ (evaluation K D).obj k✝) k =
    (J.diagramNatTrans (limit.π F k✝) (unop X)).app k ≫ colimit.ι (J.diagram (F.obj k✝) (unop X)) k
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
rw [H c' _ _ _ (NatTrans.congr_app hα ⟨WalkingPair.left⟩)
        (NatTrans.congr_app hα ⟨WalkingPair.right⟩)]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (const (Discrete WalkingPair)).map f
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (((const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : ↑(M₁.obj Z)),
    (ConcreteCategory.hom (φ.app Z)) ((ConcreteCategory.hom (f.app Z)) x) = (ConcreteCategory.hom (ψ.app Z)) x
X : Cᵒᵖ
r : ↑(R.obj X)
y : ↑(M₂.obj X)
Y : C
p : Y ⟶ Opposite.unop X
x : ↑(M₁.obj (Opposite.op Y))
hx : (ConcreteCategory.hom (f.app (Opposite.op Y))) x = (ConcreteCategory.hom (M₂.map p.op)) y
hφ' :
  ∀ (z : ↑(M₂.obj X)),
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) z) =
      (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app (Opposite.op (Opposite.unop X)))) z)
⊢ (ConcreteCategory.hom (N.presheaf.map p.op)) ((ConcreteCategory.hom (φ.app X)) (r • y)) =
    (ConcreteCategory.hom (N.presheaf.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)

Tactic:
change N.map p.op (φ.app X (r • y)) = N.map p.op (r • φ.app X y)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : ↑(M₁.obj Z)),
    (ConcreteCategory.hom (φ.app Z)) ((ConcreteCategory.hom (f.app Z)) x) = (ConcreteCategory.hom (ψ.app Z)) x
X : Cᵒᵖ
r : ↑(R.obj X)
y : ↑(M₂.obj X)
Y : C
p : Y ⟶ Opposite.unop X
x : ↑(M₁.obj (Opposite.op Y))
hx : (ConcreteCategory.hom (f.app (Opposite.op Y))) x = (ConcreteCategory.hom (M₂.map p.op)) y
hφ' :
  ∀ (z : ↑(M₂.obj X)),
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) z) =
      (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app (Opposite.op (Opposite.unop X)))) z)
⊢ (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app X)) (r • y)) =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasProjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ IsZero X

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasProjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ 𝟙 X = 0
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
M : SheafOfModules R
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf
          ((SheafOfModules.toSheaf R).obj ((𝟭 (SheafOfModules R)).obj M))).symm
      ((toPresheaf R₀).map (𝟙 ((SheafOfModules.forget R ⋙ restrictScalars α).obj M))) =
    (CategoryTheory.sheafificationAdjunction J AddCommGrpCat).counit.app ((SheafOfModules.toSheaf R).obj M)

Tactic:
rw [← Adjunction.homEquiv_symm_id]

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
M : SheafOfModules R
⊢ ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((SheafOfModules.forget R ⋙ restrictScalars α).obj M).presheaf
          ((SheafOfModules.toSheaf R).obj ((𝟭 (SheafOfModules R)).obj M))).symm
      ((toPresheaf R₀).map (𝟙 ((SheafOfModules.forget R ⋙ restrictScalars α).obj M))) =
    ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv
          ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M))
          ((SheafOfModules.toSheaf R).obj M)).symm
      (𝟙 ((sheafToPresheaf J AddCommGrpCat).obj ((SheafOfModules.toSheaf R).obj M)))
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
⊢ projectiveDimension X < ↑n ↔ HasProjectiveDimensionLT X n

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
  · have : projectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩
    simp only [Set.mem_ofPred_eq] at this
    exact this _ h
  · obtain _ | n := n
    · exact ⟨⊥, fun _ _ ↦ hasProjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩
    · exact ⟨n, fun i hi ↦ hasProjectiveDimensionLT_of_ge _ (n + 1) _ (by simpa using hi),
        by simp [ENat.WithBot.lt_add_one_iff]⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

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 α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
h₁ : S ≤ Presheaf.imageSieve α r
h₂ : S ≤ Presheaf.imageSieve φ m
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows :=
  Presieve.FamilyOfElements.restrict h₁ (Presieve.FamilyOfElements.localPreimage (whiskerRight α (forget RingCat)) r)
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows :=
  Presieve.FamilyOfElements.restrict h₂ (Presieve.FamilyOfElements.localPreimage (whiskerRight φ (forget Ab)) m)
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
⊢ SMulCandidate α φ r m

Tactic:
have hm₀ : (m₀.map (whiskerRight φ (forget _))).IsAmalgamation m := by
    rw [Presieve.FamilyOfElements.restrict_map]
    apply Presieve.isAmalgamation_restrict
    apply Presieve.FamilyOfElements.isAmalgamation_map_localPreimage

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 α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
h₁ : S ≤ Presheaf.imageSieve α r
h₂ : S ≤ Presheaf.imageSieve φ m
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows :=
  Presieve.FamilyOfElements.restrict h₁ (Presieve.FamilyOfElements.localPreimage (whiskerRight α (forget RingCat)) r)
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows :=
  Presieve.FamilyOfElements.restrict h₂ (Presieve.FamilyOfElements.localPreimage (whiskerRight φ (forget Ab)) m)
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
⊢ SMulCandidate α φ r m
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝¹ val✝ : J
⊢ Fintype (Bicone.diagram val✝¹ ⟶ Bicone.diagram val✝)

Tactic:
· exact
    { elems := Finset.image BiconeHom.diagram Fintype.elems
      complete := fun f => by
        rcases f with (_ | _ | _ | _ | f)
        simp only [Finset.mem_image]
        use f
        simpa using Fintype.complete _ }

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this✝ : J.IsClosed ⊤
this : ↑⟨J.close S, ⋯⟩ = ↑⟨⊤, this✝⟩
⊢ J.close S = ⊤

Tactic:
exact this

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

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) =
    B.hom

Tactic:
· simp [← Functor.map_comp, B', T]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y ⊤

Tactic:
apply Saturate.top

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ J : Precoverage C
inst✝ : J.Small
S : C
E : J.ZeroHypercover S
⊢ E.Small

Tactic:
by
  have : ZeroHypercover.Small.{w} (ZeroHypercover.restrictIndexOfSmall.{max u v} E) :=
    Small.zeroHypercoverSmall _
  let E' := ZeroHypercover.restrictIndexOfSmall.{w}
    (ZeroHypercover.restrictIndexOfSmall.{max u v} E)
  use E'.I₀, ZeroHypercover.Small.restrictFun _ ∘ ZeroHypercover.Small.restrictFun _
  exact E'.mem₀

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯).op))
      (x g₁ hg₁) =
    (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯).op))
      (x g₂ hg₂)

Tactic:
simp only [c, op_comp, Functor.map_comp, types_comp_apply, eqToHom_op, eqToHom_map]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map c'.pt.hom.op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app left))).op))
        ((ConcreteCategory.hom (eqToHom ⋯)) (x g₁ hg₁))) =
    (ConcreteCategory.hom (ℱ.obj.map c'.pt.hom.op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app right))).op))
        ((ConcreteCategory.hom (eqToHom ⋯)) (x g₂ hg₂)))
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✝ : PreOneHypercover S
E : PreOneHypercover S
F : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i j : __spread✝⁻⁰.I₀
k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2
⊢ (F.p₁ k.2 ≫ F.f i.2) ≫ 𝟙 S = F.p₂ k.2 ≫ F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd

Tactic:
by simp [F.w]

Goal state after:
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
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    f ≫ (sheafifyHomEquivOfIsEquivalence J K G) g

Tactic:
have := IsDenseSubsite.isLocallyFull J K G

Goal state after:
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
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this : G.IsLocallyFull K
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    f ≫ (sheafifyHomEquivOfIsEquivalence J K G) g