-- Mathlib/LinearAlgebra/Basis/Exact.lean
private lemma top_le_span_of_aux (v : κ ⊕ σ → M)
    (hg : Function.Surjective g) (hslzero : ∀ i, s (v (.inl i)) = 0)
    (hli : LinearIndependent R (s ∘ v ∘ .inr)) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) :
    ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ .inl)

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✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
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_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
h : m ∈ LinearMap.ker s
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
have : m ∈ Submodule.span R (Set.range v) := hsp Submodule.mem_top

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✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
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_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
h : m ∈ LinearMap.ker s
this : m ∈ Submodule.span R (Set.range v)
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

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_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) →
                  ∀ m ∈ LinearMap.ker s, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ LinearMap.ker s
x : M := f (s m)
⊢ g m = g (m - f (s m))

Tactic:
simp [hfg.apply_apply_eq_zero]

Result:
no goals

Proof state:
case intro
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_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
wlog h : m ∈ LinearMap.ker s

Result:
case intro.inr
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_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
this :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
    [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K]
    [inst_6 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
    s ∘ₗ f = LinearMap.id →
      Function.Exact ⇑f ⇑g →
        ∀ {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M),
          Function.Surjective ⇑g →
            (∀ (i : κ), s (v (Sum.inl i)) = 0) →
              LinearIndependent R (⇑s ∘ v ∘ Sum.inr) →
                ⊤ ≤ Submodule.span R (Set.range v) →
                  ∀ m ∈ LinearMap.ker s, g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))
h : m ∉ LinearMap.ker s
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

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✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
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_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
h : m ∈ LinearMap.ker s
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))