-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
lemma Pi.map_ext (x y : ToType (F.obj (∏ᶜ f : C)))
    (h : ∀ i, F.map (Pi.π f i) x = F.map (Pi.π f i) y) : x = y

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
⊢ x = y

Tactic:
apply ConcreteCategory.injective_of_mono_of_preservesPullback (PreservesProduct.iso F f).hom

Result:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
⊢ (ConcreteCategory.hom (PreservesProduct.iso F f).hom) x = (ConcreteCategory.hom (PreservesProduct.iso F f).hom) y

Proof state:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
⊢ (ConcreteCategory.hom (PreservesProduct.iso F f).hom) x = (ConcreteCategory.hom (PreservesProduct.iso F f).hom) y

Tactic:
apply Concrete.limit_ext _ (piComparison F _ x) (piComparison F _ y)

Result:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
⊢ ∀ (j : Discrete J),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) j))
        ((ConcreteCategory.hom (piComparison F f)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) j))
        ((ConcreteCategory.hom (piComparison F f)) y)

Proof state:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
j : J
⊢ (ConcreteCategory.hom (F.map (Pi.π f j))) x = (ConcreteCategory.hom (F.map (Pi.π f j))) y

Tactic:
exact h j

Result:
no goals

Proof state:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
j : J
⊢ (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) { as := j }))
      ((ConcreteCategory.hom (piComparison F f)) x) =
    (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) { as := j }))
      ((ConcreteCategory.hom (piComparison F f)) y)

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, piComparison_comp_π]

Result:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
j : J
⊢ (ConcreteCategory.hom (F.map (Pi.π f j))) x = (ConcreteCategory.hom (F.map (Pi.π f j))) y

Proof state:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
⊢ ∀ (j : Discrete J),
    (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) j))
        ((ConcreteCategory.hom (piComparison F f)) x) =
      (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) j))
        ((ConcreteCategory.hom (piComparison F f)) y)

Tactic:
intro ⟨j⟩

Result:
case a
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j => F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (ConcreteCategory.hom (F.map (Pi.π f i))) x = (ConcreteCategory.hom (F.map (Pi.π f i))) y
j : J
⊢ (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) { as := j }))
      ((ConcreteCategory.hom (piComparison F f)) x) =
    (ConcreteCategory.hom (limit.π (Discrete.functor fun b => F.obj (f b)) { as := j }))
      ((ConcreteCategory.hom (piComparison F f)) y)