-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem sheaf_condition : (Presieve.ofArrows X π).IsSheafFor P ↔
    Nonempty (IsLimit (Fork.ofι (forkMap P X π) (w P X π)))

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
⊢ ∀ (a : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π a →
      ((∃! t, ∀ (i : I), P.map (π i).op t = a i) ↔
        ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a)

Tactic:
intro x _

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
⊢ (∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔
    ∃! x_1, forkMap P X π x_1 = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x

Proof state:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q : ∀ (i : I), P.map (π i).op t = x i
⊢ (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x

Tactic:
funext i

Result:
case h.h.mp.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q : ∀ (i : I), P.map (π i).op t = x i
i : I
⊢ (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) i = x i

Proof state:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x → ∀ (i : I), P.map (π i).op t = x i

Tactic:
intro q i

Result:
case h.h.mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q : (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x
i : I
⊢ P.map (π i).op t = x i

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      Arrows.Compatible P π a → ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a

Tactic:
apply forall₂_congr

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
⊢ ∀ (a : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π a →
      ((∃! t, ∀ (i : I), P.map (π i).op t = a i) ↔
        ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
⊢ IsSheafFor P (Presieve.ofArrows X π) ↔ Nonempty (IsLimit (Fork.ofι (forkMap P X π) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique, isSheafFor_arrows_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔
    ∀ (y : FirstObj P X), firstMap P X π y = secondMap P X π y → ∃! x, forkMap P X π x = y

Proof state:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), P.map (π i).op t = x i) → (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x

Tactic:
intro q

Result:
case h.h.mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q : ∀ (i : I), P.map (π i).op t = x i
⊢ (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x