[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))
[PROOFSTEP]
rw [huv, disjoint_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range (↑f ∘ v)))
[PROOFSTEP]
refine' Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ↑f))
[PROOFSTEP]
rw [← LinearMap.range_coe, (span_eq (LinearMap.range f)), (exact_iff _ _).mp he]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (LinearMap.ker g)
[PROOFSTEP]
exact range_ker_disjoint hw
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ LinearIndependent R (Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w))
[PROOFSTEP]
refine' linearIndependent_leftExact hv _ hse.mono hse.exact _
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ LinearIndependent R (↑g ∘ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inr)
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ LinearIndependent R (↑g ∘ Function.invFun ↑g ∘ w)
[PROOFSTEP]
rwa [← Function.comp.assoc,
  Function.RightInverse.comp_eq_id (Function.rightInverse_invFun ((epi_iff_surjective _).mp hse.epi)),
  Function.comp.left_id]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
hv : LinearIndependent R v
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
hw✝ : LinearIndependent R (↑g ∘ u ∘ Sum.inr)
hm : Mono f
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
w : ι' → ↑P
hw : LinearIndependent R w
hse : ShortExact f g
⊢ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inl = ↑f ∘ v
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
⊢ ⊤ ≤ span R (range u)
[PROOFSTEP]
intro m _
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
⊢ m ∈ span R (range u)
[PROOFSTEP]
have hgm : g m ∈ span R (range (g ∘ u ∘ Sum.inr)) := hw mem_top
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
hgm : ↑g m ∈ span R (range (↑g ∘ u ∘ Sum.inr))
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hgm 
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
hgm : ∃ c, (Finsupp.sum c fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
⊢ m ∈ span R (range u)
[PROOFSTEP]
obtain ⟨cm, hm⟩ := hgm
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
⊢ m ∈ span R (range u)
[PROOFSTEP]
let m' : M := Finsupp.sum cm fun j a ↦ a • (u (Sum.inr j))
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ m ∈ span R (range u)
[PROOFSTEP]
have hsub : m - m' ∈ LinearMap.range f
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ m - m' ∈ LinearMap.range f
[PROOFSTEP]
rw [(exact_iff _ _).mp he]
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ m - m' ∈ LinearMap.ker g
[PROOFSTEP]
simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ ↑g m = ↑g (Finsupp.sum cm fun j a => a • u (Sum.inr j))
[PROOFSTEP]
rw [← hm, map_finsupp_sum]
[GOAL]
case hsub
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
⊢ (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = Finsupp.sum cm fun a b => ↑g (b • u (Sum.inr a))
[PROOFSTEP]
simp only [Function.comp_apply, SMulHomClass.map_smul]
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
hsub : m - m' ∈ LinearMap.range f
⊢ m ∈ span R (range u)
[PROOFSTEP]
obtain ⟨n, hnm⟩ := hsub
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
⊢ m ∈ span R (range u)
[PROOFSTEP]
have hn : n ∈ span R (range v) := hv mem_top
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
hn : n ∈ span R (range v)
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn 
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
hn : ∃ c, (Finsupp.sum c fun i a => a • v i) = n
⊢ m ∈ span R (range u)
[PROOFSTEP]
obtain ⟨cn, hn⟩ := hn
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
hnm : ↑f n = m - m'
cn : ι →₀ R
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [← hn, map_finsupp_sum] at hnm 
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ m ∈ span R (range u)
[PROOFSTEP]
rw [← sub_add_cancel m m', ← hnm, ]
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ (Finsupp.sum cn fun a b => ↑f (b • v a)) + m' ∈ span R (range u)
[PROOFSTEP]
simp only [SMulHomClass.map_smul]
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ ((Finsupp.sum cn fun a b => b • ↑f (v a)) + Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
have hn' : (Finsupp.sum cn fun a b ↦ b • f (v a)) = (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) := by congr; ext a b;
  change b • (f ∘ v) a = _; rw [← huv]; rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
[PROOFSTEP]
congr
[GOAL]
case e_g
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
⊢ (fun a b => b • ↑f (v a)) = fun a b => b • u (Sum.inl a)
[PROOFSTEP]
ext a b
[GOAL]
case e_g.h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
a : ι
b : R
⊢ b • ↑f (v a) = b • u (Sum.inl a)
[PROOFSTEP]
change b • (f ∘ v) a = _
[GOAL]
case e_g.h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
a : ι
b : R
⊢ b • (↑f ∘ v) a = b • u (Sum.inl a)
[PROOFSTEP]
rw [← huv]
[GOAL]
case e_g.h.h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
a : ι
b : R
⊢ b • (u ∘ Sum.inl) a = b • u (Sum.inl a)
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ((Finsupp.sum cn fun a b => b • ↑f (v a)) + Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
rw [hn']
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ((Finsupp.sum cn fun a b => b • u (Sum.inl a)) + Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
apply add_mem
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum cn fun a b => b • u (Sum.inl a)) ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp]
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ∃ c, (Finsupp.sum c fun i a => a • u i) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
[PROOFSTEP]
use cn.mapDomain (Sum.inl)
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum (Finsupp.mapDomain Sum.inl cn) fun i a => a • u i) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
[PROOFSTEP]
rw [Finsupp.sum_mapDomain_index_inj Sum.inl_injective]
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum cm fun j a => a • u (Sum.inr j)) ∈ span R (range u)
[PROOFSTEP]
rw [Finsupp.mem_span_range_iff_exists_finsupp]
[GOAL]
case intro.intro.intro.a
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ ∃ c, (Finsupp.sum c fun i a => a • u i) = Finsupp.sum cm fun j a => a • u (Sum.inr j)
[PROOFSTEP]
use cm.mapDomain (Sum.inr)
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
he : Exact f g
huv : u ∘ Sum.inl = ↑f ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (↑g ∘ u ∘ Sum.inr))
m : ↑M
a✝ : m ∈ ⊤
cm : ι' →₀ R
hm : (Finsupp.sum cm fun i a => a • (↑g ∘ u ∘ Sum.inr) i) = ↑g m
m' : ↑M := Finsupp.sum cm fun j a => a • u (Sum.inr j)
n : ↑N
cn : ι →₀ R
hnm : (Finsupp.sum cn fun a b => ↑f (b • v a)) = m - m'
hn : (Finsupp.sum cn fun i a => a • v i) = n
hn' : (Finsupp.sum cn fun a b => b • ↑f (v a)) = Finsupp.sum cn fun a b => b • u (Sum.inl a)
⊢ (Finsupp.sum (Finsupp.mapDomain Sum.inr cm) fun i a => a • u i) = Finsupp.sum cm fun j a => a • u (Sum.inr j)
[PROOFSTEP]
rw [Finsupp.sum_mapDomain_index_inj Sum.inr_injective]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ⊤ ≤ span R (range (Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w)))
[PROOFSTEP]
refine' span_exact he _ hv _
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inl = ↑f ∘ v
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ⊤ ≤ span R (range (↑g ∘ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inr))
[PROOFSTEP]
convert hw
[GOAL]
case h.e'_4.h.e'_6.h.e'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ↑g ∘ Sum.elim (↑f ∘ v) (Function.invFun g.toFun ∘ w) ∘ Sum.inr = w
[PROOFSTEP]
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]
[GOAL]
case h.e'_4.h.e'_6.h.e'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi g
he : Exact f g
⊢ ↑g ∘ Function.invFun ↑g ∘ w = w
[PROOFSTEP]
rw [ModuleCat.epi_iff_surjective] at hE 
[GOAL]
case h.e'_4.h.e'_6.h.e'_3
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
u : ι ⊕ ι' → ↑M
f : N ⟶ M
g : M ⟶ P
w : ι' → ↑P
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Function.Surjective ↑g
he : Exact f g
⊢ ↑g ∘ Function.invFun ↑g ∘ w = w
[PROOFSTEP]
rw [← Function.comp.assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE), Function.comp.left_id]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝³ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝² : Module.Free R ↑N
inst✝¹ : Module.Free R ↑P
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑M = Module.rank R ↑N + Module.rank R ↑P
[PROOFSTEP]
haveI := free_shortExact h
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝³ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝² : Module.Free R ↑N
inst✝¹ : Module.Free R ↑P
inst✝ : StrongRankCondition R
this : Module.Free R ↑M
⊢ Module.rank R ↑M = Module.rank R ↑N + Module.rank R ↑P
[PROOFSTEP]
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R N,
  Module.Free.rank_eq_card_chooseBasisIndex R P, Cardinal.add_def, Cardinal.eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝³ : Ring R
