-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean
/-- If `F` is cover-preserving and compatible-preserving, then `F` is a continuous functor. -/
@[stacks 00WW "This is basically this Stacks entry."]
lemma Functor.isContinuous_of_coverPreserving (hF₁ : CompatiblePreserving.{w} K F)
    (hF₂ : CoverPreserving J K F) : Functor.IsContinuous.{w} F J K where
  op_comp_isSheaf_of_types G X S hS x hx

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
apply existsUnique_of_exists_of_unique

Result:
case hex
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
⊢ ∃ x_1, x.IsAmalgamation x_1

case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
⊢ ∀ (y₁ y₂ : (F.op ⋙ G.val).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Proof state:
case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ F.obj X⦄, (Sieve.functorPushforward F S).arrows f → G.val.map f.op y₁ = G.val.map f.op y₂

Tactic:
rintro Y _ ⟨Z, g, h, hg, rfl⟩

Result:
case hunique.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
Y : D
Z : C
g : Z ⟶ X
h : Y ⟶ F.obj Z
hg : S.arrows g
⊢ G.val.map (h ≫ F.map g).op y₁ = G.val.map (h ≫ F.map g).op y₂

Proof state:
case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
⊢ ∀ (y₁ y₂ : (F.op ⋙ G.val).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
intro y₁ y₂ hy₁ hy₂

Result:
case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
⊢ y₁ = y₂

Proof state:
case hunique.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
Y : D
Z : C
g : Z ⟶ X
h : Y ⟶ F.obj Z
hg : S.arrows g
⊢ G.val.map ((F.map g).op ≫ h.op) y₁ = G.val.map ((F.map g).op ≫ h.op) y₂

Tactic:
simp only [Functor.map_comp, types_comp_apply]

Result:
case hunique.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
Y : D
Z : C
g : Z ⟶ X
h : Y ⟶ F.obj Z
hg : S.arrows g
⊢ G.val.map h.op (G.val.map (F.map g).op y₁) = G.val.map h.op (G.val.map (F.map g).op y₂)

Proof state:
case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
⊢ y₁ = y₂

Tactic:
apply (Presieve.isSeparated_of_isSheaf _ _ ((isSheaf_iff_isSheaf_of_type _ _).1 G.2) _
  (hF₂.cover_preserve hS)).ext

Result:
case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.val).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ F.obj X⦄, (Sieve.functorPushforward F S).arrows f → G.val.map f.op y₁ = G.val.map f.op y₂

Proof state:
case hex
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
⊢ ∃ x_1, x.IsAmalgamation x_1

Tactic:
have H := (isSheaf_iff_isSheaf_of_type _ _).1 G.2 _ (hF₂.cover_preserve hS)

Result:
case hex
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type w)
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.val) S.arrows
hx : x.Compatible
H : IsSheafFor G.val (Sieve.functorPushforward F S).arrows
⊢ ∃ x_1, x.IsAmalgamation x_1