-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem functorPullback_pushforward_covering [G.IsCoverDense K] [G.IsLocallyFull K] {X : C}
    (T : K (G.obj X)) : (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X)

Proof state:
case intro.mk
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback (iWZ ≫ iZY) (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K W

Tactic:
rw [Sieve.pullback_comp]

Result:
case intro.mk
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))) ∈
    K W

Proof state:
case intro.mk
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))) ∈
    K W

Tactic:
apply K.pullback_stable

Result:
case intro.mk.hS
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)

Proof state:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ Y⦄,
    (Sieve.coverByImage G Y).arrows f →
      Sieve.pullback f (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K Y_1

Tactic:
rintro W _ ⟨Z, iWZ, iZY, rfl⟩

Result:
case intro.mk
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback (iWZ ≫ iZY) (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K W

Proof state:
case intro.mk.hS
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)

Tactic:
clear W iWZ

Result:
case intro.mk.hS
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)

Proof state:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
⊢ Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)) ∈ K Y

Tactic:
apply K.transitive (G.is_cover_of_isCoverDense _ _) _

Result:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ Y⦄,
    (Sieve.coverByImage G Y).arrows f →
      Sieve.pullback f (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K Y_1

Proof state:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤
    Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))

Tactic:
rintro W _ ⟨V, iVZ, iWV, ⟨iVX, e⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))).arrows
    (iWV ≫ G.map iVZ)

Proof state:
case intro.mk.hS
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)

Tactic:
apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))

Result:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
⊢ Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤
    Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))

Proof state:
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ ((iWV ≫ G.map iVZ) ≫ iZY) ≫ iYX = iWV ≫ G.map iVX

Tactic:
simp [e]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
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
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))).arrows
    (iWV ≫ G.map iVZ)

Tactic:
exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩

Result:
no goals