-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem pullbackCompatible_iff (x : FamilyOfElements P R) [R.hasPullbacks] :
    x.Compatible ↔ x.PullbackCompatible

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)

Tactic:
rw [← pullback.lift_fst _ _ comm, op_comp, FunctorToTypes.map_comp_apply, t hf₁ hf₂,
  ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.lift_snd]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
⊢ x.Compatible ↔ x.PullbackCompatible

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
⊢ x.Compatible → x.PullbackCompatible

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
⊢ x.PullbackCompatible → x.Compatible

Proof state:
case mp.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
this : HasPullback f₁ f₂
⊢ pullback.fst f₁ f₂ ≫ f₁ = pullback.snd f₁ f₂ ≫ f₂

Tactic:
apply pullback.condition

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)

Tactic:
haveI := hasPullbacks.has_pullbacks hf₁ hf₂

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
⊢ x.Compatible → x.PullbackCompatible

Tactic:
intro t Y₁ Y₂ f₁ f₂ hf₁ hf₂

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ P.map (pullback.fst f₁ f₂).op (x f₁ hf₁) = P.map (pullback.snd f₁ f₂).op (x f₂ hf₂)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ P.map (pullback.fst f₁ f₂).op (x f₁ hf₁) = P.map (pullback.snd f₁ f₂).op (x f₂ hf₂)

Tactic:
apply t

Result:
case mp.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ pullback.fst f₁ f₂ ≫ f₁ = pullback.snd f₁ f₂ ≫ f₂

Proof state:
case mp.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
⊢ pullback.fst f₁ f₂ ≫ f₁ = pullback.snd f₁ f₂ ≫ f₂

Tactic:
haveI := hasPullbacks.has_pullbacks hf₁ hf₂

Result:
case mp.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.Compatible
Y₁ Y₂ : C
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
this : HasPullback f₁ f₂
⊢ pullback.fst f₁ f₂ ≫ f₁ = pullback.snd f₁ f₂ ≫ f₂

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
⊢ x.PullbackCompatible → x.Compatible

Tactic:
intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.hasPullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ P.map g₁.op (x f₁ hf₁) = P.map g₂.op (x f₂ hf₂)