-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pullbackArrows_comm [HasPullbacks C] {X Y : C} (f : Y ⟶ X) (R : Presieve X) :
    Sieve.generate (R.pullbackArrows f) = (Sieve.generate R).pullback f

Proof state:
case h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g

Tactic:
rintro ⟨_, h, k, ⟨W, g, hg⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)

Proof state:
case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
rintro ⟨W, h, k, hk, comm⟩

Result:
case h.mpr.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g

Tactic:
constructor

Result:
case h.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g

case h.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows g

Tactic:
exact Sieve.le_generate R W hg

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
⊢ generate (Presieve.pullbackArrows f R) = pullback f (generate R)

Tactic:
ext W g

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)

Tactic:
exact Sieve.downward_closed _ (by exact Sieve.le_generate R W hg) (h ≫ pullback.fst g f)

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)

Tactic:
rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]

Result:
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)