-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
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
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K)
hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
m : M
inr :
  ∀
    (this :
      ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_7 : AddCommGroup M]
        [inst_8 : AddCommGroup K] [inst_9 : AddCommGroup P] [inst_10 : Module R M] [inst_11 : Module R K]
        [inst_12 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id)
        (hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P))
        {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M)
        (hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P))
        (hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K))
        (hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr))
        (hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))) (m : M) (h : m ∈ s.ker),
        Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P))
    (h : m ∉ s.ker),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
wlog :
  ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_7 : AddCommGroup M]
    [inst_8 : AddCommGroup K] [inst_9 : AddCommGroup P] [inst_10 : Module R M] [inst_11 : Module R K]
    [inst_12 : Module R P] {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id)
    (hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P))
    {κ : Type u_6} {σ : Type u_7} (v : κ ⊕ σ → M)
    (hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P))
    (hslzero : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (Sum.inl i)) : K) (0 : K))
    (hli : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ Sum.inr))
    (hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))) (m : M) (h : m ∈ s.ker),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl))) ((g : (a : M) → P) m : P)

Tactic:
wlog h : m ∈ LinearMap.ker s

Premises used: LinearMap.ker