-- Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
theorem w : res F U ≫ leftRes F U = res F U ≫ rightRes F U

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map (leSupr U x✝.as.1).op ≫ F.map ((U x✝.as.1).infLELeft (U x✝.as.2)).op =
    F.map (leSupr U x✝.as.2).op ≫ F.map ((U x✝.as.1).infLERight (U x✝.as.2)).op

Tactic:
rw [← F.map_comp]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U x✝.as.1).op ≫ ((U x✝.as.1).infLELeft (U x✝.as.2)).op) =
    F.map (leSupr U x✝.as.2).op ≫ F.map ((U x✝.as.1).infLERight (U x✝.as.2)).op

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U x✝.as.1).op ≫ ((U x✝.as.1).infLELeft (U x✝.as.2)).op) =
    F.map ((leSupr U x✝.as.2).op ≫ ((U x✝.as.1).infLERight (U x✝.as.2)).op)

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.1 ⊓ U p.2))) x✝ =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.1 ⊓ U p.2))) x✝

Tactic:
simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map (leSupr U x✝.as.1).op ≫ F.map ((U x✝.as.1).infLELeft (U x✝.as.2)).op =
    F.map (leSupr U x✝.as.2).op ≫ F.map ((U x✝.as.1).infLERight (U x✝.as.2)).op

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
⊢ ((Pi.lift fun i => F.map (leSupr U i).op) ≫
      Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) =
    (Pi.lift fun i => F.map (leSupr U i).op) ≫
      Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op

Tactic:
refine limit.hom_ext (fun _ => ?_)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.1 ⊓ U p.2))) x✝ =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.1 ⊓ U p.2))) x✝

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U x✝.as.1).op ≫ ((U x✝.as.1).infLELeft (U x✝.as.2)).op) =
    F.map (leSupr U x✝.as.2).op ≫ F.map ((U x✝.as.1).infLERight (U x✝.as.2)).op

Tactic:
rw [← F.map_comp]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U x✝.as.1).op ≫ ((U x✝.as.1).infLELeft (U x✝.as.2)).op) =
    F.map ((leSupr U x✝.as.2).op ≫ ((U x✝.as.1).infLERight (U x✝.as.2)).op)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
⊢ res F U ≫ leftRes F U = res F U ≫ rightRes F U

Tactic:
dsimp [res, leftRes, rightRes]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
⊢ ((Pi.lift fun i => F.map (leSupr U i).op) ≫
      Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) =
    (Pi.lift fun i => F.map (leSupr U i).op) ≫
      Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op