awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
h₄ : lift.{u, 0} #(Fin n) = lift.{0, u} (Module.rank R M)
⊢ LinearIndepOn R _root_.id t

Tactic:
rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂

Premises used: Cardinal.mk_range_eq_of_injective, Function.Injective.eq_iff, LinearIndependent.injective, Cardinal.lift_injective
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
h₄ : lift.{u, 0} #(Fin n) = lift.{0, u} (Module.rank R M)
h₅ : LinearIndepOn R _root_.id t
⊢ Set.range v = t

Tactic:
rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂

Premises used: Cardinal.mk_range_eq_of_injective, Function.Injective.eq_iff, LinearIndependent.injective, Cardinal.lift_injective
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : lift.{u, 0} #(Fin n) = lift.{0, u} (Module.rank R M)
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
⊢ (↑n : Cardinal.{u}) = Module.rank R M

Tactic:
simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂

Premises used: Fintype.card_fin, Cardinal.lift_id', Cardinal.mk_fintype, Cardinal.lift_natCast
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ Set.range v ≠ t

Tactic:
have : range v ≠ t := by
    refine fun e ↦ h.ne ?_
    rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂
    simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
this : Set.range v ≠ t
obtain :
  ∀ (x : M) (hx : x ∈ t) (hx' : x ∉ Set.range v),
    ∃ (x : M),
      LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)

Tactic:
obtain ⟨x, hx, hx'⟩ := nonempty_of_ssubset (h₁.ssubset_of_ne this)

Premises used: Set.nonempty_of_ssubset, HasSubset.Subset.ssubset_of_ne
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
this : Set.range v ≠ t
x : M
hx : x ∈ t
hx' : x ∉ Set.range v
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)

Tactic:
⟨x, (linearIndepOn_id_range_iff (Fin.cons_injective_iff.mpr ⟨hx', hv.injective⟩)).mp
    (h₃.mono (Fin.range_cons x v ▸ insert_subset hx h₁))⟩

Premises used: Iff.mpr, Eq.rec, linearIndepOn_id_range_iff, LinearIndependent.injective, LinearIndepOn.mono, Fin.range_cons, And.intro, Exists.intro, Iff.mp, Fin.cons_injective_iff, Eq.symm, Set.insert_subset
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
this : Set.range v ≠ t
x : M
hx : x ∈ t
hx' : x ∉ Set.range v
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)

Tactic:
exact ⟨x, (linearIndepOn_id_range_iff (Fin.cons_injective_iff.mpr ⟨hx', hv.injective⟩)).mp
    (h₃.mono (Fin.range_cons x v ▸ insert_subset hx h₁))⟩
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
simp :
  ∃ (x : M),
    LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) v x)

Tactic:
simp only [Fin.snoc_eq_cons_rotate]

Premises used: Fin.snoc_eq_cons_rotate
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
have :
  ∀ (x : M)
    (hx : LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)),
    ∃ (x : M),
      LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
        Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)
⊢ ∃ (x : M),
    LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)

Tactic:
have ⟨x, hx⟩ := exists_linearIndependent_cons_of_lt_rank hv h
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
x : M
hx : LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
⊢ ∃ (x : M),
    LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)

Tactic:
⟨x, hx.comp _ (finRotate _).injective⟩

Premises used: finRotate, Exists.intro, Equiv.injective, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
x : M
hx : LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
⊢ ∃ (x : M),
    LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)

Tactic:
exact ⟨x, hx.comp _ (finRotate _).injective⟩
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
obtain :
  ∀ (y : M)
    (hy :
      LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
        (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)),
    ∃ (y : M), LinearIndependent R ![x, y]
⊢ ∃ (y : M), LinearIndependent R ![x, y]

Tactic:
obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (.of_subsingleton (v := ![x]) 0 hx) h

Premises used: LinearIndependent.of_subsingleton, exists_linearIndependent_snoc_of_lt_rank, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy :
  LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
    (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy :
  LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
    (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]

Tactic:
have : Fin.snoc ![x] y = ![x, y] := by simp
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy :
  LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
    (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)
this : Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]
⊢ LinearIndependent R ![x, y]

Tactic:
rw [this] at hy
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy :
  LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
    (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)
this : Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]
hy₁ : LinearIndependent R ![x, y]
⊢ Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]

Tactic:
rw [this] at hy
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R ![x, y]
this : Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]
⊢ ∃ (y : M), LinearIndependent R ![x, y]

Tactic:
⟨y, hy⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy : LinearIndependent R ![x, y]
this : Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]
⊢ ∃ (y : M), LinearIndependent R ![x, y]

Tactic:
exact ⟨y, hy⟩
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
e : Module.rank R (M ⧸ N) = 0
⊢ Module.rank R ↥N < Module.rank R ↥N

Tactic:
rw [← rank_quotient_add_rank N, e, zero_add] at h

