C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (Functor.op G ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
⊢ (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)))
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (Functor.op G ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
⊢ FamilyOfElements.functorPushforward G x (G.map f) (_ : Presieve.functorPushforward G T (G.map f)) = x f hf
unfold FamilyOfElements.functorPushforward
case mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (Functor.op G ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
e₁ :
  getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)) =
    { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (Functor.op G ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
⊢ (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)))
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf
rcases e₁ : getFunctorPushforwardStructure (image_mem_functorPushforward G T hf) with
  ⟨X, g, f', hg, eq⟩
no goals
case mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (Functor.op G ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
e₁ :
  getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)) =
    { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac => ℱ.val.map h.op (x g h₁)) =
    x f hf
simpa using hG.Compatible ℱ h f' (𝟙 _) hg hf (by simp [eq])
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : SheafOfTypes K
Z : C
T : Presieve Z
x : FamilyOfElements (Functor.op G ⋙ ℱ.val) T
h : FamilyOfElements.Compatible x
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
e₁ :
  getFunctorPushforwardStructure (_ : Presieve.functorPushforward G T (G.map f)) =
    { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
⊢ f' ≫ G.map g = 𝟙 (G.obj Y) ≫ G.map f
simp [eq]