N P : ModuleCat R
v : ι → ↑N
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝² : Module.Free R ↑N
inst✝¹ : Module.Free R ↑P
inst✝ : StrongRankCondition R
this : Module.Free R ↑M
⊢ Nonempty (Module.Free.ChooseBasisIndex R ↑M ≃ Module.Free.ChooseBasisIndex R ↑N ⊕ Module.Free.ChooseBasisIndex R ↑P)
[PROOFSTEP]
exact
  ⟨Basis.indexEquiv (Module.Free.chooseBasis R M)
      (Basis.ofShortExact h (Module.Free.chooseBasis R N) (Module.Free.chooseBasis R P))⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝⁵ : Ring R
N P : ModuleCat R
v : ι → ↑N
n p : ℕ
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝⁴ : Module.Free R ↑N
inst✝³ : Module.Finite R ↑N
inst✝² : Module.Free R ↑P
inst✝¹ : Module.Finite R ↑P
hN : FiniteDimensional.finrank R ↑N = n
hP : FiniteDimensional.finrank R ↑P = p
inst✝ : StrongRankCondition R
⊢ FiniteDimensional.finrank R ↑M = n + p
[PROOFSTEP]
apply FiniteDimensional.finrank_eq_of_rank_eq
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝⁵ : Ring R
N P : ModuleCat R
v : ι → ↑N
n p : ℕ
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝⁴ : Module.Free R ↑N
inst✝³ : Module.Finite R ↑N
inst✝² : Module.Free R ↑P
inst✝¹ : Module.Finite R ↑P
hN : FiniteDimensional.finrank R ↑N = n
hP : FiniteDimensional.finrank R ↑P = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑M = ↑(n + p)
[PROOFSTEP]
rw [free_shortExact_rank_add h, ← hN, ← hP]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝⁵ : Ring R
N P : ModuleCat R
v : ι → ↑N
n p : ℕ
M : ModuleCat R
f : N ⟶ M
g : M ⟶ P
h : ShortExact f g
inst✝⁴ : Module.Free R ↑N
inst✝³ : Module.Finite R ↑N
inst✝² : Module.Free R ↑P
inst✝¹ : Module.Finite R ↑P
hN : FiniteDimensional.finrank R ↑N = n
hP : FiniteDimensional.finrank R ↑P = p
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑N + Module.rank R ↑P = ↑(FiniteDimensional.finrank R ↑N + FiniteDimensional.finrank R ↑P)
[PROOFSTEP]
simp only [Nat.cast_add, FiniteDimensional.finrank_eq_rank]
