mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
| TrivSqZeroExt.sndHom R N ∘ₗ ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap

Tactic:
AlgHom.comp_toLinearMap,

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
| TrivSqZeroExt.sndHom R N ∘ₗ (TrivSqZeroExt.map f).toLinearMap ∘ₗ toTrivSqZeroExt.toLinearMap
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} J₁
inst✝² : Category.{v₂, u₂} J₂
inst✝¹ : Category.{v₃, u₃} C
inst✝ : MonoidalCategory C
x✝ : (J₁ ⥤ C) × (J₁ ⥤ C)
⊢ ∀ {X Y : J₁} (f : X ⟶ Y),
    ((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj x✝).map f ≫
        (Iso.refl
            (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj x✝).obj Y)).hom =
      (Iso.refl
            (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj x✝).obj X)).hom ≫
        ((tensor (J₁ ⥤ C)).obj x✝).map f

Tactic:
by simp [tensorHom_def]

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 C
⊢ F.Final ↔
    (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩
  · intro d
    obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty
    exact ⟨_, ⟨f.hom⟩⟩
  · let s₁ : C ≌ AsSmall.{max u₁ v₁ u₂ v₂} C := AsSmall.equiv
    let s₂ : D ≌ AsSmall.{max u₁ v₁ u₂ v₂} D := AsSmall.equiv
    have : IsFilteredOrEmpty (AsSmall.{max u₁ v₁ u₂ v₂} C) := .of_equivalence s₁
    intro d c s s'
    obtain ⟨c', t, ht⟩ := Functor.Final.exists_coeq_of_locally_small (s₁.inverse ⋙ F ⋙ s₂.functor)
      (AsSmall.up.map s) (AsSmall.up.map s')
    exact ⟨AsSmall.down.obj c', AsSmall.down.map t, s₂.functor.map_injective (by simp_all [s₁, s₂])⟩

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (x✝ ⟶ F.obj c)

Tactic:
use Classical.choice IsFiltered.nonempty

Goal state after:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (x✝ ⟶ F.obj (Classical.choice ⋯))
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
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cone (uncurry.obj F) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
h1 :
  (Q p.1).lift ((Cone.postcompose (E p.1).hom).obj (Cone.whisker (Prod.sectR p.1 K) s)) ≫ (D.obj p.1).π.app p.2 =
    ((Cone.postcompose (E p.1).hom).obj (Cone.whisker (Prod.sectR p.1 K) s)).π.app p.2
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p

Tactic:
simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj,
        Cone.postcompose_obj_pt, Cone.whisker_pt, Cone.postcompose_obj_π,
        Cone.whisker_π, NatTrans.comp_app, Functor.const_obj_obj, whiskerLeft_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Category.comp_id, E] at h1

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
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cone (uncurry.obj F) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
h1 :
  (Q p.1).lift
        ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).hom).obj
          (Cone.whisker (Prod.sectR p.1 K) s)) ≫
      (D.obj p.1).π.app p.2 =
    s.π.app (p.1, p.2)
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p
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
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k = limit.π (uncurry.obj F) (j, k)

Tactic:
by
  dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]
  simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ IsIso G.ι → G = ⊤

Tactic:
intro H

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
H : IsIso G.ι
⊢ 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
x✝³ x✝² x✝¹ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : x✝² ⟶ x✝¹
⊢ x✝³ ◁ x✝ ≫ (isoMk (fun X ↦ β_ (x✝³.obj X) (x✝¹.obj X)) ⋯).hom =
    (isoMk (fun X ↦ β_ (x✝³.obj X) (x✝².obj X)) ⋯).hom ≫ x✝ ▷ x✝³

Tactic:
ext : 1
    exact ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl)

Goal state after:
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
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X✝ ⟶ Y✝
x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ x✝¹ ▷ x✝ ≫ (isoMk (fun X ↦ β_ (Y✝.obj X) (x✝.obj X)) ⋯).hom =
    (isoMk (fun X ↦ β_ (X✝.obj X) (x✝.obj X)) ⋯).hom ≫ x✝ ◁ x✝¹

Tactic:
ext : 1
    exact ModuleCat.MonoidalCategory.tensor_ext (fun _ _ ↦ rfl)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ {S | ∃ R ∈ K.coverings X, R ≤ S.arrows} →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∃ R ∈ K.coverings Y, R ≤ S.arrows}) →
          R ∈ {S | ∃ R ∈ K.coverings X, R ≤ S.arrows}

Tactic:
by
    rintro X S ⟨R', hR', RS⟩ R t
    choose t₁ t₂ t₃ using t
    refine ⟨_, K.transitive _ _ hR' fun _ f hf => t₂ (RS _ _ hf), ?_⟩
    rintro Y _ ⟨Z, g, f, hg, hf, rfl⟩
    apply t₃ (RS _ _ hg) _ _ hf

