-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem compatible_iff (x : FirstObj P X) : (Arrows.Compatible P π ((Types.productIso _).hom x)) ↔
    firstMap P X π x = secondMap P X π x

Proof state:
case 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 : FirstObj P X
t : Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x)
ij : I × I
⊢ Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij (firstMap P X π x) =
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij (secondMap P X π x)

Tactic:
simpa [firstMap, secondMap] using t ij.1 ij.2

Result:
no goals

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 : FirstObj P X
⊢ Arrows.Compatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) ↔ firstMap P X π x = secondMap P X π x

Tactic:
rw [Arrows.pullbackCompatible_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 : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) ↔
    firstMap P X π x = secondMap P X π x

Proof state:
case 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 : FirstObj P X
i j : I
t :
  Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j) (firstMap P X π x) =
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j) (secondMap P X π x)
⊢ P.map (pullback.fst (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x i) =
    P.map (pullback.snd (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x j)

Tactic:
simpa [firstMap, secondMap] using t

Result:
no goals

Proof state:
case 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 : FirstObj P X
t : Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x)
⊢ firstMap P X π x = secondMap P X π x

Tactic:
ext ij

Result:
case 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 : FirstObj P X
t : Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x)
ij : I × I
⊢ Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij (firstMap P X π x) =
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij (secondMap P X π x)

Proof state:
case 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 : FirstObj P X
⊢ firstMap P X π x = secondMap P X π x →
    Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x)

Tactic:
intro t i j

Result:
case 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 : FirstObj P X
t : firstMap P X π x = secondMap P X π x
i j : I
⊢ P.map (pullback.fst (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x i) =
    P.map (pullback.snd (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x j)

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 : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) ↔
    firstMap P X π x = secondMap P X π x

Tactic:
constructor

Result:
case 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 : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) →
    firstMap P X π x = secondMap P X π x

case 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 : FirstObj P X
⊢ firstMap P X π x = secondMap P X π x →
    Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x)

Proof state:
case 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 : FirstObj P X
t : firstMap P X π x = secondMap P X π x
i j : I
⊢ P.map (pullback.fst (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x i) =
    P.map (pullback.snd (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x j)

Tactic:
apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t

Result:
case 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 : FirstObj P X
i j : I
t :
  Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j) (firstMap P X π x) =
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) (i, j) (secondMap P X π x)
⊢ P.map (pullback.fst (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x i) =
    P.map (pullback.snd (π i) (π j)).op ((Types.productIso fun i => P.obj (op (X i))).hom x j)

Proof state:
case 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 : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x) →
    firstMap P X π x = secondMap P X π x

Tactic:
intro t

Result:
case 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 : FirstObj P X
t : Arrows.PullbackCompatible P π ((Types.productIso fun i => P.obj (op (X i))).hom x)
⊢ firstMap P X π x = secondMap P X π x