-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
/-- A locally-fully-faithful and cover-dense functor preserves compatible families. -/
lemma compatiblePreserving [G.IsLocallyFaithful K] : CompatiblePreserving K G

Proof state:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ ∀ ⦃Z_1 : C⦄ (j : Z_1 ⟶ V₂),
    j ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = j ≫ iV₂Y₂ ≫ g₂ →
      ℱ.val.map (G.map j).op
          (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))))) =
        ℱ.val.map (G.map j).op
          (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))))

Tactic:
intro V₃ iV₃ e₄

Result:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
V₃ : C
iV₃ : V₃ ⟶ V₂
e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂
⊢ ℱ.val.map (G.map iV₃).op
      (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))))) =
    ℱ.val.map (G.map iV₃).op
      (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))))

Proof state:
case compatible
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Tactic:
apply Functor.IsCoverDense.ext G

Result:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
⊢ ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op (ℱ.val.map f₁.op (x g₁ hg₁)) = ℱ.val.map f.op (ℱ.val.map f₂.op (x g₂ hg₂))

Proof state:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁)))) =
    ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂))))

Tactic:
refine IsLocallyFaithful.ext G _ (iV₂V₁ ≫ iV₁Y₁ ≫ g₁) (iV₂Y₂ ≫ g₂) (by simp [e₁, e₂, eq]) ?_

Result:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ ∀ ⦃Z_1 : C⦄ (j : Z_1 ⟶ V₂),
    j ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = j ≫ iV₂Y₂ ≫ g₂ →
      ℱ.val.map (G.map j).op
          (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))))) =
        ℱ.val.map (G.map j).op
          (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))))

Proof state:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
⊢ ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))) =
    ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))

Tactic:
refine IsLocallyFull.ext G _ (G.map iVW ≫ i ≫ f₂) fun V₂ iV₂V₁ iV₂Y₂ e₂ ↦ ?_

Result:
case compatible.h
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
D : Type u_2
inst✝³ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_7)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁)))) =
    ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂))))