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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
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 : Compatible x
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
⊢ Presheaf.IsSheaf J (Functor.op G ⋙ ℱ.val)
intro X U S hS x hx
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
change FamilyOfElements (G.op ⋙ ℱ.val ⋙ coyoneda.obj (op X)) _ at x
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
⊢ ∃! t, IsAmalgamation x t
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
let H := ℱ.2 X _ (hG₂.cover_preserve hS)
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ∃! t, IsAmalgamation x t
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
⊢ ∃! t, IsAmalgamation x t
let hx' := hx.functorPushforward hG₁ (sheafOver ℱ X)
case h
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) ?w ∧
    ∀ (y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op), (fun t => IsAmalgamation x t) y → y = ?w

case w
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ∃! t, IsAmalgamation x t
constructor
case w
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op

case h
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) ?w ∧
    ∀ (y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op), (fun t => IsAmalgamation x t) y → y = ?w
case h
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) ?w ∧
    ∀ (y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op), (fun t => IsAmalgamation x t) y → y = ?w

case w
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
swap
case h.left
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx')

case h.right
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ∀ (y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op),
    (fun t => IsAmalgamation x t) y → y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
case h
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx') ∧
    ∀ (y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op),
      (fun t => IsAmalgamation x t) y → y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
constructor
case w
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ Compatible (FamilyOfElements.functorPushforward G x)
case w
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
apply H.amalgamate (x.functorPushforward G)
no goals
case w
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ Compatible (FamilyOfElements.functorPushforward G x)
exact hx'
case h.left
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
V : C
f : V ⟶ U
hf : S.arrows f
⊢ ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).map f.op
      (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx') =
    x f hf
case h.left
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ (fun t => IsAmalgamation x t) (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx')
intro V f hf
case h.e'_3.h
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
V : C
f : V ⟶ U
hf : S.arrows f
e_1✝ : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj V.op = (ℱ.val ⋙ coyoneda.obj X.op).obj (G.obj V).op
⊢ x f hf = FamilyOfElements.functorPushforward G x (G.map f) (_ : Presieve.functorPushforward G S.arrows (G.map f))
case h.left
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
V : C
f : V ⟶ U
hf : S.arrows f
⊢ ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).map f.op
      (IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx') =
    x f hf
convert H.isAmalgamation hx' (G.map f) (image_mem_functorPushforward G S hf)
no goals
case h.e'_3.h
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
V : C
f : V ⟶ U
hf : S.arrows f
e_1✝ : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj V.op = (ℱ.val ⋙ coyoneda.obj X.op).obj (G.obj V).op
⊢ x f hf = FamilyOfElements.functorPushforward G x (G.map f) (_ : Presieve.functorPushforward G S.arrows (G.map f))
rw [hG₁.apply_map (sheafOver ℱ X) hx]
case h.right
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
⊢ y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
case h.right
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
⊢ ∀ (y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op),
    (fun t => IsAmalgamation x t) y → y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
intro y hy
case h.right
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
⊢ IsAmalgamation (FamilyOfElements.functorPushforward G x) y
case h.right
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
⊢ y = IsSheafFor.amalgamate H (FamilyOfElements.functorPushforward G x) hx'
refine'
  H.isSeparatedFor _ y _ _ (H.isAmalgamation (hx.functorPushforward hG₁ (sheafOver ℱ X)))
case h.right.intro.intro.intro.intro
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✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ (ℱ.val ⋙ coyoneda.obj X.op).map (g' ≫ G.map f').op y =
    FamilyOfElements.functorPushforward G x (g' ≫ G.map f') (_ : ∃ Z_1 g h, S.arrows g ∧ g' ≫ G.map f' = h ≫ G.map g)
case h.right
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 : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
⊢ IsAmalgamation (FamilyOfElements.functorPushforward G x) y
rintro V f ⟨Z, f', g', h, rfl⟩
case h.right.intro.intro.intro.intro
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✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ (ℱ.val ⋙ coyoneda.obj X.op).map (g' ≫ G.map f').op y =
    (sheafOver ℱ X).val.map g'.op
      (FamilyOfElements.functorPushforward G x (G.map f') (_ : Presieve.functorPushforward G S.arrows (G.map f')))
case h.right.intro.intro.intro.intro
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✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ (ℱ.val ⋙ coyoneda.obj X.op).map (g' ≫ G.map f').op y =
    FamilyOfElements.functorPushforward G x (g' ≫ G.map f') (_ : ∃ Z_1 g h, S.arrows g ∧ g' ≫ G.map f' = h ≫ G.map g)
erw [FamilyOfElements.comp_of_compatible (S.functorPushforward G) hx'
    (image_mem_functorPushforward G (S : Presieve U) h) g']
case h.right.intro.intro.intro.intro
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✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ y ≫ ℱ.val.map ((G.map f').op ≫ g'.op) =
    FamilyOfElements.functorPushforward G x (G.map f') (_ : Presieve.functorPushforward G S.arrows (G.map f')) ≫
      ℱ.val.map g'.op
case h.right.intro.intro.intro.intro
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✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ (ℱ.val ⋙ coyoneda.obj X.op).map (g' ≫ G.map f').op y =
    (sheafOver ℱ X).val.map g'.op
      (FamilyOfElements.functorPushforward G x (G.map f') (_ : Presieve.functorPushforward G S.arrows (G.map f')))
dsimp
no goals
case h.right.intro.intro.intro.intro
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✝ : Compatible x✝
G : C ⥤ D
hG₁ : CompatiblePreserving K G
hG₂ : CoverPreserving J K G
ℱ : Sheaf K A
X : A
U : C
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves J U
x : FamilyOfElements (Functor.op G ⋙ ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
H : IsSheafFor (ℱ.val ⋙ coyoneda.obj X.op) (Sieve.functorPushforward G S).arrows :=
  Sheaf.cond ℱ X (Sieve.functorPushforward G S) (CoverPreserving.cover_preserve hG₂ hS)
hx' : Compatible (FamilyOfElements.functorPushforward G x) := Compatible.functorPushforward hG₁ (sheafOver ℱ X) hx
y : ((Functor.op G ⋙ ℱ.val) ⋙ coyoneda.obj X.op).obj U.op
hy : IsAmalgamation x y
V : D
Z : C
f' : Z ⟶ U
g' : V ⟶ G.obj Z
h : S.arrows f'
⊢ y ≫ ℱ.val.map ((G.map f').op ≫ g'.op) =
    FamilyOfElements.functorPushforward G x (G.map f') (_ : Presieve.functorPushforward G S.arrows (G.map f')) ≫
      ℱ.val.map g'.op
simp [hG₁.apply_map (sheafOver ℱ X) hx h, ← hy f' h]