-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem compatible_iff (x : FirstObj P R) :
    ((firstObjEqFamily P R).hom x).Compatible ↔ firstMap P R x = secondMap P R x

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ ((firstObjEqFamily P R).hom x).PullbackCompatible → firstMap P R x = secondMap P R x

Tactic:
intro t

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : ((firstObjEqFamily P R).hom x).PullbackCompatible
⊢ firstMap P R x = secondMap P R x

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t :
  ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (secondMap P R x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map (pullback.fst f g).op ((firstObjEqFamily P R).hom x f hf) =
    P.map (pullback.snd f g).op ((firstObjEqFamily P R).hom x g hg)

Tactic:
simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩

Result:
no goals

Proof state:
case mp.w
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : ((firstObjEqFamily P R).hom x).PullbackCompatible
⊢ ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (secondMap P R x)

Tactic:
rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩

Result:
case mp.w.mk.mk.mk.mk.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : ((firstObjEqFamily P R).hom x).PullbackCompatible
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
      { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } (firstMap P R x) =
    limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
      { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } (secondMap P R x)

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ firstMap P R x = secondMap P R x → ((firstObjEqFamily P R).hom x).PullbackCompatible

Tactic:
intro t Y Z f g hf hg

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : firstMap P R x = secondMap P R x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map (pullback.fst f g).op ((firstObjEqFamily P R).hom x f hf) =
    P.map (pullback.snd f g).op ((firstObjEqFamily P R).hom x g hg)

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : firstMap P R x = secondMap P R x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map (pullback.fst f g).op ((firstObjEqFamily P R).hom x f hf) =
    P.map (pullback.snd f g).op ((firstObjEqFamily P R).hom x g hg)

Tactic:
rw [Types.limit_ext_iff'] at t

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t :
  ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (secondMap P R x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
⊢ P.map (pullback.fst f g).op ((firstObjEqFamily P R).hom x f hf) =
    P.map (pullback.snd f g).op ((firstObjEqFamily P R).hom x g hg)

Proof state:
case mp.w.mk.mk.mk.mk.mk.mk
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : ((firstObjEqFamily P R).hom x).PullbackCompatible
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
      { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } (firstMap P R x) =
    limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
      { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } (secondMap P R x)

Tactic:
simpa [firstMap, secondMap] using t hf hg

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : ((firstObjEqFamily P R).hom x).PullbackCompatible
⊢ firstMap P R x = secondMap P R x

Tactic:
apply Limits.Types.limit_ext

Result:
case mp.w
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
t : ((firstObjEqFamily P R).hom x).PullbackCompatible
⊢ ∀ (j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })),
    limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (firstMap P R x) =
      limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j (secondMap P R x)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ ((firstObjEqFamily P R).hom x).PullbackCompatible ↔ firstMap P R x = secondMap P R x

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ ((firstObjEqFamily P R).hom x).PullbackCompatible → firstMap P R x = secondMap P R x

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ firstMap P R x = secondMap P R x → ((firstObjEqFamily P R).hom x).PullbackCompatible

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ ((firstObjEqFamily P R).hom x).Compatible ↔ firstMap P R x = secondMap P R x

Tactic:
rw [Presieve.pullbackCompatible_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : FirstObj P R
⊢ ((firstObjEqFamily P R).hom x).PullbackCompatible ↔ firstMap P R x = secondMap P R x