-- Mathlib/Algebra/Exact.lean
theorem Exact.split_tfae' (h : Function.Exact f g) :
    List.TFAE [
      Function.Injective f ∧ ∃ l, g ∘ₗ l = LinearMap.id,
      Function.Surjective g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e : N ≃ₗ[R] M × P, f = e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ e]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_3_to_1 : (∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e) → Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
this : Surjective ⇑g
⊢ Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id

Tactic:
exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
tfae_have 3 → 1
| ⟨e, e₁, e₂⟩ => by
  have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
  exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_3_to_1 : (∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e) → Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
tfae_have 2 → 3
| ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
this : Injective ⇑f
⊢ Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id

Tactic:
exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
⊢ Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id

Tactic:
have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
this : Injective ⇑f
⊢ Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_3_to_1 : (∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e) → Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id
tfae_3_to_2 : (∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e) → Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
tfae_have 1 → 3
| ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE