-- Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
lemma Pi.map_eq_prod_map [∀ i, Decidable (P i)] : Pi.map f =
    ((Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd _ _)).hom ≫
      prod.map (Pi.map (fun (i : {x : I // P x}) ↦ f i.val))
      (Pi.map (fun (i : {x : I // ¬ P x}) ↦ f i.val)) ≫
        ((Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd _ _)).inv

Proof state:
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f ≫ ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).hom =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom ≫
      prod.map (map fun i => f ↑i) (map fun i => f ↑i)

Tactic:
dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]

Result:
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f ≫
      ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
          ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
            ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
              (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom =
    ((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
          ((binaryFanOfPropIsLimit X P).uniqueUpToIso
            ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
              (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
      prod.map (map fun i => f ↑i) (map fun i => f ↑i)

Proof state:
case h₁
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ (map f ≫
        ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
            ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom) ≫
      prod.fst =
    (((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
            ((binaryFanOfPropIsLimit X P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
        prod.map (map fun i => f ↑i) (map fun i => f ↑i)) ≫
      prod.fst

case h₂
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ (map f ≫
        ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
            ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom) ≫
      prod.snd =
    (((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
            ((binaryFanOfPropIsLimit X P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
        prod.map (map fun i => f ↑i) (map fun i => f ↑i)) ≫
      prod.snd

Tactic:
all_goals aesop_cat

Result:
no goals

Proof state:
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f ≫
      ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
          ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
            ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
              (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom =
    ((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
          ((binaryFanOfPropIsLimit X P).uniqueUpToIso
            ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
              (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
      prod.map (map fun i => f ↑i) (map fun i => f ↑i)

Tactic:
apply prod.hom_ext

Result:
case h₁
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ (map f ≫
        ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
            ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom) ≫
      prod.fst =
    (((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
            ((binaryFanOfPropIsLimit X P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
        prod.map (map fun i => f ↑i) (map fun i => f ↑i)) ≫
      prod.fst

case h₂
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ (map f ≫
        ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
            ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom) ≫
      prod.snd =
    (((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
            ((binaryFanOfPropIsLimit X P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
        prod.map (map fun i => f ↑i) (map fun i => f ↑i)) ≫
      prod.snd