-- 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:
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₂

Tactic:
dsimp

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 ((F.map g).op ≫ h.op) y₁ = G.val.map ((F.map g).op ≫ h.op) 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 h.op (G.val.map (F.map g).op y₁) = G.val.map h.op (G.val.map (F.map g).op y₂)

Tactic:
have H := (hy₁ g hg).trans (hy₂ g hg).symm

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
H : (F.op ⋙ G.val).map g.op y₁ = (F.op ⋙ G.val).map g.op y₂
⊢ 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 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

Tactic:
exact ⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁),
  fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
    (hF₁.apply_map _ hx hf)⟩

Result:
no goals

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
H : (F.op ⋙ G.val).map g.op y₁ = (F.op ⋙ G.val).map g.op y₂
⊢ 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₂)

Tactic:
dsimp at H

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
H : G.val.map (F.map g).op y₁ = G.val.map (F.map g).op y₂
⊢ 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.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
H : G.val.map (F.map g).op y₁ = G.val.map (F.map g).op y₂
⊢ 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₂)

Tactic:
rw [H]

Result:
no goals