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

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j (firstMap P S x) =
      limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j (secondMap P S x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) ⋯ = P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)

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

Result:
no goals

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

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

Result:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ ((firstObjEqFamily P S.arrows).hom x).SieveCompatible ↔ firstMap P S x = secondMap P S x

Proof state:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : ((firstObjEqFamily P S.arrows).hom x).SieveCompatible
⊢ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (firstMap P S x) =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (secondMap P S x)

Tactic:
intros Y Z g f hf

Result:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : ((firstObjEqFamily P S.arrows).hom x).SieveCompatible
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (firstMap P S x) =
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (secondMap P S x)

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ firstMap P S x = secondMap P S x → ((firstObjEqFamily P S.arrows).hom x).SieveCompatible

Tactic:
intro t Y Z f g hf

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : firstMap P S x = secondMap P S x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) ⋯ = P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ ((firstObjEqFamily P S.arrows).hom x).SieveCompatible → firstMap P S x = secondMap P S x

Tactic:
intro t

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : ((firstObjEqFamily P S.arrows).hom x).SieveCompatible
⊢ firstMap P S x = secondMap P S x

Proof state:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : ((firstObjEqFamily P S.arrows).hom x).SieveCompatible
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (firstMap P S x) =
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (secondMap P S x)

Tactic:
simpa [firstMap, secondMap] using t _ g hf

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ ((firstObjEqFamily P S.arrows).hom x).SieveCompatible ↔ firstMap P S x = secondMap P S x

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ ((firstObjEqFamily P S.arrows).hom x).SieveCompatible → firstMap P S x = secondMap P S x

case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ firstMap P S x = secondMap P S x → ((firstObjEqFamily P S.arrows).hom x).SieveCompatible

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : firstMap P S x = secondMap P S x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) ⋯ = P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)

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
S : Sieve X
x : FirstObj P S.arrows
t :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j (firstMap P S x) =
      limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j (secondMap P S x)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).hom x (g ≫ f) ⋯ = P.map g.op ((firstObjEqFamily P S.arrows).hom x f hf)

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : ((firstObjEqFamily P S.arrows).hom x).SieveCompatible
⊢ firstMap P S x = secondMap P S x

Tactic:
apply SecondObj.ext

Result:
case mp.h
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : ((firstObjEqFamily P S.arrows).hom x).SieveCompatible
⊢ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (firstMap P S x) =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ (secondMap P S x)