-- Mathlib/CategoryTheory/Limits/MonoCoprod.lean
lemma mono_of_injective_aux (hι : Function.Injective ι) (c : Cofan X) (c₁ : Cofan (X ∘ ι))
    (hc : IsColimit c) (hc₁ : IsColimit c₁)
    (c₂ : Cofan (fun (k : ((Set.range ι)ᶜ : Set I)) => X k.1))
    (hc₂ : IsColimit c₂) : Mono (Cofan.IsColimit.desc hc₁ (fun i => c.inj (ι i)))

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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
e : J ⊕ ↑(Set.range ι)ᶜ ≃ I :=
  ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl ↑(Set.range ι)ᶜ)).trans (Equiv.Set.sumCompl (Set.range ι))
⊢ ∀ (i₁ : J),
    (c₁.inj i₁ ≫ Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i)) =
      (Cofan.mk c.pt fun i' => c.inj (e i')).inj (Sum.inl i₁)

Tactic:
simp [e]

Result:
no goals

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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))

Tactic:
let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)

Result:
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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
e : J ⊕ ↑(Set.range ι)ᶜ ≃ I :=
  ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl ↑(Set.range ι)ᶜ)).trans (Equiv.Set.sumCompl (Set.range ι))
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))

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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
e : J ⊕ ↑(Set.range ι)ᶜ ≃ I :=
  ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl ↑(Set.range ι)ᶜ)).trans (Equiv.Set.sumCompl (Set.range ι))
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))

Tactic:
refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
  hc₁ hc₂ _ (by simp [e])

Result:
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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
e : J ⊕ ↑(Set.range ι)ᶜ ≃ I :=
  ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl ↑(Set.range ι)ᶜ)).trans (Equiv.Set.sumCompl (Set.range ι))
⊢ IsColimit (Cofan.mk c.pt fun i' => c.inj (e i'))

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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
e : J ⊕ ↑(Set.range ι)ᶜ ≃ I :=
  ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl ↑(Set.range ι)ᶜ)).trans (Equiv.Set.sumCompl (Set.range ι))
⊢ IsColimit (Cofan.mk c.pt fun i' => c.inj (e i'))

Tactic:
exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocones.equivalenceOfReindexing
  (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocones.ext (Iso.refl _))

Result:
no goals

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 ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k => X ↑k
hc₂ : IsColimit c₂
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))

Tactic:
classical
let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
  hc₁ hc₂ _ (by simp [e])
exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocones.equivalenceOfReindexing
  (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocones.ext (Iso.refl _))

Result:
no goals