-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
/-- If `prodComparison F A B` is an isomorphism, then `F` preserves the limit of `pair A B`. -/
lemma preservesLimit_pair_of_isIso_prodComparison (A B : C)
    [IsIso (prodComparison F A B)] :
    PreservesLimit (pair A B) F

Proof state:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).π.app { as := WalkingPair.left } =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B)).π.app { as := WalkingPair.left }

Tactic:
simp [pairComp, prodComparison, lift, fst]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt ≅
    ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B)).pt

Tactic:
exact Iso.refl _

Result:
no goals

Proof state:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.snd ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)) =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      BinaryFan.snd ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B))

Tactic:
dsimp only [BinaryFan.snd]

Result:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).π.app { as := WalkingPair.right } =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B)).π.app { as := WalkingPair.right }

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ IsLimit (F.mapCone (product A B).cone)

Tactic:
refine IsLimit.equivOfNatIsoOfIso (pairComp A B F) _
   ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B))
     (BinaryFan.ext (by exact Iso.refl _) ?_ ?_) |>.invFun
     (IsLimit.extendIso _ (product (F.obj A) (F.obj B)).isLimit)

Result:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.fst ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)) =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      BinaryFan.fst ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B))

case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.snd ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)) =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      BinaryFan.snd ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B))

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ PreservesLimit (pair A B) F

Tactic:
apply preservesLimit_of_preserves_limit_cone (product A B).isLimit

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ IsLimit (F.mapCone (product A B).cone)

Proof state:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).π.app { as := WalkingPair.right } =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B)).π.app { as := WalkingPair.right }

Tactic:
simp [pairComp, prodComparison, lift, snd]

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ BinaryFan.fst ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)) =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      BinaryFan.fst ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B))

Tactic:
dsimp only [BinaryFan.fst]

Result:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).π.app { as := WalkingPair.left } =
    (Iso.refl ((Cones.postcompose (pairComp A B F).hom).obj (F.mapCone (product A B).cone)).pt).hom ≫
      ((product (F.obj A) (F.obj B)).cone.extend (prodComparison F A B)).π.app { as := WalkingPair.left }