-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem pushforwardFamily_compatible {X} (x : ℱ.obj (op X)) :
    (pushforwardFamily α x).Compatible

Proof state:
case mk
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      ℱ'.val.map iZW₁.op (α.app (op W₁) (ℱ.map iWX₁.op x)) = ℱ'.val.map iZW₂.op (α.app (op W₂) (ℱ.map iWX₂.op x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ X
h₂ : coverByImage G X f₂
l₂ : CoverByImageStructure G f₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ f₂
⊢ ℱ'.val.map (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.lift).op
      (α.app (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)
        (ℱ.map { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.map.op x)) =
    ℱ'.val.map (iZY₂ ≫ l₂.lift).op (α.app (op l₂.1) (ℱ.map l₂.map.op x))

Tactic:
obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂

Result:
case mk.mk
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      ℱ'.val.map iZW₁.op (α.app (op W₁) (ℱ.map iWX₁.op x)) = ℱ'.val.map iZW₂.op (α.app (op W₂) (ℱ.map iWX₂.op x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
W₂ : C
iYW₂ : Y₂ ⟶ G.obj W₂
iWX₂ : G.obj W₂ ⟶ X
h₂ : coverByImage G X (iYW₂ ≫ iWX₂)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ iYW₂ ≫ iWX₂
⊢ ℱ'.val.map (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.lift).op
      (α.app (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)
        (ℱ.map { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.map.op x)) =
    ℱ'.val.map (iZY₂ ≫ { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.lift).op
      (α.app (op { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.1)
        (ℱ.map { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.map.op x))

Proof state:
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
⊢ (pushforwardFamily α x).Compatible

Tactic:
suffices ∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁)
    (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
    ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x)) by
  rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e
  simp only [pushforwardFamily, ← FunctorToTypes.map_comp_apply, ← op_comp]
  generalize Nonempty.some h₁ = l₁
  generalize Nonempty.some h₂ = l₂
  obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁
  obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂
  exact this _ _ _ _ (by simpa only [Category.assoc] using e)

Result:
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
⊢ ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      ℱ'.val.map iZW₁.op (α.app (op W₁) (ℱ.map iWX₁.op x)) = ℱ'.val.map iZW₂.op (α.app (op W₂) (ℱ.map iWX₂.op x))