-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
lemma Submodule.disjoint_ker_of_finrank_le [NoZeroSMulDivisors R M] {N : Type*} [AddCommGroup N]
    [Module R N] {L : Submodule R M} [Module.Finite R L] (f : M →ₗ[R] N)
    (h : finrank R L ≤ finrank R (L.map f)) :
    Disjoint L (LinearMap.ker f)

Proof state:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ Module.rank R ↥(ker (f.domRestrict L)) = 0

Tactic:
rw [← Submodule.finrank_eq_rank, Nat.cast_eq_zero]

Result:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Proof state:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(LinearMap.range (f.domRestrict L))
this : finrank R ↥(LinearMap.range (f.domRestrict L)) + finrank R ↥(ker (f.domRestrict L)) = finrank R ↥L
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(LinearMap.range (f.domRestrict L))
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Tactic:
have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank

Result:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(LinearMap.range (f.domRestrict L))
this : finrank R (↥L ⧸ ker (f.domRestrict L)) + finrank R ↥(ker (f.domRestrict L)) = finrank R ↥L
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Proof state:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ Disjoint L (ker f)

Tactic:
refine disjoint_iff.mpr <| LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <|
  Submodule.rank_eq_zero.mp ?_

Result:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ Module.rank R ↥(ker (f.domRestrict L)) = 0

Proof state:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(LinearMap.range (f.domRestrict L))
this : finrank R (↥L ⧸ ker (f.domRestrict L)) + finrank R ↥(ker (f.domRestrict L)) = finrank R ↥L
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Tactic:
rw [LinearEquiv.finrank_eq (f.domRestrict L).quotKerEquivRange] at this

Result:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(LinearMap.range (f.domRestrict L))
this : finrank R ↥(LinearMap.range (f.domRestrict L)) + finrank R ↥(ker (f.domRestrict L)) = finrank R ↥L
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Proof state:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(map f L)
⊢ finrank R ↥(ker (f.domRestrict L)) = 0

Tactic:
rw [← LinearMap.range_domRestrict] at h

Result:
R : Type u_2
M : Type u
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : HasRankNullity.{u, u_2} R
inst✝⁴ : StrongRankCondition R
inst✝³ : NoZeroSMulDivisors R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(LinearMap.range (f.domRestrict L))
⊢ finrank R ↥(ker (f.domRestrict L)) = 0