-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma functorPushforward_functor (S : Sieve X) (e : C ≌ D) :
    S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse

Proof state:
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
Z : C
iZX : Z ⟶ X
iYZ : Y ⟶ e.functor.obj Z
hiZX : S.arrows iZX
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows (iYZ ≫ e.functor.map iZX)

Tactic:
simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

Tactic:
constructor

Result:
case h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ S.arrows (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
simpa using H

Result:
no goals

Proof state:
case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ (functorPushforward e.functor S).arrows iYX

Tactic:
exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩

Result:
no goals

Proof state:
case h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

Tactic:
rintro ⟨Z, iZX, iYZ, hiZX, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
Z : C
iZX : Z ⟶ X
iYZ : Y ⟶ e.functor.obj Z
hiZX : S.arrows iZX
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows (iYZ ≫ e.functor.map iZX)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ iYX = e.counitInv.app Y ≫ e.functor.map (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
⊢ functorPushforward e.functor S = functorPullback e.inverse (pullback (e.unitInv.app X) S)

Tactic:
ext Y iYX

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

Proof state:
case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX

Tactic:
intro H

Result:
case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ (functorPushforward e.functor S).arrows iYX