-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma IsStableUnderProductsOfShape.mk (J : Type*) [W.RespectsIso]
    (hW : ∀ (X₁ X₂ : J → C) [HasProduct X₁] [HasProduct X₂]
      (f : ∀ j, X₁ j ⟶ X₂ j) (_ : ∀ (j : J), W (f j)),
      W (Limits.Pi.map f)) : W.IsStableUnderProductsOfShape J

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j => X₁.obj { as := j }
this : HasProduct fun j => X₂.obj { as := j }
hf' : W (Limits.Pi.map φ)
⊢ ∀ (j : Discrete J),
    ((hc₁.conePointUniqueUpToIso (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm).hom ≫ (Arrow.mk (Limits.Pi.map φ)).hom) ≫
        limit.π (Discrete.functor fun j => X₂.obj { as := j }) j =
      ((Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })).hom ≫
          (hc₂.conePointUniqueUpToIso (limit.isLimit X₂) ≪≫ (Pi.isoLimit X₂).symm).hom) ≫
        limit.π (Discrete.functor fun j => X₂.obj { as := j }) j

Tactic:
rintro ⟨j⟩

Result:
case w.mk
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j => X₁.obj { as := j }
this : HasProduct fun j => X₂.obj { as := j }
hf' : W (Limits.Pi.map φ)
j : J
⊢ ((hc₁.conePointUniqueUpToIso (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm).hom ≫ (Arrow.mk (Limits.Pi.map φ)).hom) ≫
      limit.π (Discrete.functor fun j => X₂.obj { as := j }) { as := j } =
    ((Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })).hom ≫
        (hc₂.conePointUniqueUpToIso (limit.isLimit X₂) ≪≫ (Pi.isoLimit X₂).symm).hom) ≫
      limit.π (Discrete.functor fun j => X₂.obj { as := j }) { as := j }

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
let φ := fun j => f.app (Discrete.mk j)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j => X₁.obj { as := j }
this : HasProduct fun j => X₂.obj { as := j }
hf' : W (Limits.Pi.map φ)
⊢ Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f }) ≅ Arrow.mk (Limits.Pi.map φ)

Tactic:
refine Arrow.isoMk
  (IsLimit.conePointUniqueUpToIso hc₁ (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm)
  (IsLimit.conePointUniqueUpToIso hc₂ (limit.isLimit X₂) ≪≫ (Pi.isoLimit _).symm) ?_

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j => X₁.obj { as := j }
this : HasProduct fun j => X₂.obj { as := j }
hf' : W (Limits.Pi.map φ)
⊢ (hc₁.conePointUniqueUpToIso (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm).hom ≫ (Arrow.mk (Limits.Pi.map φ)).hom =
    (Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })).hom ≫
      (hc₂.conePointUniqueUpToIso (limit.isLimit X₂) ≪≫ (Pi.isoLimit X₂).symm).hom

Proof state:
case w.mk
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j => X₁.obj { as := j }
this : HasProduct fun j => X₂.obj { as := j }
hf' : W (Limits.Pi.map φ)
j : J
⊢ ((hc₁.conePointUniqueUpToIso (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm).hom ≫ (Arrow.mk (Limits.Pi.map φ)).hom) ≫
      limit.π (Discrete.functor fun j => X₂.obj { as := j }) { as := j } =
    ((Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })).hom ≫
        (hc₂.conePointUniqueUpToIso (limit.isLimit X₂) ≪≫ (Pi.isoLimit X₂).symm).hom) ≫
      limit.π (Discrete.functor fun j => X₂.obj { as := j }) { as := j }

Tactic:
simp [φ]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
have : HasLimit X₁ := ⟨c₁, hc₁⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Pi.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
hc₁ : IsLimit c₁
hc₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }
this : HasLimit X₁
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })