awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
rw : finrank.{u, v} K ↥(s ⊔ t) ≤ finrank K V
⊢ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t ≤ finrank K V

Tactic:
rw [← Submodule.finrank_sup_add_finrank_inf_eq s t, hdisjoint.eq_bot, finrank_bot, add_zero]

Premises used: Submodule.finrank_sup_add_finrank_inf_eq, finrank_bot, add_zero, Disjoint.eq_bot
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank.{u, v} K ↥(s ⊔ t) ≤ finrank K V

Tactic:
Submodule.finrank_le _

Premises used: Submodule.finrank_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank.{u, v} K ↥(s ⊔ t) ≤ finrank K V

Tactic:
exact Submodule.finrank_le _

Premises used: Submodule.finrank_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
⊢ s ⊓ t = ⊥

Tactic:
rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint

Premises used: le_bot_iff, disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : s ⊓ t = ⊥
rw : finrank.{u, v} K ↥⊥ = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ finrank.{u, v} K ↥(s ⊓ t) = 0

Tactic:
rw [hdisjoint, finrank_bot]

Premises used: finrank_bot
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
⊢ finrank.{u, v} K ↥(s ⊓ t) = 0

Tactic:
have h_finrank_inf : finrank K ↑(s ⊓ t) = 0 := by
    rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
    rw [hdisjoint, finrank_bot]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
h : finrank.{u, v} K ↥(s ⊔ t) = finrank K V
⊢ s ⊔ t = ⊤

Tactic:
apply eq_top_of_finrank_eq

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
⊢ finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t

Tactic:
replace hdim : finrank K V = finrank K s + finrank K t :=
    le_antisymm hdim (finrank_add_finrank_le_of_disjoint hdisjoint)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank K V

Tactic:
rw [hdim]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
⊢ finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t

Tactic:
s.finrank_sup_add_finrank_inf_eq t

Premises used: Submodule.finrank_sup_add_finrank_inf_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t

Tactic:
convert! s.finrank_sup_add_finrank_inf_eq t

Premises used: Submodule.finrank_sup_add_finrank_inf_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank.{u, v} K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
h : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + 0
h₁ h₂ : finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t)
⊢ finrank.{u, v} K ↥(s ⊔ t) = finrank.{u, v} K ↥(s ⊔ t) + finrank.{u, v} K ↥(s ⊓ t)

Tactic:
rw [h_finrank_inf, add_zero]

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank.{u, v} K ↥s + finrank.{u, v} K ↥t
⊢ IsCompl s t ↔ Disjoint s t

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h, codisjoint_iff.mpr <| eq_top_of_disjoint s t hdim h⟩⟩

Premises used: Iff.mpr, codisjoint_iff, Submodule.eq_top_of_disjoint, Iff.intro, IsCompl.mk, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
⊢ W ⊔ K ∙ v = ⊤ ↔ finrank.{u, v} K (V ⧸ W) = 1

Tactic:
⟨fun hW ↦ ?_, fun hW ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
refine_1 : ∀ (hW : W ⊔ K ∙ v = ⊤), finrank.{u, v} K (V ⧸ W) = 1
refine_2 : ∀ (hW : finrank.{u, v} K (V ⧸ W) = 1), W ⊔ K ∙ v = ⊤
⊢ W ⊔ K ∙ v = ⊤ ↔ finrank.{u, v} K (V ⧸ W) = 1

Tactic:
refine ⟨fun hW ↦ ?_, fun hW ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
⊢ v ≠ 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
⊢ v ≠ 0

Tactic:
have hv₀ : v ≠ 0 := by aesop
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
⊢ finrank.{u, v} K ↥(W ⊔ K ∙ v) + finrank.{u, v} K ↥(W ⊓ K ∙ v) = finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)

Tactic:
have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
aux : finrank.{u, v} K ↥(W ⊔ K ∙ v) + finrank.{u, v} K ↥(W ⊓ K ∙ v) = finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
⊢ finrank.{u, v} K (V ⧸ W) + finrank.{u, v} K ↥W + 0 = finrank.{u, v} K ↥W + 1

Tactic:
rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
        ← finrank_quotient_add_finrank W] at aux

Premises used: Submodule.finrank_quotient_add_finrank, finrank_top, finrank_span_singleton, finrank_bot
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
aux : finrank.{u, v} K (V ⧸ W) + finrank.{u, v} K ↥W + 0 = finrank.{u, v} K ↥W + 1
⊢ finrank.{u, v} K (V ⧸ W) = 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
refine_1 : W ⊓ K ∙ v = ⊥
⊢ finrank.{u, v} K (V ⧸ W) = 1

Tactic:
suffices W ⊓ span K {v} = ⊥ by
      have hv₀ : v ≠ 0 := by aesop
      have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
      rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
        ← finrank_quotient_add_finrank W] at aux
      lia
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
⊢ W ⊓ K ∙ v = ⊥

