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

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| N.actRight ≫ (ρ_ N.X).inv

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| N.X ◁ η

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| f.hom ▷ Y.X

Tactic:
rightUnitor_inv_naturality

Goal state after:
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (ρ_ (N.X ⊗ Y.X)).inv ≫ N.actRight ▷ 𝟙_ C

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| N.X ◁ η

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| f.hom ▷ Y.X
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str

Tactic:
rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
⊢ M = N

Tactic:
ext i j; exact isEmptyElim j

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
simp only [add_eq_left_addition, ← Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ (f ≫ biprod.lift g h) ≫ biprod.desc (𝟙 Z) (𝟙 Z) = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.desc (𝟙 Z) (𝟙 Z)
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (if h : j = j' then if h_1 : ⋯ ▸ x = y then eqToHom ⋯ else 0 else 0) = (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
split_ifs with h h'

Goal state after:
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : j = j'
h' : ⋯ ▸ x = y
⊢ eqToHom ⋯ = eqToHom ⋯ x y

case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : j = j'
h' : ¬⋯ ▸ x = y
⊢ 0 = eqToHom ⋯ x y

case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : ¬j = j'
⊢ 0 = 0 x y
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
⊢ x✝ ≫ ⋯.choose = ⋯.choose

Tactic:
by
    obtain ⟨li, lj, hli, hlj, fac⟩ := h₃ _ hf
    rw [h₂ (D.src hf) _ li (h₁ (D.src hf)).choose_spec hli,
      h₂ (D.tgt hf) _ lj (h₁ (D.tgt hf)).choose_spec hlj, fac]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
s : ↑J.obj
hs✝ : s ∈ S
k : K
hs : s ∈ ↑(α k)
⊢ s ⟶ ↑(t k)

Tactic:
by exact terminal.from (C := (α k).val) ⟨_, hs⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X K : Type u
f : K → SetCardinalLT κ X
hK : Cardinal.mk K < κ
⊢ HasCardinalLT K κ

Tactic:
hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X K : Type u
f : K → SetCardinalLT κ X
hK : Cardinal.mk K < κ
⊢ Cardinal.mk K < κ
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
ι : Type u
A : ι → HasCardinalLT.Set X κ
hι : Cardinal.mk ι < κ
⊢ HasCardinalLT ι κ

Tactic:
hasCardinalLT_iff_cardinal_mk_lt

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
ι : Type u
A : ι → HasCardinalLT.Set X κ
hι : Cardinal.mk ι < κ
⊢ Cardinal.mk ι < κ
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsDirectedOrder (HasCardinalLT.Set X κ)
⊢ IsFilteredOrEmpty (HasCardinalLT.Set X κ)

Tactic:
exact isFilteredOrEmpty_of_directed_le _

Goal state after:
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)

Tactic:
refine .of_right ?_ (by simp [g₁, g₂]) (.of_hasPullback e k₁)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ IsPullback (g₁ ≫ pullback.fst e k₁) g₂ e (pullback.fst k₂ e ≫ k₁)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ Presieve.singleton (F.effectiveEpiOver B) =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

Tactic:
· funext; ext -- Do we want `Presieve.ext`?
    refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
    rintro ⟨⟩
    simp

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
f : Arrow (Sheaf J A)
⊢ ((inv (sheafificationAdjunction J A).counit).app f.left ≫
        (presheafToSheaf J A).map
          ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk f.hom.hom))) ≫
      (presheafToSheaf J A).map
          ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).p.app (Arrow.mk f.hom.hom)) ≫
        (sheafificationAdjunction J A).counit.app f.right =
    f.hom

Tactic:
simp only [assoc, ← Functor.map_comp_assoc,
      MorphismProperty.FunctorialFactorizationData.fac_app,
      NatIso.isIso_inv_app, IsIso.inv_comp_eq]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
f : Arrow (Sheaf J A)
⊢ (presheafToSheaf J A).map (Arrow.mk f.hom.hom).hom ≫ (sheafificationAdjunction J A).counit.app f.right =
    (sheafificationAdjunction J A).counit.app f.left ≫ f.hom
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u_2
inst✝³ : Category.{v_2, u_2} A
S✝¹ : C
E✝¹ : PreZeroHypercover S✝¹
inst✝² : E✝¹.HasPullbacks
S✝ : C
E✝ : PreZeroHypercover S✝
inst✝¹ : E✝.HasPullbacks
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ A
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)

Tactic:
toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u_2
inst✝³ : Category.{v_2, u_2} A
S✝¹ : C
E✝¹ : PreZeroHypercover S✝¹
inst✝² : E✝¹.HasPullbacks
S✝ : C
E✝ : PreZeroHypercover S✝
inst✝¹ : E✝.HasPullbacks
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ A
⊢ PreOneHypercover.Homotopy (PreOneHypercover.Hom.id E.toPreOneHypercover)
    (PreOneHypercover.Hom.id E.toPreOneHypercover)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))

Tactic:
have : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst _ _) := by
    simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), m] using .of_hasPullback _ _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
q' : Y ⟶ S
f₁' : Y ⟶ X (α j₁)
f₂' : Y ⟶ X (α j₂)
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hq' : q ≫ p = q'
hf₁' : f₁ ≫ p' j₁ = f₁'
hf₂' : f₂ ≫ p' j₂ = f₂'
⊢ pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom q' f₁' f₂' ⋯ ⋯ ≫ (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))

