awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₂ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₃ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₄ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₅ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map s.subtype (comap s.subtype (s ⊓ t))) +
    Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₂ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₃ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₄ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₅ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map s.subtype (comap s.subtype (s ⊓ t))) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₆ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₂ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₃ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₄ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₅ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map s.subtype (comap s.subtype (s ⊓ t))) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₆ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₇ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map (s ⊔ t).subtype (comap (s ⊔ t).subtype t)) +
    Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₂ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₃ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₄ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₅ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map s.subtype (comap s.subtype (s ⊓ t))) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₆ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
rw₇ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map (s ⊔ t).subtype (comap (s ⊔ t).subtype t)) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₈ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥((s ⊔ t) ⊓ t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t
have rw : Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t)
Tactic: rw [← Submodule.rank_sup_add_rank_inf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
⊢ finrank.{u_1, u} R (M ⧸ N) + finrank.{u_1, u} R ↥N = finrank R M
have rw : Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
Tactic: rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
    Submodule.finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
S : Type u_1
inst_6 : Ring S
inst_7 : SMul R S
inst_8 : Module S M
inst_9 : IsScalarTower R S M
N : Submodule S M
⊢ finrank.{u_2, u} R (M ⧸ N) = finrank R M - finrank.{u_2, u} R ↥N
have rw : finrank.{u_2, u} R (M ⧸ N) =
  finrank.{u_2, u} R (HasQuotient.Quotient M (B := Submodule R M) (restrictScalars R N)) +
      finrank.{u_2, u} R ↥(restrictScalars R N) -
    finrank.{u_2, u} R ↥N
Tactic: rw [← (N.restrictScalars R).finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
⊢ Disjoint L f.ker
have refine : Module.rank R ↥(f.domRestrict L).ker = 0
Tactic: refine disjoint_iff.mpr <| LinearMap.injective_domRestrict_iff.mp <| LinearMap.ker_eq_bot.mp <|
    Submodule.rank_eq_zero.mp ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
⊢ Module.rank R ↥(f.domRestrict L).ker = 0
have rw : finrank.{u_2, u} R ↥(f.domRestrict L).ker = 0
Tactic: rw [← Submodule.finrank_eq_rank, Nat.cast_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(map f L)
⊢ finrank.{u_2, u} R ↥(f.domRestrict L).ker = 0
have h₁ : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range
Tactic: rw [← LinearMap.range_domRestrict] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range
⊢ finrank.{u_2, u} R ↥(f.domRestrict L).ker = 0
have this : finrank.{u_2, u} R (↥L ⧸ (f.domRestrict L).ker) + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L
Tactic: have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_2} R
inst_4 : StrongRankCondition R
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
N : Type u_1
inst_7 : AddCommGroup N
inst_8 : Module R N
L : Submodule R M
inst_9 : Module.Finite.{u_2, u} R ↥L
f : M →ₗ[R] N
h : finrank.{u_2, u} R ↥L ≤ finrank.{u_2, u_1} R ↥(f.domRestrict L).range
this :
  finrank.{u_2, u} R (↥L ⧸ (f.domRestrict L).ker) + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L
⊢ finrank.{u_2, u} R ↥(f.domRestrict L).ker = 0
have this₁ : finrank.{u_2, u_1} R ↥(f.domRestrict L).range + finrank.{u_2, u} R ↥(f.domRestrict L).ker = finrank.{u_2, u} R ↥L
Tactic: rw [LinearEquiv.finrank_eq (f.domRestrict L).quotKerEquivRange] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have obtain : ∀ (s : Finset (M ⧸ N)) (hs : s.card = finrank.{u_1, u} R (M ⧸ N))
  (hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))),
  ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic: obtain ⟨s, hs, hs'⟩ :=
    exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
⊢ s.Nonempty
have rwa : s ≠ ∅
Tactic: rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
rwa : s ≠ ∅
⊢ s.Nonempty
have rwa₁ : ¬s = ∅
Tactic: rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
⊢ s.Nonempty
have rwa₂ : ¬s.card = 0
Tactic: rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
rwa₂ : ¬s.card = 0
⊢ s.Nonempty
have rwa₃ : ¬finrank.{u_1, u} R (M ⧸ N) = 0
Tactic: rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
rwa₂ : ¬s.card = 0
rwa₃ : ¬finrank.{u_1, u} R (M ⧸ N) = 0
⊢ s.Nonempty
have rwa₄ : ¬finrank R M - finrank.{u_1, u} R ↥N = 0
Tactic: rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
rwa₂ : ¬s.card = 0
rwa₃ : ¬finrank.{u_1, u} R (M ⧸ N) = 0
rwa₄ : ¬finrank R M - finrank.{u_1, u} R ↥N = 0
⊢ s.Nonempty
have rwa₅ : ¬finrank R M ≤ finrank.{u_1, u} R ↥N
Tactic: rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have obtain : ∀ (v : M ⧸ N) (hv : v ∈ s), ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic: obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M ⧸ N
hv : v ∈ s
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have obtain : ∀ (v : M) (hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)),
  ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic: obtain ⟨v, rfl⟩ := N.mkQ_surjective v
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have refine : ∀ (r : R) (hr : r ≠ 0), r • v ∈ N → r = 0
Tactic: refine ⟨v, fun r hr ↦ mt ?_ hr⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
inst_5 : Module.Finite R M
N : Submodule R M
h : finrank.{u_1, u} R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank.{u_1, u} R (M ⧸ N)
hs' : LinearIndependent.{u, u_1, u} (ι := ↥s) R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s))
v : M
hv : Membership.mem (α := M ⧸ N) s ((N.mkQ : (a : M) → M ⧸ N) v : M ⧸ N)
r : R
hr : r ≠ 0
⊢ r • v ∈ N → r = 0
have this : Eq.{u + 1} (α := M ⧸ N)
    ((Finsupp.linearCombination R (Subtype.val (p := fun (x : M ⧸ N) ↦ x ∈ s)) : (a : ↥s →₀ R) → M ⧸ N)
        (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r) :
      M ⧸ N)
    (0 : M ⧸ N) →
  Eq (α := Finsupp.{u, u_1} (↥s) R)
    (Finsupp.single (Subtype.mk (p := fun (x : M ⧸ N) ↦ x ∈ s) ((N.mkQ : (a : M) → M ⧸ N) v) hv) r :
      Finsupp.{u, u_1} (↥s) R)
    (0 : Finsupp.{u, u_1} (↥s) R)
Tactic: have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)