Tactic:
(Submodule.eq_bot_iff _).mpr fun w hw ↦ ?_

Premises used: Iff.mpr, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
refine_1 : ∀ (w : V) (hw : w ∈ W ⊓ K ∙ v), w = 0
⊢ W ⊓ K ∙ v = ⊥

Tactic:
refine (Submodule.eq_bot_iff _).mpr fun w hw ↦ ?_

Premises used: Iff.mpr, Submodule.eq_bot_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
w : V
hw : w ∈ W ⊓ K ∙ v
⊢ w ∈ W ∧ ∃ (t : K), t • v = w

Tactic:
simpa [mem_span_singleton] using hw

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
w : V
hw : w ∈ W ⊓ K ∙ v
refine_1 : ∀ (t : K) (hw : t • v ∈ W ⊓ K ∙ v) (ht : t • v ∈ W), t • v = 0
⊢ w = 0

Tactic:
obtain ⟨ht, t, rfl⟩ : w ∈ W ∧ ∃ t : K, t • v = w := by simpa [mem_span_singleton] using hw

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
refine_1 :
  ∀ (hw : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W ⊓ K ∙ v) (ht : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W),
    HSMul.hSMul.{u, v, v} (α := K) 0 v = 0
refine_1₁ : ∀ (ht₀ : t ≠ 0), t • v = 0
⊢ t • v = 0

Tactic:
rcases eq_or_ne t 0 with rfl | ht₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
hw : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W ⊓ K ∙ v
ht : HSMul.hSMul.{u, v, v} (α := K) 0 v ∈ W
⊢ HSMul.hSMul.{u, v, v} (α := K) 0 v = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
ht₀ : t ≠ 0
⊢ v ∈ W

Tactic:
rw [Submodule.smul_mem_iff _ ht₀] at ht

Premises used: Submodule.smul_mem_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
ht₀ : t ≠ 0
ht₁ : v ∈ W
⊢ t ≠ 0

Tactic:
rw [Submodule.smul_mem_iff _ ht₀] at ht

Premises used: Submodule.smul_mem_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : v ∈ W
ht₀ : t ≠ 0
⊢ t • v = 0

Tactic:
contradiction
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
refine_2 : finrank K V ≤ finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)
refine_2₁ : Disjoint W (K ∙ v)
⊢ W ⊔ K ∙ v = ⊤

Tactic:
apply Submodule.eq_top_of_disjoint

Premises used: Submodule.eq_top_of_disjoint
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
refine_2 : 1 ≤ finrank.{u, v} K ↥(K ∙ v)
⊢ finrank K V ≤ finrank.{u, v} K ↥W + finrank.{u, v} K ↥(K ∙ v)

Tactic:
rw [← W.finrank_quotient_add_finrank, add_comm, add_le_add_iff_left, hW]

Premises used: Submodule.finrank_quotient_add_finrank, add_le_add_iff_left, add_comm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
⊢ 1 ≤ finrank.{u, v} K ↥(K ∙ v)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
⊢ Disjoint W (K ∙ v)

Tactic:
Submodule.disjoint_span_singleton_of_notMem hv

Premises used: Submodule.disjoint_span_singleton_of_notMem
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank.{u, v} K (V ⧸ W) = 1
⊢ Disjoint W (K ∙ v)

Tactic:
exact Submodule.disjoint_span_singleton_of_notMem hv

Premises used: Submodule.disjoint_span_singleton_of_notMem
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ v ≠ 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
rw : p ⊓ K ∙ v ≤ ⊥
⊢ finrank.{u, v} K ↥(p ⊔ K ∙ v) = finrank.{u, v} K ↥p + 1

Tactic:
rw [← Nat.add_left_inj, finrank_sup_add_finrank_inf_eq, add_assoc,
    Nat.add_left_cancel_iff, finrank_span_singleton (by aesop),
    Nat.left_eq_add, Submodule.finrank_eq_zero, eq_bot_iff]

Premises used: Submodule.finrank_sup_add_finrank_inf_eq, Nat.left_eq_add, add_assoc, Nat.add_left_cancel_iff, Submodule.finrank_eq_zero, finrank_span_singleton, eq_bot_iff, Nat.add_left_inj
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
simp : (x ∈ p ∧ ∃ (a : K), a • v = x) → Membership.mem (γ := Submodule K V) ⊥ x
⊢ x ∈ p ⊓ K ∙ v → Membership.mem (γ := Submodule K V) ⊥ x

Tactic:
simp only [mem_inf, mem_span_singleton]

Premises used: Submodule.mem_span_singleton, Submodule.mem_inf
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
hx : x ∈ p
a : K
hx' : a • v = x
⊢ a • v ∈ p