Goal state after:
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
T : Set (GrothendieckTopology C)
⊢ ∀ (X : C), ⊤ ∈ sInf (sieves '' T) X

Tactic:
rintro X S ⟨⟨_, J, hJ, rfl⟩, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X : C
J : GrothendieckTopology C
hJ : J ∈ T
⊢ ⊤ ∈ (fun f ↦ ↑f X) ⟨J.sieves, ⋯⟩
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ ofArrows (W (g ij.fst) ⋯) (p (g ij.fst) ⋯) (p (g ij.fst) ⋯ ij.snd) ∧
    p (g ij.fst) ⋯ ij.snd ≫ g ij.fst = p (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
exact ⟨⟨_⟩, rfl⟩

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g → f = g

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ f = f
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)

Tactic:
intro H

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit S.arrows.cocone)
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows

Tactic:
intro H

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
⊢ ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry →
    ∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩

Tactic:
rintro ⟨Y, g, f, hf, ht, hv⟩
    exact ⟨⟨_, f⟩, hf, ⟨_, g⟩, ht, Sigma.ext rfl (heq_of_eq hv)⟩

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Z : D
u : Z ⟶ F.obj X
⊢ (generate (Presieve.map F s)).arrows u → Presieve.functorPushforward F s u

Tactic:
rintro ⟨_, _, _, ⟨hu⟩, rfl⟩; exact ⟨_, _, _, hu, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ ∀ (a : Presieve.FamilyOfElements P S.arrows),
    a.Compatible →
      ((∃! t, a.IsAmalgamation t) ↔
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a)

Tactic:
intro x _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔
    ∃! x_1, (ConcreteCategory.hom (forkMap P S.arrows)) x_1 = (firstObjEqFamily P S.arrows).toEquiv.symm x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x.sieveExtend f hf

Tactic:
dsimp [FamilyOfElements.sieveExtend]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = (ConcreteCategory.hom (P.map ⋯.choose.op)) (x ⋯.choose ⋯)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ ∀ (a : Presieve.FamilyOfElements P R),
    a.Compatible →
      ((∃! t, a.IsAmalgamation t) ↔
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a)

Tactic:
intro x _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔ ∃! x_1, (ConcreteCategory.hom (forkMap P R)) x_1 = (firstObjEqFamily P R).toEquiv.symm x
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX

Tactic:
intro H

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ (functorPushforward e.functor S).arrows iYX
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ ∃ g, F.map g = f ∧ R.arrows g

Tactic:
use h' ≫ g

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve X
F : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor F S.arrows ↔ Function.Bijective fun g ↦ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g

Tactic:
by
  simp only [IsSheafFor, Function.bijective_iff_existsUnique,
    shrinkFunctor_ι_comp_eq_iff_isAmalgamation, shrinkFunctorHomEquiv.forall_congr_left,
    Subtype.forall]
  exact forall₂_congr fun x hx ↦ by simp [Equiv.existsUnique_congr_right]

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

Goal state before:
pp: 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
⊢ ∀ (a : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π a →
      ((∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = a i) ↔
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm
              ((equivShrink ((j : I) → P.obj (op (X j)))) a))

Tactic:
intro x _

Goal state after:
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, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∃! x_1,
      (ConcreteCategory.hom (forkMap P X π)) x_1 =
        (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
intro x _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤

Tactic:
rw [← arrows_top, ← generate_of_singleton_isSplitEpi (𝟙 X)]
  rw [← isSheafFor_iff_generate]
  apply isSheafFor_singleton_iso

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P ≫ γ)

Tactic:
plusMap_comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P) ≫ J.plusMap γ
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_2
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑x { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι (S.index P) (I.map h1.unop))) ((Meq.equiv P S).symm x)

Tactic:
Meq.equiv_symm_eq_apply

Goal state after:
case e'_2
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑x { Y := I.Y, f := I.f, hf := ⋯ } = ↑x (I.map h1.unop)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_3
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑y { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι (T.index P) (I.map h2.unop))) ((Meq.equiv P T).symm y)

Tactic:
Meq.equiv_symm_eq_apply

Goal state after:
case e'_3
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑y { Y := I.Y, f := I.f, hf := ⋯ } = ↑y (I.map h2.unop)
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
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
V : C
i : V ⟶ unop U
⊢ (G.sieveOfSection s).arrows i

Tactic:
exact G.map i.op hs

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
this : ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
⊢ s ∈ G.obj U

Tactic:
by
    rw [← this]
    exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2

Goal state after: