-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem LinearIndependent.sumElim_of_quotient
    {M' : Submodule R M} {ι₁ ι₂} {f : ι₁ → M'} (hf : LinearIndependent R f) (g : ι₂ → M)
    (hg : LinearIndependent R (Submodule.Quotient.mk (p := M') ∘ g)) :
    LinearIndependent R (Sum.elim (f · : ι₁ → M) g)

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
⊢ LinearIndependent R (Sum.elim (fun x => ↑(f x)) g)

Tactic:
refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
⊢ Disjoint (span R (range fun x => ↑(f x))) (span R (range g))

Proof state:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a => a • g i) ∈ span R (range fun x => ↑(f x))
h₂ : (c.sum fun i a => a • g i) ∈ span R (range g)
this : (c.sum fun a b => b • Submodule.Quotient.mk (g a)) = 0
⊢ (c.sum fun i a => a • g i) = 0

Tactic:
rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]

Result:
no goals

Proof state:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a => a • g i) ∈ span R (range fun x => ↑(f x))
h₂ : (c.sum fun i a => a • g i) ∈ span R (range g)
this : (c.sum fun i a => a • g i) ∈ M'
⊢ (c.sum fun i a => a • g i) = 0

Tactic:
simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsupp_sum, map_smul, mkQ_apply] at this

Result:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a => a • g i) ∈ span R (range fun x => ↑(f x))
h₂ : (c.sum fun i a => a • g i) ∈ span R (range g)
this : (c.sum fun a b => b • Submodule.Quotient.mk (g a)) = 0
⊢ (c.sum fun i a => a • g i) = 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
⊢ Disjoint (span R (range fun x => ↑(f x))) (span R (range g))

Tactic:
refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
x : M
h₁ : x ∈ span R (range fun x => ↑(f x))
h₂ : x ∈ span R (range g)
⊢ x = 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
x : M
h₁ : x ∈ span R (range fun x => ↑(f x))
h₂ : x ∈ span R (range g)
⊢ x = 0

Tactic:
have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
x : M
h₁ : x ∈ span R (range fun x => ↑(f x))
h₂ : x ∈ span R (range g)
this : x ∈ M'
⊢ x = 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
x : M
h₁ : x ∈ span R (range fun x => ↑(f x))
h₂ : x ∈ span R (range g)
this : x ∈ M'
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂

Result:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a => a • g i) ∈ span R (range fun x => ↑(f x))
h₂ : (c.sum fun i a => a • g i) ∈ span R (range g)
this : (c.sum fun i a => a • g i) ∈ M'
⊢ (c.sum fun i a => a • g i) = 0