-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem sheaf_condition : R.IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι _ (w P R)))

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ ∀ (a : P.obj (op X)), x.IsAmalgamation a ↔ forkMap P R a = (firstObjEqFamily P R).toEquiv.symm x

Tactic:
intro t

Result:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ forkMap P R t = (firstObjEqFamily P R).toEquiv.symm x

Proof state:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv (forkMap P R t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ P.map f.op t = (firstObjEqFamily P R).toEquiv (forkMap P R t) f hf

Tactic:
simp [forkMap]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      firstMap P R ((firstObjEqFamily P R).toEquiv.symm a) = secondMap P R ((firstObjEqFamily P R).toEquiv.symm a) →
        ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
simp_rw [← compatible_iff, ← Iso.toEquiv_fun, Equiv.apply_symm_apply]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R), a.Compatible → ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a

Proof state:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
⊢ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x

Tactic:
funext Y f hf

Result:
case h.h.mp.h.h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : R f
⊢ (firstObjEqFamily P R).toEquiv (forkMap P R t) f hf = x f hf

Proof state:
case h.h.mp.h.h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : R f
⊢ (firstObjEqFamily P R).toEquiv (forkMap P R t) f hf = x f hf

Tactic:
simpa [forkMap] using q _ _

Result:
no goals

Proof state:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv (forkMap P R t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ P.map f.op t = x f hf

Tactic:
rw [← q]

Result:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv (forkMap P R t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ P.map f.op t = (firstObjEqFamily P R).toEquiv (forkMap P R t) f hf

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ Presieve.IsSheafFor P R ↔ Nonempty (IsLimit (Fork.ofι (forkMap P R) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique,
  ← Equiv.forall_congr_right (firstObjEqFamily P R).toEquiv.symm]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      firstMap P R ((firstObjEqFamily P R).toEquiv.symm a) = secondMap P R ((firstObjEqFamily P R).toEquiv.symm a) →
        ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ ∀ (a : Presieve.FamilyOfElements P R),
    a.Compatible → ((∃! t, a.IsAmalgamation t) ↔ ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a)

Tactic:
intro x _

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔ ∃! x_1, forkMap P R x_1 = (firstObjEqFamily P R).toEquiv.symm x

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x

Tactic:
constructor

Result:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t → (firstObjEqFamily P R).toEquiv (forkMap P R t) = x

case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x → x.IsAmalgamation t

Proof state:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t → (firstObjEqFamily P R).toEquiv (forkMap P R t) = x

Tactic:
intro q

Result:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
⊢ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ forkMap P R t = (firstObjEqFamily P R).toEquiv.symm x

Tactic:
rw [Equiv.eq_symm_apply]

Result:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t ↔ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x

Proof state:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ (firstObjEqFamily P R).toEquiv (forkMap P R t) = x → x.IsAmalgamation t

Tactic:
intro q Y f hf

Result:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv (forkMap P R t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ P.map f.op t = x f hf

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R), a.Compatible → ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
apply forall₂_congr

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.hasPullbacks
⊢ ∀ (a : Presieve.FamilyOfElements P R),
    a.Compatible → ((∃! t, a.IsAmalgamation t) ↔ ∃! x, forkMap P R x = (firstObjEqFamily P R).toEquiv.symm a)