-- Mathlib/CategoryTheory/Limits/MonoCoprod.lean
lemma mono_map'_of_injective [HasCoproduct (X ∘ ι)] [HasCoproduct X]
    [HasCoproduct (fun (k : ((Set.range ι)ᶜ : Set I)) => X k.1)] :
    Mono (Sigma.map' ι (fun j => 𝟙 ((X ∘ ι) j)))

Proof state:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
j : J
⊢ Sigma.ι X (ι j) = (Cofan.mk (∐ X) fun j => Sigma.ι X (ι j)).ι.app { as := j }

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_5
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
⊢ (Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.desc fun j => Sigma.ι X (ι j)

Tactic:
apply Sigma.hom_ext

Result:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
⊢ ∀ (b : J),
    (Sigma.ι (X ∘ ι) b ≫ Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) b ≫ Sigma.desc fun j => Sigma.ι X (ι j)

Proof state:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
j : J
⊢ (Sigma.ι (X ∘ ι) j ≫ Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) j ≫ Sigma.desc fun j => Sigma.ι X (ι j)

Tactic:
rw [Sigma.ι_comp_map', id_comp, colimit.ι_desc]

Result:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
j : J
⊢ Sigma.ι X (ι j) = (Cofan.mk (∐ X) fun j => Sigma.ι X (ι j)).ι.app { as := j }

Proof state:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
⊢ ∀ (b : J),
    (Sigma.ι (X ∘ ι) b ≫ Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) b ≫ Sigma.desc fun j => Sigma.ι X (ι j)

Tactic:
intro j

Result:
case h.e'_5.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
j : J
⊢ (Sigma.ι (X ∘ ι) j ≫ Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.ι (X ∘ ι) j ≫ Sigma.desc fun j => Sigma.ι X (ι j)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
⊢ Mono (Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j))

Tactic:
convert mono_of_injective' X ι hι

Result:
case h.e'_5
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst✝² : HasCoproduct (X ∘ ι)
inst✝¹ : HasCoproduct X
inst✝ : HasCoproduct fun k => X ↑k
⊢ (Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j)) = Sigma.desc fun j => Sigma.ι X (ι j)