awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
x : M := (f : (a : K) → M) ((s : (a : M) → K) m : K)
⊢ Eq (α := K) ((s ∘ₗ f : (a : K) → K) ((s : (a : M) → K) m : K) : K)
    ((LinearMap.id : (a : K) → K) ((s : (a : M) → K) m : K) : K)

Tactic:
replace hs := DFunLike.congr_fun hs (s m)
-- 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
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
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
x : M := (f : (a : K) → M) ((s : (a : M) → K) m : K)
hs :
  Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M) : K)
    ((s : (a : M) → K) m : K)
⊢ HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M) ∈ s.ker

Tactic:
simp [hs]
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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 (γ := Submodule R M) (Submodule.span R (Set.range v)) m

Tactic:
have : m ∈ Submodule.span R (Set.range v) := hsp Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) m
obtain :
  ∀ (c : κ ⊕ σ →₀ R) (h : (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i) ∈ s.ker)
    (this :
      Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)),
    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) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i) : 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:
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this

Premises used: Finsupp.mem_span_range_iff_exists_finsupp, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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))
c : κ ⊕ σ →₀ R
h : (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i) ∈ s.ker
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)
⊢ Eq.{u_3 + 1} (α := K)
    (∑ x ∈ c.support.toRight,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := K) ((c : (a : κ ⊕ σ) → R) (Sum.inr x) : R)
        ((s : (a : M) → K) (v (Sum.inr x)) : K))
    0

Tactic:
simp only [LinearMap.mem_ker, Finsupp.sum, map_sum, map_smul,
    Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, map_add, hslzero, smul_zero,
    Finset.sum_const_zero, zero_add] at h

Premises used: Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, Finsupp.sum, smul_zero, map_add, map_sum, zero_add, Finset.sum_const_zero, LinearMap.mem_ker, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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))
c : κ ⊕ σ →₀ R
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)
h :
  Eq.{u_3 + 1} (α := K)
    (∑ x ∈ c.support.toRight,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := K) ((c : (a : κ ⊕ σ) → R) (Sum.inr x) : R)
        ((s : (a : M) → K) (v (Sum.inr x)) : K))
    0
⊢ ∀ i ∈ c.support.toRight, Eq.{u_1 + 1} (α := R) (Function.comp (β := κ ⊕ σ) (⇑c : (a : κ ⊕ σ) → R) Sum.inr i) 0

Tactic:
replace hli := (linearIndependent_iff'.mp hli) c.support.toRight (c ∘ .inr) h
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
c : κ ⊕ σ →₀ R
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)
h :
  Eq.{u_3 + 1} (α := K)
    (∑ x ∈ c.support.toRight,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := K) ((c : (a : κ ⊕ σ) → R) (Sum.inr x) : R)
        ((s : (a : M) → K) (v (Sum.inr x)) : K))
    0
hli : ∀ i ∈ c.support.toRight, Eq.{u_1 + 1} (α := R) (Function.comp (β := κ ⊕ σ) (⇑c : (a : κ ⊕ σ) → R) Sum.inr i) 0
⊢ ∀ (i : σ), Eq.{u_1 + 1} (α := R) ((c : (a : κ ⊕ σ) → R) (Sum.inr i) : R) (0 : R)

Tactic:
simp only [Finset.mem_toRight, Finsupp.mem_support_iff, Function.comp_apply, not_imp_self] at hli

Premises used: Finsupp.mem_support_iff, not_imp_self, Finset.mem_toRight, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
c : κ ⊕ σ →₀ R
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)
h :
  Eq.{u_3 + 1} (α := K)
    (∑ x ∈ c.support.toRight,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := K) ((c : (a : κ ⊕ σ) → R) (Sum.inr x) : R)
        ((s : (a : M) → K) (v (Sum.inr x)) : K))
    0
hli : ∀ (i : σ), Eq.{u_1 + 1} (α := R) ((c : (a : κ ⊕ σ) → R) (Sum.inr i) : R) (0 : R)
simp :
  Membership.mem (γ := Submodule R P) (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl)))
    (∑ x ∈ c.support.toLeft,
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) ((c : (a : κ ⊕ σ) → R) (Sum.inl x) : R)
        ((g : (a : M) → P) (v (Sum.inl x)) : 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) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i) : P)

Tactic:
simp only [Finsupp.sum, Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, hli, zero_smul,
    Finset.sum_const_zero, add_zero, map_sum, map_smul]

Premises used: Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, Finsupp.sum, map_sum, Finset.sum_const_zero, zero_smul, add_zero, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
c : κ ⊕ σ →₀ R
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)
h :
  Eq.{u_3 + 1} (α := K)
    (∑ x ∈ c.support.toRight,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := K) ((c : (a : κ ⊕ σ) → R) (Sum.inr x) : R)
        ((s : (a : M) → K) (v (Sum.inr x)) : K))
    0
hli : ∀ (i : σ), Eq.{u_1 + 1} (α := R) ((c : (a : κ ⊕ σ) → R) (Sum.inr i) : R) (0 : R)
⊢ Membership.mem (γ := Submodule R P) (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl)))
    (∑ x ∈ c.support.toLeft,
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) ((c : (a : κ ⊕ σ) → R) (Sum.inl x) : R)
        ((g : (a : M) → P) (v (Sum.inl x)) : P))

Tactic:
Submodule.sum_mem _ (fun i hi ↦ Submodule.smul_mem _ _ <| Submodule.subset_span ⟨i, rfl⟩)

Premises used: Submodule.sum_mem, Function.comp, Sum.inl, Exists.intro, Submodule.span, Submodule.subset_span, Set.range, DFunLike.coe, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Basis.Exact
Goal:
R_1 : Type u_1
M_1 : Type u_2
K_1 : Type u_3
P_1 : Type u_4
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup K_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 K_1
inst_6 : Module R_1 P_1
g_1 : M_1 →ₗ[R_1] P_1
s_1 : M_1 →ₗ[R_1] K_1
κ_1 : Type u_6
σ_1 : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst_7 : Ring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup K
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R K
inst_13 : 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)
hsp : LE.le (α := Submodule R M) ⊤ (Submodule.span R (Set.range v))
c : κ ⊕ σ →₀ R
this : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range v)) (c.sum fun (i : κ ⊕ σ) (a : R) ↦ a • v i)
h :
  Eq.{u_3 + 1} (α := K)
    (∑ x ∈ c.support.toRight,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := K) ((c : (a : κ ⊕ σ) → R) (Sum.inr x) : R)
        ((s : (a : M) → K) (v (Sum.inr x)) : K))
    0
hli : ∀ (i : σ), Eq.{u_1 + 1} (α := R) ((c : (a : κ ⊕ σ) → R) (Sum.inr i) : R) (0 : R)
⊢ Membership.mem (γ := Submodule R P) (Submodule.span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ Sum.inl)))
    (∑ x ∈ c.support.toLeft,
      HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) ((c : (a : κ ⊕ σ) → R) (Sum.inl x) : R)
        ((g : (a : M) → P) (v (Sum.inl x)) : P))

Tactic:
exact Submodule.sum_mem _ (fun i hi ↦ Submodule.smul_mem _ _ <| Submodule.subset_span ⟨i, rfl⟩)
-- 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_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hlib : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ b)
hab : Codisjoint (Set.range a) (Set.range b)
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
apply : LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
⊢ LE.le.{u_4} (α := Submodule R P) ⊤ (span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ a)))

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

Premises used: Function.comp, _private.0.top_le_span_of_aux, Sum.elim
-- 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_5
κ : Type u_6
σ : Type u_7
v : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) (v (a i)) : K) (0 : K)
hlib : LinearIndependent.{u_7, u_1, u_3} R (M := K) ((⇑s : (a : M) → K) ∘ v ∘ b)
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
hab : Set.range a ∪ Set.range b = Set.univ
rwa : LE.le (α := Submodule R M) ⊤ (span R (Set.range (v ∘ a) ∪ Set.range (v ∘ b)))
rwa₁ : LE.le (α := Submodule R M) ⊤ (span R (v '' Set.range a ∪ Set.range (v ∘ b)))
rwa₂ : LE.le (α := Submodule R M) ⊤ (span R (v '' Set.range a ∪ v '' Set.range b))
rwa₃ : LE.le (α := Submodule R M) ⊤ (span R (v '' (Set.range a ∪ Set.range b)))
rwa₄ : LE.le (α := Submodule R M) ⊤ (span R (v '' Set.univ))
rwa₅ rwa₆ rwa₇ rwa₈ : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
⊢ LE.le (α := Submodule R M) ⊤ (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]

Premises used: Set.range_comp, Set.image_univ, Set.Sum.elim_range, Set.image_union
-- 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_5
κ : Type u_6
σ : Type u_7
v_1 : ι → M
a : κ → ι
b : σ → ι
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
v : Basis ι R M
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((v : (a : ι) → M) (a i) : M) : K) (0 : K)
hlib :
  LinearIndependent.{u_7, u_1, u_3} R (M := K)
    (Function.comp.{u_7 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑s : (a : M) → K) ((⇑v : (a : ι) → M) ∘ b))
hab : Codisjoint (Set.range a) (Set.range b)
rw rw₁ : LE.le.{u_2} (α := Submodule R M) ⊤ ⊤
⊢ LE.le.{u_2} (α := Submodule R M) ⊤ (Submodule.span R (Set.range.{u_2, u_5 + 1} (ι := ι) (⇑v : (a : ι) → M)))

Tactic:
rw [v.span_eq]

Premises used: Module.Basis.span_eq
-- 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_5
κ : Type u_6
σ : Type u_7
a : κ → ι
b : σ → ι
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
v : Basis ι R M
hainj : Function.Injective a
hsa : ∀ (i : κ), Eq.{u_3 + 1} (α := K) ((s : (a : M) → K) ((v : (a : ι) → M) (a i) : M) : K) (0 : K)
hlib :
  LinearIndependent.{u_7, u_1, u_3} R (M := K)
    (Function.comp.{u_7 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑s : (a : M) → K) ((⇑v : (a : ι) → M) ∘ b))
hab : Codisjoint (Set.range a) (Set.range b)
k : κ
⊢ Eq.{u_4 + 1} (α := P) ((ofSplitExact hs hfg hg v hainj hsa hlib hab : (a : κ) → P) k : P)
    ((g : (a : M) → P) ((v : (a : ι) → M) (a k) : M) : P)

Tactic:
simp [ofSplitExact]

Premises used: Module.Basis.ofSplitExact
-- 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
hfg : Function.Exact.{u_3, u_2, u_4} (M := K) (N := M) (P := P) (⇑f : (a : K) → M) (⇑g : (a : M) → P)
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
rw :
  Set.SurjOn (α := M) (β := ↥p) (⇑(p.projectionOnto q hpq) : (a : M) → ↥p)
    (Set.range.{u_2, u_3 + 1} (ι := K) (⇑f : (a : K) → M)) Set.univ
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := K) (β := ↥p) (⇑(p.projectionOnto q hpq ∘ₗ f) : (a : K) → ↥p)

Tactic:
rw [← Set.surjOn_univ, LinearMap.coe_comp, Set.surjOn_comp_iff, Set.image_univ]

Premises used: Set.image_univ, Set.surjOn_univ, Set.surjOn_comp_iff, LinearMap.coe_comp