mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ presheafMap data G₀ ((data X).f i) = presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv

Tactic:
]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ presheafMap data G₀ ((data X).f i) = presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj ((data X).X i))).f j)

Tactic:
]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ restriction data G₀ ((data (F.obj ((data X).X i))).f j ≫ (data X).f i) =
    presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ ((data (F.obj ((data X).X i))).f j)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
⊢ Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀) ∧
    ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))

Tactic:
]

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
⊢ Presheaf.IsSheaf J₀ (F.op ⋙ presheaf data G₀) ∧
    ∀ (X : C), Nonempty (IsLimit ((data X).toOneHypercover.multifork (presheaf data G₀)))
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₃ ≫ b + x₂ ≫ r = x₃ ≫ b + x₂ ≫ r

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z✝ : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z✝
hR : Sieve.ofArrows T g ∈ (J.over X) Z✝
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : gi ≫ (fun i ↦ Over.Hom.left (g i)) i = gj ≫ (fun i ↦ Over.Hom.left (g i)) j
⊢ gj ≫ Over.Hom.left (g j) ≫ Z✝.hom = gj ≫ Over.Hom.left (g j) ≫ Z✝.hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0
⊢ x₄ = 0

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
⊢ ∀ (P : C) (g : P ⟶ cokernel t), g ≫ cokernel.map t b l r ⋯ = 0 → g = 0

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
⊢ ∀ (P : C) (g : P ⟶ cokernel t), g ≫ cokernel.map t b l r ⋯ = 0 → g = 0
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: ⊢ precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale

Tactic:
]

Goal state after:
⊢ precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
⊢ CoverPreserving (topology S) (proetaleTopology.over S) (ProEt.forget S)

Tactic:
]

Goal state after:
S : Scheme
⊢ CoverPreserving (topology S) (proetaleTopology.over S) (ProEt.forget S)
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
X : S.ProEt
inst✝ : IsEmpty ↥X.left
⊢ Sieve.generate ⊥ ∈ (precoverage S).toGrothendieck X

Tactic:
]

Goal state after:
S : Scheme
X : S.ProEt
inst✝ : IsEmpty ↥X.left
⊢ Sieve.generate ⊥ ∈ (precoverage S).toGrothendieck X
Module: Mathlib.AlgebraicGeometry.Sites.Proetale

Goal state before:
pp: S : Scheme
inst✝ : IsEmpty ↥S
⊢ ∀ (X : S.ProEt), ⊥ ∈ (topology S) X

Tactic:
]

Goal state after:
S : Scheme
inst✝ : IsEmpty ↥S
⊢ ∀ (X : S.ProEt), ⊥ ∈ (topology S) X
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ φ.app j ≫ colimit.ι X₂ j = φ.app j ≫ colimit.ι X₂ j

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ φ.app j ≫ c₂.ι.app j ≫ g₂ = φ.app j ≫ c₂.ι.app j ≫ g₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
⊢ ∀ ⦃A : C⦄ (y : A ⟶ kernel b), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ kernel.map t b l r ⋯

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPushout t l r b
⊢ ∀ ⦃A : C⦄ (y : A ⟶ kernel b), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ kernel.map t b l r ⋯
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ colimit.ι S.X₂ j = S.f.app j ≫ colimit.ι S.X₂ j

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.g.app j ≫ colimit.ι S.X₃ j = S.g.app j ≫ colimit.ι S.X₃ j

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom ((J.yoneda.map f).hom.app (op X))) (𝟙 X) = f

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom ((J.yoneda.map f).hom.app (op X))) (𝟙 X) = f
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app (op X'))) f =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.yonedaEquiv.symm x).hom.app (op X'))) f =
    J.yonedaEquiv (J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x))
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.hom.app (op Y))) g = (ConcreteCategory.hom (f.hom.app (op Y))) g

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type v)
f : J.yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.hom.app (op (unop Y)))) g.unop = (ConcreteCategory.hom (f.hom.app Y)) g.unop

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ∀ (b : Subobject X), (∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ b) → Subobject.mk f ≤ b

Tactic:
]

Goal state after:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ∀ (b : Subobject X), (∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ b) → Subobject.mk f ≤ b
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
u : J.yoneda.obj (unop X) ⟶ F
⊢ J.yoneda.map f.unop ≫ u = J.yoneda.map f.unop ≫ u

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (((uliftYoneda.{v', v, u} J).obj X).obj.map g.op ≫ f.hom.app (op Y))) { down := 𝟙 X } =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := 𝟙 Y ≫ g }

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (((uliftYoneda.{v', v, u} J).obj X).obj.map g.op ≫ f.hom.app (op Y))) { down := 𝟙 X } =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := 𝟙 Y ≫ g }
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) =
    J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map g ≫ f)

Tactic:
change (f.hom.app (op X) ≫ F.obj.map g.op) ⟨𝟙 X⟩ = f.hom.app (op Y) ⟨𝟙 Y ≫ g⟩
  rw [← f.hom.naturality]
  simp [uliftYoneda]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (((uliftYoneda.{v', v, u} J).map f).hom.app (op X))) { down := 𝟙 X } = { down := f }

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (((uliftYoneda.{v', v, u} J).map f).hom.app (op X))) { down := 𝟙 X } = { down := f }
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app (op X'))) { down := f } =
    (ConcreteCategory.hom (F.obj.map f.op)) x

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app (op X'))) { down := f } =
    (ConcreteCategory.hom (F.obj.map f.op)) x
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.hom.app (op Y))) { down := g } = (ConcreteCategory.hom (f.hom.app (op Y))) { down := g }

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
c' : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X) :=
  { pt := A✝, ι := { app := fun j ↦ Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯, naturality := ⋯ } }
j : J
⊢ (F.obj j).obj.hom = (F.obj j).obj.hom

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.hom.app (op (unop Y)))) { down := g.unop } =
    (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk f

Tactic:
]

Goal state after:
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk f
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
⊢ (uliftYoneda.{v', v, u} J).map f.unop ≫ u = (uliftYoneda.{v', v, u} J).map f.unop ≫ u

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
⊢ IsColimit ((Over.forget X).mapCocone c)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
⊢ IsColimit ((Over.forget X).mapCocone c)
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i : ι
a b : Y ⟶ X i
hab : a ≫ c.inj i = b ≫ c.inj i
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) b = (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) b

Tactic:
]

Goal state after: