-- 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.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 = (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) i

Tactic:
simp [forkMap]

Result:
no goals

Proof state:
case h.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
⊢ ∀ (a : P.obj (op B)),
    (∀ (i : I), P.map (π i).op a = x i) ↔ forkMap P X π a = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x

Tactic:
intro t

Result:
case h.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)
⊢ (∀ (i : I), P.map (π i).op t = x i) ↔ forkMap P X π t = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x

Proof state:
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

Tactic:
simpa [forkMap] using q i

Result:
no goals

Proof state:
case h.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)
⊢ (∀ (i : I), P.map (π i).op t = x i) ↔ forkMap P X π t = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x

Tactic:
erw [Equiv.eq_symm_apply]

Result:
case h.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)
⊢ (∀ (i : I), P.map (π i).op t = x i) ↔ (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x

Proof state:
case h.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)
⊢ (∀ (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:
constructor

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)
⊢ (∀ (i : I), P.map (π i).op t = x i) → (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x

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

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)
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

Tactic:
rw [← q]

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 = (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) i

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
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

Tactic:
apply existsUnique_congr

Result:
case h.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
⊢ ∀ (a : P.obj (op B)),
    (∀ (i : I), P.map (π i).op a = x i) ↔ forkMap P X π a = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x

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))),
      firstMap P X π ((Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a) =
          secondMap P X π ((Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a) →
        ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).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 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

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) ↔
    ∀ (y : FirstObj P X), firstMap P X π y = secondMap P X π y → ∃! x, forkMap P X π x = y

Tactic:
erw [← Equiv.forall_congr_right (Types.productIso _).toEquiv.symm]

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) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      firstMap P X π ((Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a) =
          secondMap P X π ((Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a) →
        ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a