-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
theorem to_product_injective_of_isLimit {D : Cone F} (hD : IsLimit D) :
    Function.Injective fun (x : ToType D.pt) (j : J) => D.π.app j x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
a b : E.pt
h : T.hom a = T.hom b
⊢ T.inv (T.hom a) = T.inv (T.hom b)

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
⊢ Function.Injective T.hom

Tactic:
intro a b h

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
a b : E.pt
h : T.hom a = T.hom b
⊢ a = b

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Tactic:
let hE : IsLimit E := isLimitOfPreserves _ hD

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
a b : E.pt
h : T.hom a = T.hom b
⊢ a = b

Tactic:
suffices T.inv (T.hom a) = T.inv (T.hom b) by simpa

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
a b : E.pt
h : T.hom a = T.hom b
⊢ T.inv (T.hom a) = T.inv (T.hom b)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Tactic:
let E := (forget C).mapCone D

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Tactic:
let hG := Types.limitConeIsLimit.{w, v} (F ⋙ forget C)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
⊢ Function.Injective fun x j => (ConcreteCategory.hom (D.π.app j)) x

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
a b : E.pt
h : T.hom a = T.hom b
this : T.inv (T.hom a) = T.inv (T.hom b)
⊢ a = b

Tactic:
simpa

Result:
no goals