-- Mathlib/CategoryTheory/Abelian/CommSq.lean
/-- Given a pushout square in an abelian category
```
X₁ ⟶ X₂
|    |
v    v
X₃ ⟶ X₄
```
the morphism `X₂ ⊞ X₃ ⟶ X₄` is an epimorphism. This lemma translates this
as the existence of liftings up to refinements: a morphism `z : T ⟶ X₄`
can be written as a sum of a morphism to `X₂` and a morphism to `X₃`,
at least if we allow a precomposition with an epimorphism `π : T' ⟶ T`. -/
lemma hom_eq_add_up_to_refinements (h : IsPushout t l r b) {T : C} (x₄ : T ⟶ X₄) :
    ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃),
      π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
have := h.epi_shortComplex_g

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Proof state:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ u ≫ ⋯.shortComplex.g = u ≫ (biprod.fst ≫ r + biprod.snd ≫ b)

Tactic:
congr

Result:
case intro.intro.intro.intro.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ ⋯.shortComplex.g = biprod.fst ≫ r + biprod.snd ≫ b

Proof state:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b

Tactic:
simp only [hu, assoc, ← Preadditive.comp_add]

Result:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ u ≫ ⋯.shortComplex.g = u ≫ (biprod.fst ≫ r + biprod.snd ≫ b)

Proof state:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
refine ⟨T', π, inferInstance, u ≫ biprod.fst, u ≫ biprod.snd, ?_⟩

Result:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b

Proof state:
case intro.intro.intro.intro.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ ⋯.shortComplex.g = biprod.fst ≫ r + biprod.snd ≫ b

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b

Tactic:
obtain ⟨T', π, _, u, hu⟩ := surjective_up_to_refinements_of_epi h.shortComplex.g x₄

Result:
case intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ ∃ T' π, ∃ (_ : Epi π), ∃ x₂ x₃, π ≫ x₄ = x₂ ≫ r + x₃ ≫ b