Premises used: Submodule.rank_quotient_add_rank, zero_add
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
e : Module.rank R (M ⧸ N) = 0
h₁ : Module.rank R ↥N < Module.rank R ↥N
⊢ Module.rank R (M ⧸ N) = 0

Tactic:
rw [← rank_quotient_add_rank N, e, zero_add] at h

Premises used: Submodule.rank_quotient_add_rank, zero_add
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R ↥N
e : Module.rank R (M ⧸ N) = 0
⊢ False

Tactic:
h.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R ↥N
e : Module.rank R (M ⧸ N) = 0
⊢ False

Tactic:
exact h.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ Module.rank R (M ⧸ N) ≠ 0

Tactic:
have : Module.rank R (M ⧸ N) ≠ 0 := by
    intro e
    rw [← rank_quotient_add_rank N, e, zero_add] at h
    exact h.ne rfl
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : Module.rank R (M ⧸ N) ≠ 0
⊢ ¬∀ (x : M), ∃ (a : R), a ≠ 0 ∧ HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) = 0

Tactic:
rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this

Premises used: Function.Surjective.forall, ne_eq, Submodule.Quotient.mk_surjective, rank_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ¬∀ (x : M), ∃ (a : R), a ≠ 0 ∧ HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) = 0
⊢ ∃ (x : M), ∀ (a : R) (_ : a ≠ 0), HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) ≠ 0

Tactic:
push Not at this

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ (x : M), ∀ (a : R) (_ : a ≠ 0), HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) ≠ 0
⊢ ∃ (x : M), ∀ (a : R) (_ : ¬a = 0), a • x ∉ N

Tactic:
simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this

Premises used: Submodule.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero, map_smul
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ (x : M), ∀ (a : R) (_ : ¬a = 0), a • x ∉ N
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
this
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ (x : M), ∀ (a : R) (_ : ¬a = 0), a • x ∉ N
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
exact this
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
enter : Module.rank R ↥t
| Module.rank R ↥s + Module.rank R ↥t

Tactic:
enter [2]
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
⊢ t = (s ⊔ t) ⊓ t

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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) ⊓ t)
| Module.rank R ↥t

Tactic:
rw [show t = (s ⊔ t) ⊓ t by simp]
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
enter : Module.rank R ↥((s ⊔ t) ⊓ t)
| Module.rank R ↥s + Module.rank R ↥t

Tactic:
enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
conv_rhs : Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t

Tactic:
conv_rhs => enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t

Tactic:
rw [← Submodule.rank_sup_add_rank_inf_eq]

Premises used: Submodule.rank_sup_add_rank_inf_eq
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 ⊔ t) + Module.rank R ↥(s ⊓ t)

Tactic:
self_le_add_right _ _

Premises used: self_le_add_right
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 ⊔ t) + Module.rank R ↥(s ⊓ t)

Tactic:
exact self_le_add_right _ _

Premises used: self_le_add_right
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : n < finrank R M
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) v x)

Tactic:
exists_linearIndependent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h)

Premises used: Module.lt_rank_of_lt_finrank, exists_linearIndependent_snoc_of_lt_rank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : n < finrank R M
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)

Tactic:
exists_linearIndependent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h)

Premises used: exists_linearIndependent_cons_of_lt_rank, Module.lt_rank_of_lt_finrank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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 : IsDomain R
inst_6 : IsTorsionFree R M
h : 1 < finrank R M
x : M
hx : x ≠ 0
⊢ ∃ (y : M), LinearIndependent R ![x, y]

Tactic:
exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx

Premises used: Module.one_lt_rank_of_one_lt_finrank, exists_linearIndependent_pair_of_one_lt_rank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
rw : Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
⊢ finrank.{u_1, u} R (M ⧸ N) + finrank.{u_1, u} R ↥N = finrank R M

Tactic:
rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
    Submodule.finrank_eq_rank]

Premises used: Nat.cast_inj, Module.finrank_eq_rank, Nat.cast_add, Submodule.finrank_eq_rank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Tactic:
HasRankNullity.rank_quotient_add_rank _

Premises used: HasRankNullity.rank_quotient_add_rank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Tactic:
exact HasRankNullity.rank_quotient_add_rank _

Premises used: HasRankNullity.rank_quotient_add_rank
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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
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
⊢ finrank.{u_2, u} R (M ⧸ N) = finrank R M - finrank.{u_2, u} R ↥N

Tactic:
rw [← (N.restrictScalars R).finrank_quotient_add_finrank]

Premises used: Submodule.finrank_quotient_add_finrank, Submodule.restrictScalars
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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.{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:
Nat.eq_sub_of_add_eq rfl

Premises used: Nat.eq_sub_of_add_eq, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.RankNullity
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.{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:
exact Nat.eq_sub_of_add_eq rfl

Premises used: Nat.eq_sub_of_add_eq, rfl