Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
this :
  (ConcreteCategory.hom (g₁.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y) =
    (ConcreteCategory.hom (g₂.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y)
E :
  (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
⊢ (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩ =
    (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y

pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
this :
  (ConcreteCategory.hom (g₁.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y) =
    (ConcreteCategory.hom (g₂.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y)
E :
  (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
⊢ (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩ =
    (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y

Tactic:
<;>

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
this :
  (ConcreteCategory.hom (g₁.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y) =
    (ConcreteCategory.hom (g₂.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y)
E :
  (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
⊢ (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩ =
    (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y

case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
this :
  (ConcreteCategory.hom (g₁.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y) =
    (ConcreteCategory.hom (g₂.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y)
E :
  (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
⊢ (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩ =
    (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y