mathlib-initiative/mathlib-tactics huggingface dataset:
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
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
⊢ ∀ (g₁ : Z✝ ⟶ Y₁✝) (g₂ : Z✝ ⟶ Y₂✝) ⦃f₁ : Y₁✝ ⟶ X⦄ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁)
    (h₂ : (generate R).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) (x.sieveExtend f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂.op)) (x.sieveExtend f₂ h₂)

Tactic:
_

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
⊢ ∀ (g₂ : Z✝ ⟶ Y₂✝) ⦃f₁ : Y₁✝ ⟶ X⦄ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁✝ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂.op)) (x.sieveExtend f₂ h₂)
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
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
⊢ ∀ (g₂ : Z✝ ⟶ Y₂✝) ⦃f₁ : Y₁✝ ⟶ X⦄ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁✝ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂.op)) (x.sieveExtend f₂ h₂)

Tactic:
_

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
⊢ ∀ ⦃f₁ : Y₁✝ ⟶ X⦄ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁✝ ≫ f₁ = g₂✝ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂ h₂)
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
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
⊢ ∀ ⦃f₁ : Y₁✝ ⟶ X⦄ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁) (h₂ : (generate R).arrows f₂),
    g₁✝ ≫ f₁ = g₂✝ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂ h₂)

Tactic:
_

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
⊢ ∀ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁✝) (h₂ : (generate R).arrows f₂),
    g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁✝ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂ h₂)
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
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
⊢ ∀ ⦃f₂ : Y₂✝ ⟶ X⦄ (h₁ : (generate R).arrows f₁✝) (h₂ : (generate R).arrows f₂),
    g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁✝ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂ h₂)

Tactic:
_

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
⊢ ∀ (h₁ : (generate R).arrows f₁✝) (h₂ : (generate R).arrows f₂✝),
    g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁✝ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂✝ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (Q.map g₁.op)) ((ConcreteCategory.hom (f.app (op Z₁))) (x f₁ h₁)) =
    (ConcreteCategory.hom (Q.map g₂.op)) ((ConcreteCategory.hom (f.app (op Z₂))) (x f₂ h₂))

Tactic:
rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]

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
| ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible →
    ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
1,

Goal state after:
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
| ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible
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
| ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible

Tactic:
1,

Goal state after:
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
| (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) ((firstObjEqFamily P S.arrows).toEquiv.symm a)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ : C
⊢ ∀ {Z : C} {f : Y✝ ⟶ X},
    Presieve.functorPullback F R.arrows f → ∀ (g : Z ⟶ Y✝), Presieve.functorPullback F R.arrows (g ≫ f)

Tactic:
_

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
⊢ ∀ {f : Y✝ ⟶ X}, Presieve.functorPullback F R.arrows f → ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPullback F R.arrows (g ≫ f)
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
x : Presieve.FamilyOfElements P S.arrows
⊢ x.Compatible →
    ((∃! t, x.IsAmalgamation t) ↔
      ∃! x_1, (ConcreteCategory.hom (forkMap P S.arrows)) x_1 = (firstObjEqFamily P S.arrows).toEquiv.symm x)

Tactic:
_

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.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ : D
⊢ ∀ {Z : D} {f : Y✝ ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z ⟶ Y✝), Presieve.functorPushforward F R.arrows (g ≫ f)

Tactic:
_

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ Z✝ : D
⊢ ∀ {f : Y✝ ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPushforward F R.arrows (g ≫ f)
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 : Sieve X
S : Sieve (F.obj X)
hle : functorPushforward F R ≤ S
⊢ R ≤ functorPullback F S

Tactic:
X

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
⊢ ∀ (f : X ⟶ X✝), R.arrows f → (functorPullback F S).arrows f
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
| ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
    ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
1,

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
a : Presieve.FamilyOfElements P R
| ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible
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
x : Presieve.FamilyOfElements P R
⊢ x.Compatible →
    ((∃! t, x.IsAmalgamation t) ↔
      ∃! x_1, (ConcreteCategory.hom (forkMap P R)) x_1 = (firstObjEqFamily P R).toEquiv.symm x)

Tactic:
_

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: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ uliftYoneda.{w, v₁, u₁}.obj X
Y Z : C
⊢ ∀ {f_1 : Y ⟶ X},
    (∃ t, (hom (f.app (Opposite.op Y))) t = { down := f_1 }) →
      ∀ (g : Z ⟶ Y), ∃ t, (hom (f.app (Opposite.op Z))) t = { down := g ≫ f_1 }

Tactic:
_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝¹ : Y✝ ⟶ X
S R✝ : Sieve X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ uliftYoneda.{w, v₁, u₁}.obj X
Y Z : C
f✝ : Y ⟶ X
⊢ (∃ t, (hom (f.app (Opposite.op Y))) t = { down := f✝ }) →
    ∀ (g : Z ⟶ Y), ∃ t, (hom (f.app (Opposite.op Z))) t = { down := g ≫ f✝ }
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (x : ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}),
      (ConcreteCategory.hom (b.app a✝)) (shrinkYonedaObjObjEquiv ↑x) =
        (ConcreteCategory.hom (a.app a✝)) ⟨shrinkYonedaObjObjEquiv ↑x, ⋯⟩) ↔
    ∀ (x : { g // S.arrows g }), (ConcreteCategory.hom (b.app a✝)) ↑x = (ConcreteCategory.hom (a.app a✝)) x

Tactic:
simp only [Subtype.forall, shrinkYonedaObjObjEquiv.forall_congr_left, Equiv.apply_symm_apply]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (b_1 : unop a✝ ⟶ X) (b_2 : shrinkYonedaObjObjEquiv.symm b_1 ∈ {f | S.arrows (shrinkYonedaObjObjEquiv f)}),
      (ConcreteCategory.hom (b.app a✝)) b_1 = (ConcreteCategory.hom (a.app a✝)) ⟨b_1, ⋯⟩) ↔
    ∀ (a_1 : unop a✝ ⟶ X) (b_1 : S.arrows a_1),
      (ConcreteCategory.hom (b.app a✝)) a_1 = (ConcreteCategory.hom (a.app a✝)) ⟨a_1, b_1⟩
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
x : (i : I) → P.obj (op (X i))
⊢ 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))

Tactic:
_

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
x : FamilyOfElements P (singleton (𝟙 X))
⊢ x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
_

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.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
⊢ Presheaf.IsSheaf J P

Tactic:
X

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
⊢ Presieve.IsSheaf J (P ⋙ coyoneda.obj (op X))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
⊢ Presieve.IsSheaf J (P ⋙ coyoneda.obj (op E))

Tactic:
X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
⊢ ∀ S ∈ J X, Presieve.IsSheafFor (P ⋙ coyoneda.obj (op E)) S.arrows
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
this : Mono (toRange p)
i : C
⊢ IsIso ((toRange p).app i)

Tactic:
rw [isIso_iff_bijective]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((toRange p).app i))
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ {s | G.sieveOfSection s ∈ J (unop U)}
Y✝ : C
⊢ ∀ (f : Y✝ ⟶ unop V),
    (Sieve.pullback i.unop (G.sieveOfSection s)).arrows f →
      (G.sieveOfSection ((ConcreteCategory.hom (F.map i)) s)).arrows f

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
U V : Cᵒᵖ
i : U ⟶ V
s : F.obj U
hs : s ∈ {s | G.sieveOfSection s ∈ J (unop U)}
Y✝ : C
f✝ : Y✝ ⟶ unop V
⊢ (Sieve.pullback i.unop (G.sieveOfSection s)).arrows f✝ →
    (G.sieveOfSection ((ConcreteCategory.hom (F.map i)) s)).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
⊢ Presieve.IsSheaf J (P' ⋙ coyoneda.obj (op U))

Tactic:
X

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
⊢ ∀ S ∈ J X, Presieve.IsSheafFor (P' ⋙ coyoneda.obj (op U)) S.arrows
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
⊢ Presieve.IsSheaf J G.toFunctor ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U

Tactic:
rw [← G.eq_sheafify_iff h]
  change _ ↔ G.sheafify J ≤ G
  exact ⟨Eq.ge, (G.le_sheafify J).antisymm⟩

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom ≫ 𝟙 (J.plusObj (J.plusObj (P ⋙ F))) =
    (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom

Tactic:
simp only [sheafify, Category.comp_id]

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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ IsIso ((forget D).map (S.toMultiequalizer (J.plusObj P)))

Tactic:
rw [isIso_iff_bijective]

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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))
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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
⊢ ∀ (f : P ⟶ Q) (g : Q ⟶ (sheafToPresheaf J D).obj R),
    { toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (f ≫ g) =
      (plusPlusSheaf J D).map f ≫
        { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          g

Tactic:
η

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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
⊢ ∀ (g : Q ⟶ (sheafToPresheaf J D).obj R),
    { toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (η ≫ g) =
      (plusPlusSheaf J D).map η ≫
        { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          g
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
by
    have := (TopCat.mono_iff_injective _).mpr hf.injective
    have := (TopCat.mono_iff_injective _).mpr hg.injective
    exact (TopCat.mono_iff_injective _).mp inferInstance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (empty C)
α : empty C ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') → ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)

Tactic:
by rintro _ ⟨⟨⟩⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr.refine_1
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ (ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(y, x), eq⟩ ∈
    ⇑(ConcreteCategory.hom (pullback.fst f g)) ⁻¹' U

Tactic:
simp only [coe_of, Set.mem_preimage]
      convert! hy
      rw [pullbackIsoProdSubtype_inv_fst_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
⊢ IsVanKampenColimit ((Cocone.precompose α).obj c)

Tactic:
intro F' c' α' f e hα

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono c₁.inl → Mono c₂.inl

Tactic:
_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono c₁.inl
⊢ Mono c₂.inl