mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
⊢ ∀ [Epi p], ∃ f', f' ≫ p = f

Tactic:
hp

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
⊢ ∃ f', f' ≫ p = f
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case inr
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
⊢ ∃ c, c • f = g

Tactic:
obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f)

Goal state after:
case inr
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ ∃ c, c • f = g
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
this : IsFiltered J
K : Type u
f : K → CoconePt hc
hK : HasCardinalLT K κ
⊢ ∃ j, ∀ (k : K), f k ≤ j

Tactic:
choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k)

Goal state after:
κ : Cardinal.{u}
inst✝² : Fact κ.IsRegular
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
hF : ∀ (j : J), IsCardinalFiltered (↑(F.obj j)) κ
this : IsFiltered J
K : Type u
f : K → CoconePt hc
hK : HasCardinalLT K κ
j₀ : K → J
x₀ : (k : K) → (fun X ↦ X) ((F ⋙ forget PartOrdEmb).obj (j₀ k))
hx₀ : ∀ (k : K), (ConcreteCategory.hom (c.ι.app (j₀ k))) (x₀ k) = f k
⊢ ∃ j, ∀ (k : K), f k ≤ j
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
h : (ConcreteCategory.hom (F.map (a₁ ≫ d))) x' ≤ (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
| (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'

Tactic:
h₁

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
h : (ConcreteCategory.hom (F.map (a₁ ≫ d))) x' ≤ (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
| (ConcreteCategory.hom (F.map (a₂ ≫ d'))) y'
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case neg
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
i j : X.ι
h : ¬j = i
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i

Tactic:
· simp [h]

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

Goal state before:
pp: case refine_2.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j : J
i : ι
hi : (D i).P j
⊢ ∃ lift,
    (((⨆ i, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
        MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
      lift

Tactic:
exact ⟨φ ⟨i, _, hi⟩, Or.inr (.mk _)⟩

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) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
⊢ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯)

Tactic:
rw [← cancel_epi (g₁ ≫ pullback.snd 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) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
⊢ (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP : Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))
hc : IsLimit c
⊢ Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))

Tactic:
Types.type_equalizer_iff_unique

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
⊢ Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
Types.type_equalizer_iff_unique

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
hc : IsLimit c
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a

Tactic:
intro y h
    apply ha₂ y
    ext
    simpa [mapToEqualizer] using h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))
⊢ Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
Types.type_equalizer_iff_unique

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP : Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯))
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
⊢ ∀ (h₁ : (sieve f f' i).arrows f₁) (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)

Tactic:
h₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
⊢ ∀ (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)
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
x : (fun X ↦ X) (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₁
⊢ (⇑(((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₁₂))
      x =
    (⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₂) ∘
        ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv))
      x

Tactic:
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
x : (fun X ↦ X) (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₁
⊢ (⇑(((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₁₃))
      x =
    (⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₃) ∘
        ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv))
      x

Tactic:
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
x : (fun X ↦ X) (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₂
⊢ (⇑(((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₂₄))
      x =
    (⇑(ConcreteCategory.hom (sq.op.map F.obj).f₂₄) ∘
        ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv))
      x

Tactic:
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
x : (fun X ↦ X) (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).X₃
⊢ (⇑(((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₃₄))
      x =
    (⇑(ConcreteCategory.hom (sq.op.map F.obj).f₃₄) ∘
        ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv))
      x

Tactic:
simp [Adjunction.homEquiv, yonedaEquiv_naturality]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
⊢ ∀ ⦃X_1 Y_1 : (Sieve.pullback g S).arrows.categoryᵒᵖ⦄ (f : X_1 ⟶ Y_1),
    (((Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ).obj (F.obj (op Y))).map f ≫
        match Y_1 with
        | op { obj := Z, property := hZ } =>
          F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left)))))) =
      (match X_1 with
        | op { obj := Z, property := hZ } =>
          F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left)))))) ≫
        ((Sieve.pullback g S).arrows.diagram.op ⋙ G).map f

Tactic:
rintro ⟨Z₁, hZ₁⟩ ⟨Z₂, hZ₂⟩ ⟨⟨f : Z₂ ⟶ Z₁⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ (((Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ).obj (F.obj (op Y))).map (op { hom := f }) ≫
      match op { obj := Z₂, property := hZ₂ } with
      | op { obj := Z, property := hZ } =>
        F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left)))))) =
    (match op { obj := Z₁, property := hZ₁ } with
      | op { obj := Z, property := hZ } =>
        F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left)))))) ≫
      ((Sieve.pullback g S).arrows.diagram.op ⋙ G).map (op { hom := f })
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)
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
⊢ ∀ (i : WalkingPair),
    m ≫ F.obj.map (WalkingPair.casesOn i 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 i sq.f₂₄ sq.f₃₄).op

Tactic:
rintro (_ | _)

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 =
    ⋯.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

case refine_3.right
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.right 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.right sq.f₂₄ sq.f₃₄).op
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun x_1 ↦
          match x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
Z : C
p : Z ⟶ Y
⊢ ∀ (hp : S.arrows (p ≫ g)), (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
hp

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun x_1 ↦
          match x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
Z : C
p : Z ⟶ Y
hp : S.arrows (p ≫ g)
⊢ (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
R : Sieve U
hR : R ∈ ⊥ U
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.flip.obj (op X)).map f)) y = x

Tactic:
obtain rfl : R = ⊤ := by simpa using hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
hR : ⊤ ∈ ⊥ U
⊢ ∃ Y f, ∃ (_ : ⊤.arrows f), ∃ y, (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.flip.obj (op X)).map f)) y = x
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
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
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
let 𝒮 (Z : C) := Set.range (fun (g : { g : Z ⟶ X | S.arrows g }) ↦ x _ g.2)

Goal state after:
case refine_2
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
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
hx : x.Compatible
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) := fun Z ↦ Set.range fun g ↦ x ↑g ⋯
⊢ ∃ t, x.IsAmalgamation t