-- 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:
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 }
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
have hf' := hW _ _ φ (fun j => hf (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 }
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 φ)
⊢ 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)
⊢ W.IsStableUnderProductsOfShape J

Tactic:
intro X₁ X₂ c₁ c₂ hc₁ hc₂ f hf

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
⊢ 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 }
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
have : HasProduct fun j ↦ X₂.obj (Discrete.mk j) :=
  hasLimitOfIso (Discrete.natIso (fun j ↦ Iso.refl (X₂.obj 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 }
this✝² : HasLimit X₁
this✝¹ : HasLimit X₂
this✝ : HasProduct fun j => X₁.obj { as := j }
this : HasProduct fun j => X₂.obj { 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 φ)
⊢ W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })

Tactic:
refine (W.arrow_mk_iso_iff ?_).2 hf'

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 φ)
⊢ Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f }) ≅ Arrow.mk (Limits.Pi.map φ)

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 φ)
⊢ (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

Tactic:
apply limit.hom_ext

Result:
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