mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
x'' : (M''.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor
                    (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
              U))
          (x, x', x'')).1 =
      (m, m', m'').1 ∧
    ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor
                    (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
              U))
          (x, x', x'')).2 =
      (m, m', m'').2
⊢ ∃ U x x' x'', ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''

Tactic:
Prod.ext_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
x'' : (M''.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor
                    (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
              U))
          (x, x', x'')).1 =
      (m, m', m'').1 ∧
    ((ConcreteCategory.hom
                ((((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                  U))
              (x, x', x'')).2.1 =
        (m, m', m'').2.1 ∧
      ((ConcreteCategory.hom
                ((((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                  U))
              (x, x', x'')).2.2 =
        (m, m', m'').2.2
⊢ ∃ U x x' x'', ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  (ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
      (a, x) =
    (r, m)
⊢ ∃ U a x, (ιR cR) a = r ∧ ιM x = m

Tactic:
Prod.ext_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
          (a, x)).1 =
      (r, m).1 ∧
    ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
          (a, x)).2 =
      (r, m).2
⊢ ∃ U a x, (ιR cR) a = r ∧ ιM x = m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
              U))
          (a₁, a₂, x)).1 =
      (r₁, r₂, m).1 ∧
    ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
              U))
          (a₁, a₂, x)).2 =
      (r₁, r₂, m).2
⊢ ∃ U a₁ a₂ x, (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m

Tactic:
Prod.ext_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
              U))
          (a₁, a₂, x)).1 =
      (r₁, r₂, m).1 ∧
    ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                  U))
              (a₁, a₂, x)).2.1 =
        (r₁, r₂, m).2.1 ∧
      ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                  U))
              (a₁, a₂, x)).2.2 =
        (r₁, r₂, m).2.2
⊢ ∃ U a₁ a₂ x, (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x₁ : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x₂ : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
              U))
          (a, x₁, x₂)).1 =
      (r, m₁, m₂).1 ∧
    ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
              U))
          (a, x₁, x₂)).2 =
      (r, m₁, m₂).2
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂

Tactic:
Prod.ext_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x₁ : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x₂ : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
              U))
          (a, x₁, x₂)).1 =
      (r, m₁, m₂).1 ∧
    ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                  U))
              (a, x₁, x₂)).2.1 =
        (r, m₁, m₂).2.1 ∧
      ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                  U))
              (a, x₁, x₂)).2.2 =
        (r, m₁, m₂).2.2
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂
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₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm (τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀)

Tactic:
by
  obtain ⟨τ₁₂₃, rfl⟩ := (conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)).surjective τ₁₂₃
  obtain ⟨τ₀₁₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)).surjective τ₀₁₃
  apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective
  simp [leftAdjointCompNatTrans, ← conjugateEquiv_whiskerLeft _ _ adj₀₁]

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

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

Tactic:
Covers,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ Sieve.pullback f S ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ J Z

Tactic:
← Sieve.pullback_comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ J Z
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ (fun x ↦ x') = ⇑(hom ↑(Fork.IsLimit.lift' t y' hy'))

Tactic:
apply TypeCat.homEquiv.symm.injective

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ⋯
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ (TypeCat.homEquiv.symm fun x ↦ x') = TypeCat.homEquiv.symm ⇑(hom ↑(Fork.IsLimit.lift' t y' hy'))
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h → singleton (pullback.snd g f) h

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ singleton (pullback.snd g f) h → pullbackArrows f (singleton g) h

Tactic:
· rintro ⟨W, _, _, _⟩
    exact singleton.mk

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ singleton (pullback.snd g f) h → pullbackArrows f (singleton g) h
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ Presieve.functorPushforward F R (f' ≫ F.map (g' ≫ f''))

Tactic:
exact ⟨X'', f'', f' ≫ F.map g', h₁, by simp⟩

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

Goal state before:
pp: case refine_1
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 : FirstObj P X
t :
  Arrows.PullbackCompatible P π
    ((equivShrink ((i : I) → P.obj (op (X i)))).symm
      ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x))
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
ext ij
    simpa [firstMap, secondMap] using t ij.1 ij.2

Goal state after:
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
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSheafFor P R

Tactic:
by
  rw [IsSeparatedFor, ← forall_and]
  apply forall_congr'
  intro x
  constructor
  · intro z hx
    exact existsUnique_of_exists_of_unique (z.2 hx) z.1
  · intro h
    refine ⟨?_, ExistsUnique.exists ∘ h⟩
    intro t₁ t₂ ht₁ ht₂
    apply (h _).unique ht₁ ht₂
    exact is_compatible_of_exists_amalgamation x ⟨_, ht₂⟩

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

Goal state before:
pp: case left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
a : S.shape.L
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.left a) =
    E.π.app (WalkingMulticospan.left a)

pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b) =
    E.π.app (WalkingMulticospan.right b)

Tactic:
· apply hP.amalgamate_map

Goal state after:
case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b) =
    E.π.app (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
⊢ ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
obtain ⟨y, hy⟩ := h.2 ⟨x, hx⟩
    rw [Subtype.ext_iff] at hy
    dsimp at hy
    subst hy
    exact ⟨y, fun _ ↦ rfl, fun y' hy' ↦ h.1 (by ext; apply hy')⟩

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

Goal state before:
pp: case h
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
hh :
  (ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x) =
    (ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y)
⊢ x.refine h1.unop = y.refine h2.unop

Tactic:
ext I

Goal state after:
case h
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
hh :
  (ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x) =
    (ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y)
I : (unop W).Arrow
⊢ ↑(x.refine h1.unop) I = ↑(y.refine h2.unop) I
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
⊢ IsIso (toRange p)

Tactic:
have := mono_of_mono_fac (toRange_ι p)
  rw [NatTrans.isIso_iff_isIso_app]
  intro i
  rw [isIso_iff_bijective]
  constructor
  · rw [← mono_iff_injective]
    infer_instance
  · rw [← epi_iff_surjective]
    infer_instance

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

Goal state before:
pp: case e'_2.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i)) ≤
    Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)

Tactic:
· rintro W _ ⟨_, a, _, ⟨i⟩, rfl⟩
    exact ⟨_, _, _, Sieve.ofArrows_mk _ _ i, rfl⟩

Goal state after:
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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
⊢ mk x = mk y

Tactic:
eq_mk_iff_exists

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
⊢ ∃ W h1 h2, x.refine h1 = y.refine h2
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) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map g₁.op)) (x'' g₃ S₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ S₂)

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← comp_apply, Functor.map_comp]

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) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map (i₁ V₁ g₃ S₁).op ≫ F.map g₁.op)) ↑(x (i₂ V₁ g₃ S₁) ⋯) =
    (ConcreteCategory.hom (F.map (i₁ V₂ g₄ S₂).op ≫ F.map g₂.op)) ↑(x (i₂ V₂ g₄ S₂) ⋯)