mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case succ.zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
hn : (Λ.chainComplexMap (f ≫ g)).f 0 = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f 0
⊢ (Λ.chainComplexMap (f ≫ g)).f (0 + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (0 + 1)

pp: case succ.succ
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
hn : (Λ.chainComplexMap (f ≫ g)).f (n + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (n + 1)
⊢ (Λ.chainComplexMap (f ≫ g)).f (n + 1 + 1) = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f (n + 1 + 1)

Tactic:
all_goals
      dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ (ConcreteCategory.hom (ε (restrictScalars f))) r = f r

Tactic:
let := f.toAlgebra
  dsimp [Adjunction.rightAdjointLaxMonoidal_ε]
  rw [extendRestrictScalarsAdj_homEquiv_apply, extendScalars_η]
  erw [AlgebraTensorModule.rid_tmul]
  rw [RingHom.smul_toAlgebra, mul_one]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.coeq s s')

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Initial ↔ ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁

Tactic:
Functor.initial_iff_of_isCofiltered

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s') ↔
    ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (f₁, f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    (colimit.ι ((curry.obj G).obj x.1) x.2 ≫ colimit.ι (curry.obj G ⋙ colim) x.1) ≫ 𝟙 (colimit (curry.obj G ⋙ colim))

Tactic:
← colimit.w (F := curry.obj G ⋙ colim) (f := f₁),

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (f₁, f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    (colimit.ι ((curry.obj G).obj x.1) x.2 ≫ (curry.obj G ⋙ colim).map f₁ ≫ colimit.ι (curry.obj G ⋙ colim) y.1) ≫
      𝟙 (colimit (curry.obj G ⋙ colim))
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y Y' : D
g : Y ⟶ Y'
f : c'.pt ⟶ Y
j : J
⊢ c.ι.app j ≫
      {
          toFun := fun f ↦
            hc.desc
              { pt := F.1 Y', ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } },
          invFun := fun g ↦
            hc'.desc
              { pt := Y', ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }
        (f ≫ g) =
    c.ι.app j ≫
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op c.pt)).map g))
        ({
            toFun := fun f ↦
              hc.desc
                { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } },
            invFun := fun g ↦
              hc'.desc
                { pt := Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }
          f)

Tactic:
dsimp
    simp only [IsColimit.fac, IsColimit.fac_assoc, partialLeftAdjointHomEquiv_comp,
      F.map_comp, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₁₃ ≫ whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃) G₁₀)

Tactic:
obtain ⟨τ₀₁₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)).surjective τ₀₁₃

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
τ₀₁₃ : F₀₁ ⋙ F₁₃ ⟶ F₀₃
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)) τ₀₁₃) =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)) τ₀₁₃ ≫
        whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃) G₁₀)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (M₁.map φ)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (g.app Y)) ((ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)

Tactic:
naturality_apply,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (M₂.map φ)) ((ConcreteCategory.hom (f.app X)) m₁) ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)]
      (ConcreteCategory.hom (g.app Y)) ((ConcreteCategory.hom (M₃.map φ)) m₃) =
    (ConcreteCategory.hom (M₂.map φ)) ((ModuleCat.Hom.hom (f.app X)) (m₁, m₃).1) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₄.map φ)) ((ModuleCat.Hom.hom (g.app X)) (m₁, m₃).2)
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
f : Y ⟶ X
hf : S ∈ {⊤}
⊢ Sieve.pullback f S ∈ {⊤}

Tactic:
rw [Set.mem_singleton_iff] at hf ⊢
    simp [hf]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
⊢ (fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) ((fun x ↦ x f ⋯) x) = x

Tactic:
ext _ _ ⟨rfl⟩; simp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (Presieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ (generate R).arrows

Tactic:
rintro _ _ ⟨f, hf⟩

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
Y : C
f : Over S
hf : R f.hom
⊢ (generate R).arrows { obj := f, property := hf }.obj.hom
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
⊢ generate (Presieve.map F s) = functorPushforward F (generate s)

Tactic:
ext
  rw [arrows_generate_map_eq_functorPushforward]
  simp [functorPushforward_extend_eq]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, (hom (↾fun f ↦ ↑f)) t = f✝) → S.arrows f✝

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, (hom (↾fun f ↦ ↑f)) t = f✝

Tactic:
· rintro ⟨⟨f, hf⟩, rfl⟩
    exact hf

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, (hom (↾fun f ↦ ↑f)) t = f✝
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
by
  dsimp [IsSheaf]
  simp_rw [isSheaf_pretopology]
  exact
    ⟨fun h X R hR => (isLimit_iff_isSheafFor_presieve P R).2 fun E => h E.unop R hR,
      fun h E X R hR => (isLimit_iff_isSheafFor_presieve P R).1 (h R hR) (op E)⟩

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q : ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
⊢ (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
    x

Tactic:
funext i

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q : ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
i : I
⊢ (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) i =
    x i
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
i : (S.pullback f).Arrow
⊢ ↑((Meq.equiv P (S.pullback f))
          ((ConcreteCategory.hom
              (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
                (fun I ↦ Multiequalizer.ι (S.index P) I.base) ⋯))
            ((Meq.equiv P S).symm x)))
      i =
    ↑(x.pullback f) i

Tactic:
simp only [Meq.equiv_apply, Cover.index_left, ← ConcreteCategory.comp_apply, limit.lift_π,
    Multifork.ofι_pt, Multifork.ofι_π_app, Meq.pullback_apply, pullback_obj]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
i : (S.pullback f).Arrow
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) i.base)) ((Meq.equiv P S).symm x) =
    ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
⊢ ∃! t, x₂.IsAmalgamation t

Tactic:
have he' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm (P₂.map f.op x) = P₁.map f.op (e.symm x) := fun X Y f x ↦
      e.injective (by simp only [Equiv.apply_symm_apply, he])
  let x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
  have hx₁ : x₁.Compatible := fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ fac ↦ e.injective
    (by simp only [he, Equiv.apply_symm_apply, hx₂ g₁ g₂ h₁ h₂ fac, x₁])
  have : ∀ (t₂ : P₂.obj (op X)),
      x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂) := fun t₂ ↦ by
    simp only [FamilyOfElements.IsAmalgamation, x₁,
      ← he', EmbeddingLike.apply_eq_iff_eq]
  refine ⟨e (hP₁.amalgamate x₁ hx₁), ?_, ?_⟩
  · dsimp
    simp only [this, Equiv.symm_apply_apply]
    exact IsSheafFor.isAmalgamation hP₁ hx₁
  · intro t₂ ht₂
    refine e.symm.injective ?_
    simp only [Equiv.symm_apply_apply]
    exact hP₁.isSeparatedFor x₁ _ _ (by simpa only [this] using ht₂)
      (IsSheafFor.isAmalgamation hP₁ hx₁)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) =
        (ConcreteCategory.hom (F.map f.op)) s

Tactic:
intro V

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
V : C
⊢ ∀ ⦃f : V ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) =
        (ConcreteCategory.hom (F.map f.op)) s
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)),
      ((FamilyOfElements.singletonEquiv P f).symm b).Compatible →
        ∃! t, ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x

Tactic:
FamilyOfElements.compatible_singleton_iff,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            (ConcreteCategory.hom (P.map p₁.op)) ((FamilyOfElements.singletonEquiv P f).symm b f ⋯) =
              (ConcreteCategory.hom (P.map p₂.op)) ((FamilyOfElements.singletonEquiv P f).symm b f ⋯)) →
        ∃! t, ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map (i' ≫ i).op)) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)

Tactic:
rw [op_comp, F.map_comp] at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map i.op ≫ F.map i'.op)) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
⊢ ∃! t, s.IsAmalgamation t

Tactic:
have hy : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).Compatible := by
    intro Y f H Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
    apply hs
    apply reassoc_of% comm

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
⊢ ∃! t, s.IsAmalgamation t