-- Mathlib/LinearAlgebra/Basis/Exact.lean
lemma Submodule.top_le_span_of_exact_of_retraction (hg : Function.Surjective g)
    (hsa : ∀ i, s (v (a i)) = 0) (hlib : LinearIndependent R (s ∘ v ∘ b))
    (hab : Codisjoint (Set.range a) (Set.range b))
    (hsp : ⊤ ≤ Submodule.span R (Set.range v)) :
    ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ a)

Proof state:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
hsp : ⊤ ≤ span R (Set.range v)
⊢ ⊤ ≤ span R (Set.range (Sum.elim (v ∘ a) (v ∘ b)))

Tactic:
simp only [codisjoint_iff, Set.sup_eq_union, Set.top_eq_univ] at hab

Result:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ v ∘ b)
hsp : ⊤ ≤ span R (Set.range v)
hab : Set.range a ∪ Set.range b = Set.univ
⊢ ⊤ ≤ span R (Set.range (Sum.elim (v ∘ a) (v ∘ b)))

Proof state:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ v ∘ b)
hsp : ⊤ ≤ span R (Set.range v)
hab : Set.range a ∪ Set.range b = Set.univ
⊢ ⊤ ≤ span R (Set.range (Sum.elim (v ∘ a) (v ∘ b)))

Tactic:
rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
hsp : ⊤ ≤ span R (Set.range v)
⊢ ⊤ ≤ span R (Set.range (⇑g ∘ v ∘ a))

Tactic:
apply top_le_span_of_aux hs hfg (Sum.elim (v ∘ a) (v ∘ b)) hg hsa hlib

Result:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective ⇑g
hsa : ∀ (i : κ), s (v (a i)) = 0
hlib : LinearIndependent R (⇑s ∘ v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
hsp : ⊤ ≤ span R (Set.range v)
⊢ ⊤ ≤ span R (Set.range (Sum.elim (v ∘ a) (v ∘ b)))