awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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)
⊢ 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) (HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M)) : P)
have inr : HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M) ∈ s.ker
Tactic: apply this hs hfg v hg hslzero hli hsp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
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)
⊢ HSub.hSub (β := M) m ((f : (a : K) → M) ((s : (a : M) → K) m : K) : M) ∈ s.ker
have hs₁ : 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)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
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.{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)
have this : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this
Cleared hypotheses: m, h, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
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)
⊢ 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)
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
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
⊢ 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)
have hli₁ : ∀ 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
Cleared hypotheses: hli
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (hypothesis)
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
⊢ 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)
have hli₁ : ∀ (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
Cleared hypotheses: hli
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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.{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)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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))
⊢ LE.le.{u_4} (α := Submodule R P) ⊤ (span R (Set.range ((⇑g : (a : M) → P) ∘ v ∘ a)))
have apply : LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
Tactic: apply top_le_span_of_aux hs hfg (Sum.elim (v ∘ a) (v ∘ b)) hg hsa hlib
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
have rwa : LE.le (α := Submodule R M) ⊤ (span R (Set.range (v ∘ a) ∪ Set.range (v ∘ b)))
Tactic: rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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)))
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
have rwa₁ : LE.le (α := Submodule R M) ⊤ (span R (v '' Set.range a ∪ Set.range (v ∘ b)))
Tactic: rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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)))
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
have rwa₂ : LE.le (α := Submodule R M) ⊤ (span R (v '' Set.range a ∪ v '' Set.range b))
Tactic: rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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))
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
have rwa₃ : LE.le (α := Submodule R M) ⊤ (span R (v '' (Set.range a ∪ Set.range b)))
Tactic: rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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)))
⊢ LE.le (α := Submodule R M) ⊤ (span R (Set.range (Sum.elim (v ∘ a) (v ∘ b))))
have rwa₄ : LE.le (α := Submodule R M) ⊤ (span R (v '' Set.univ))
Tactic: rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Exact (goal)
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)
⊢ LE.le.{u_2} (α := Submodule R M) ⊤ (Submodule.span R (Set.range.{u_2, u_5 + 1} (ι := ι) (⇑v : (a : ι) → M)))
have rw : LE.le.{u_2} (α := Submodule R M) ⊤ ⊤
Tactic: rw [v.span_eq]