Tactic:
by
  subst hq' hf₁' hf₂'
  simp [mapComp'_eq_mapComp, pullFunctorObjHom]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₂) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₂) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

Tactic:
ext x
    simp [Adjunction.homEquiv, yonedaEquiv_naturality]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₃) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₃) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

Tactic:
ext x
    simp [Adjunction.homEquiv, yonedaEquiv_naturality]

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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₂₄) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₂₄) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv)

Tactic:
ext x
    simp [Adjunction.homEquiv, yonedaEquiv_naturality]

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

Goal state before:
pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₃₄) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv)

Tactic:
ext x
    simp [Adjunction.homEquiv, yonedaEquiv_naturality]

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

Goal state before:
pp: case refine_3.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd)
        ⋯ ≫
      F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op

Tactic:
rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left]

Goal state after:
case refine_3.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m ≫ F.obj.map (WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄).op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y✝ : C
f : Y✝ ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
T : Over X
a : T ⟶ Over.mk f
Y : C
i : ι
b : (Over.forget X).obj T ⟶ Z i
hb : b ≫ g i = (Over.forget X).map a
z : (Over.forget X ⋙ ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber).obj T
hz₁ :
  z ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      T
hz₂ :
  ↑((ConcreteCategory.hom
          ({
                    obj :=
                      ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.over
                        ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd,
                    property := ⋯ }.obj.fiber.map
            a))
        ⟨z, hz₁⟩) =
    ↑⟨y, ⋯⟩
⊢ (ConcreteCategory.hom (Φ.obj.fiber.map (b ≫ g i))) z = y

Tactic:
rwa [hb]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
⊢ Presieve.IsSheaf J F

Tactic:
intro X S hS
  rw [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
  refine ⟨?_, ?_⟩
  · intro x t₁ t₂ ht₁ ht₂
    let 𝒮 (Z : C) : Set (F.obj (.op Z)) :=
      .range (fun (g : { g : Z ⟶ X | S.arrows g }) ↦ x _ g.2) ∪
      .range (fun (g : Z ⟶ X) ↦ F.map g.op t₁) ∪ .range (fun (g : Z ⟶ X) ↦ F.map g.op t₂)
    let Q : Subfunctor F := K.subsheafify 𝒮
    have (Z : C) : _root_.Small.{max u v} (Q.toFunctor.obj (Opposite.op Z)) :=
      small_subsheafify_of_small H _ inferInstance _
    have hQ : Presieve.IsSheaf J Q.toFunctor :=
      h.isSheaf_of_forall_aux _ fun X R hR ↦ isSheafFor_subsheafify _ hR (H _ hR)
    let x' : S.arrows.FamilyOfElements Q.toFunctor :=
      fun Z g hg ↦ ⟨x g hg, .base <| .inl <| .inl ⟨⟨g, hg⟩, rfl⟩⟩
    have ht₁' : t₁ ∈ Q.obj (.op X) := .base (.inl <| .inr ⟨𝟙 _, by simp⟩)
    have ht₂' : t₂ ∈ Q.obj (.op X) := .base (.inr ⟨𝟙 _, by simp⟩)
    have : (⟨t₁, ht₁'⟩ : Q.obj _) = ⟨t₂, ht₂'⟩ :=
      (hQ _ hS).isSeparatedFor x' ⟨_, ht₁'⟩ ⟨_, ht₂'⟩ (.of_mono Q.ι ht₁) (.of_mono Q.ι ht₂)
    simp_all
  · -- Let `x` be a compatible family of elements over `S`. We need to show it glues.
    intro x hx
    -- Let `𝒮` be the family of subsets consisting of the family of elements `x`.
    let 𝒮 (Z : C) := Set.range (fun (g : { g : Z ⟶ X | S.arrows g }) ↦ x _ g.2)
    /- Let `Q` be the smallest `K`-subsheaf of `K` containing `𝒮`. This is `max u v`-small, because
    `𝒮` is `max u v`-small. -/
    let Q : Subfunctor F := K.subsheafify 𝒮
    have (Z : C) : _root_.Small.{max u v} (Q.toFunctor.obj (Opposite.op Z)) :=
      small_subsheafify_of_small H _ inferInstance _
    have hQ : Presieve.IsSheaf J Q.toFunctor :=
      h.isSheaf_of_forall_aux _ fun X R hR ↦ isSheafFor_subsheafify _ hR (H _ hR)
    /- By assumption, `Q` is a `J`-sheaf, so the family of sections `x` glues and gives rise
    to an amalgamation of `x` in `F`. -/
    obtain ⟨t, ht, _⟩ := hQ _ hS (fun Z g hg ↦ ⟨x g hg, .base ⟨⟨g, hg⟩, rfl⟩⟩) (.of_mono Q.ι hx)
    exact ⟨t.val, ht.map Q.ι⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left (h.iso m).inv.hom ≫ h.π m = pullbackπ (h.χ m) h.Ω₀

Tactic:
dsimp only [π]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
⊢ Over.Hom.left (h.iso m).inv.hom ≫ Over.Hom.left (h.iso m).hom.hom ≫ pullbackπ (h.χ m) h.Ω₀ = pullbackπ (h.χ m) h.Ω₀