-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem linearIndependent_left_of_flat (H : M.LinearDisjoint N) [Module.Flat R N]
    {ι : Type*} {m : ι → M} (hm : LinearIndependent R m) : LinearMap.ker (mulLeftMap N m) = ⊥

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective ⇑(mulLeftMap N m)

Tactic:
simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
← Function.comp_assoc, EquivLike.injective_comp]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective ⇑(mulLeftMap N m)

Tactic:
classical simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
  ← Function.comp_assoc, EquivLike.injective_comp]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))

Tactic:
exact H.injective.comp (Module.Flat.rTensor_preserves_injective_linearMap (M := N) _ hm)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))

Tactic:
rw [LinearIndependent] at hm

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ LinearMap.ker (mulLeftMap N m) = ⊥

Tactic:
refine LinearMap.ker_eq_bot_of_injective ?_

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Module.Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective ⇑(mulLeftMap N m)