Tactic:
rw [← hx'] at hx
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
hx : x ∈ p
a : K
hx' : a • v = x
hx₁ : a • v ∈ p
⊢ a • v = x

Tactic:
rw [← hx'] at hx
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
this : a = 0
⊢ Membership.mem (γ := Submodule K V) ⊥ x

Tactic:
simp [← hx', this]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
suffices : a = 0
⊢ Membership.mem (γ := Submodule K V) ⊥ x

Tactic:
suffices a = 0 by simp [← hx', this]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
contrapose : ∀ (hv : ¬a = 0), v ∈ p
⊢ a = 0

Tactic:
contrapose hv
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
p : Submodule K V
v x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
hv : ¬a = 0
⊢ v ∈ p

Tactic:
simpa [smul_mem_iff p hv] using hx

Premises used: Submodule.smul_mem_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h : W = ⊤
rw : finrank.{u, v} K ↥⊤ = finrank K V
rw₁ rw₂ : finrank K V = finrank K V
⊢ finrank.{u, v} K ↥W = finrank K V

Tactic:
rw [h, finrank_top]

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
refine : ∀ (h : finrank.{u, v} K ↥W = finrank K V), W = ⊤
⊢ W = ⊤ ↔ finrank.{u, v} K ↥W = finrank K V

Tactic:
refine ⟨fun h ↦ by rw [h, finrank_top], fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h : finrank.{u, v} K ↥W = finrank K V
apply : finrank.{u, v} K ↥W = finrank.{u, v} K ↥⊤
⊢ W = ⊤

Tactic:
apply eq_of_le_of_finrank_eq le_top

Premises used: le_top, Submodule.eq_of_le_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
W : Submodule K V
h rw : finrank.{u, v} K ↥W = finrank K V
rw₁ rw₂ : finrank K V = finrank K V
⊢ finrank.{u, v} K ↥W = finrank.{u, v} K ↥⊤

Tactic:
rw [finrank_top, h]

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : LinearEquiv.{u, u, v, v'} (RingHom.id K) ↥p ↥q
f₂ : V ≃ₗ[K] V₂
rw : finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₁ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v} K ↥p
rw₂ : finrank K V = finrank.{u, v'} K (V₂ ⧸ q) + finrank.{u, v'} K ↥q
rw₃ : finrank K V = finrank K V₂
rw₄ rw₅ : finrank K V₂ = finrank K V₂
⊢ finrank.{u, v} K (V ⧸ p) = finrank.{u, v'} K (V₂ ⧸ q)

Tactic:
rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]

Premises used: Submodule.finrank_quotient_add_finrank, LinearEquiv.finrank_eq, add_right_cancel_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
rw : finrank.{u, v} K (V ⧸ q) + finrank.{u, v} K ↥q = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₁ : ℕ
rw₂ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K ↥q
rw₃ : finrank K V = finrank.{u, v} K ↥p + finrank.{u, v} K (V ⧸ p)
rw₄ : finrank K V = finrank.{u, v} K (V ⧸ p) + finrank.{u, v} K ↥p
rw₅ rw₆ : finrank K V = finrank K V
⊢ finrank.{u, v} K (V ⧸ q) = finrank.{u, v} K ↥p

Tactic:
rw [← add_right_cancel_iff, Submodule.finrank_quotient_add_finrank, ← LinearEquiv.finrank_eq f,
      add_comm, Submodule.finrank_quotient_add_finrank]

Premises used: Submodule.finrank_quotient_add_finrank, LinearEquiv.finrank_eq, add_comm, add_right_cancel_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
f : V →ₗ[K] V₂
rw : finrank.{u, v} K (V ⧸ f.ker) + finrank.{u, v} K ↥f.ker = finrank K V
⊢ finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V

Tactic:
rw [← f.quotKerEquivRange.finrank_eq]

Premises used: LinearEquiv.finrank_eq, LinearMap.quotKerEquivRange
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
f : V →ₗ[K] V₂
⊢ finrank.{u, v} K (V ⧸ f.ker) + finrank.{u, v} K ↥f.ker = finrank K V

Tactic:
Submodule.finrank_quotient_add_finrank _

Premises used: Submodule.finrank_quotient_add_finrank, Set.Mem
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
f : V →ₗ[K] V₂
⊢ finrank.{u, v} K (V ⧸ f.ker) + finrank.{u, v} K ↥f.ker = finrank K V

Tactic:
exact Submodule.finrank_quotient_add_finrank _

Premises used: Submodule.finrank_quotient_add_finrank
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : FiniteDimensional K V
inst_6 : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
⊢ finrank.{u, v'} K ↥f.range + finrank.{u, v} K ↥f.ker = finrank K V

Tactic:
have h₁ := f.finrank_range_add_finrank_ker