awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V' : Type u_1
inst_3 : AddCommGroup V'
inst_4 : Module K V'
inst_5 : FiniteDimensional K V'
f : V →ₗ[K] V'
hinj : Injective.{v + 1, u_1 + 1} (α := V) (β := V') (⇑f : (a : V) → V')
hrank : finrank K V = finrank K V'
⊢ (↑(ofInjectiveOfFinrankEq f hinj hrank) : V →ₗ[K] V') = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
mp : IsUnit f → f.ker = ⊥
mpr : f.ker = ⊥ → IsUnit f
⊢ IsUnit f ↔ f.ker = ⊥

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
u : (V →ₗ[K] V)ˣ
⊢ (↑u : V →ₗ[K] V).ker = ⊥

Tactic:
LinearMap.ker_eq_bot_of_inverse u.inv_mul

Premises used: Units.inv_mul, LinearMap.ker_eq_bot_of_inverse
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
u : (V →ₗ[K] V)ˣ
⊢ (↑u : V →ₗ[K] V).ker = ⊥

Tactic:
exact LinearMap.ker_eq_bot_of_inverse u.inv_mul

Premises used: Units.inv_mul, LinearMap.ker_eq_bot_of_inverse
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : f.ker = ⊥
⊢ Injective (α := V) (β := V) (⇑f : (a : V) → V)

Tactic:
rw [ker_eq_bot] at h_inj

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ IsUnit f

Tactic:
⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap,
      LinearEquiv.ofInjectiveEndo_right_inv f h_inj, LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
      rfl⟩

Premises used: LinearEquiv.symm, IsUnit, LinearEquiv.ofInjectiveEndo_right_inv, LinearEquiv.toLinearMap, Units.mk, Exists.intro, LinearEquiv.ofInjectiveEndo_left_inv, LinearEquiv.ofInjectiveEndo, rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ IsUnit f

Tactic:
exact ⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap,
      LinearEquiv.ofInjectiveEndo_right_inv f h_inj, LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
      rfl⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
rw : f.ker = ⊥ ↔ f.range = ⊤
rw₁ rw₂ : f.range = ⊤ ↔ f.range = ⊤
⊢ IsUnit f ↔ f.range = ⊤

Tactic:
rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]

Premises used: LinearMap.isUnit_iff_ker_eq_bot, LinearMap.ker_eq_bot_iff_range_eq_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
⊢ finrank K V = 0 ↔ ∀ (x : V), x = 0

Tactic:
Module.finrank_zero_iff.trans (subsingleton_iff_forall_eq 0)

Premises used: subsingleton_iff_forall_eq, Iff.trans, OfNat.ofNat, Module.finrank_zero_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
H : x ≠ 0
⊢ Surjective (α := K) (β := K) (⇑(LinearMap.mulLeft F x) : (a : K) → K)

Tactic:
have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
H : x ≠ 0
this : Surjective (α := K) (β := K) (⇑(LinearMap.mulLeft F x) : (a : K) → K)
⊢ ∃ (y : K), x * y = 1

Tactic:
this 1

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
H : x ≠ 0
this : Surjective (α := K) (β := K) (⇑(LinearMap.mulLeft F x) : (a : K) → K)
⊢ ∃ (y : K), x * y = 1

Tactic:
exact this 1

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K_1 : Type u
V : Type v
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
hx : x ≠ 0
rw : x * Classical.choose (p := fun (x_1 : K) ↦ x * x_1 = 1) ⋯ = 1
⊢ (x * if H : x = 0 then 0 else Classical.choose (p := fun (x_1 : K) ↦ x * x_1 = 1) ⋯) = 1

Tactic:
rw [dif_neg hx]

Premises used: dif_neg
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K_1 : Type u
V : Type v
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ x * Classical.choose (p := fun (x_1 : K) ↦ x * x_1 = 1) ⋯ = 1

Tactic:
(Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)

Premises used: Classical.choose_spec, FiniteDimensional.exists_mul_eq_one
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K_1 : Type u
V : Type v
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ x * Classical.choose (p := fun (x_1 : K) ↦ x * x_1 = 1) ⋯ = 1

Tactic:
exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)

Premises used: Classical.choose_spec, FiniteDimensional.exists_mul_eq_one
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Ring K
inst_2 : IsDomain K
inst_3 : Algebra F K
inst_4 : FiniteDimensional F K
x : K
H : x ≠ 0
⊢ IsUnit x

Tactic:
let _ := divisionRingOfFiniteDimensional F K; H.isUnit

Premises used: Ne.isUnit, divisionRingOfFiniteDimensional
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
a : finrank.{u, v} K ↥(K ∙ v) ≤ 1
a₁ : 1 ≤ finrank.{u, v} K ↥(K ∙ v)
⊢ finrank.{u, v} K ↥(K ∙ v) = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ finrank.{u, v} K ↥(K ∙ v) ≤ 1

Tactic:
finrank_span_le_card ({v} : Set V)

Premises used: finrank_span_le_card, Multiset.cons, Multiset.ofList, Finset.card, Multiset.card, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ finrank.{u, v} K ↥(K ∙ v) ≤ 1

Tactic:
exact finrank_span_le_card ({v} : Set V)

Premises used: finrank_span_le_card, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
a : Nontrivial.{v} ↥(K ∙ v)
⊢ 1 ≤ finrank.{u, v} K ↥(K ∙ v)

Tactic:
rw [Nat.succ_le_iff, finrank_pos_iff]

Premises used: Module.finrank_pos_iff, Nat.succ_le_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
h : Ne (α := ↥(K ∙ v)) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v ⋯) 0
⊢ Nontrivial.{v} ↥(K ∙ v)

Tactic:
use ⟨v, mem_span_singleton_self v⟩, 0
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
h : (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v ⋯) : V) ≠ (↑0 : V)
⊢ Ne (α := ↥(K ∙ v)) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v ⋯) 0

Tactic:
apply Subtype.coe_ne_coe.mp

Premises used: Iff.mp, Subtype.coe_ne_coe
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule K V) (K ∙ v) x) v ⋯) : V) ≠ (↑0 : V)

Tactic:
simp [hv]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
⊢ S ≠ ⊥

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
refine_1 : ∀ (hS : IsAtom S), finrank.{u, v} K ↥S = 1
refine_2 : ∀ (hS : finrank.{u, v} K ↥S = 1) (T : Submodule K V) (hT : T < S), T = ⊥
⊢ IsAtom S ↔ finrank.{u, v} K ↥S = 1

Tactic:
refine ⟨fun hS ↦ ?_, fun hS ↦ ⟨by aesop, fun T hT ↦ ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
refine_1 : ∀ (v : V) (hv : v ∈ S) (hv_ne : v ≠ 0), finrank.{u, v} K ↥S = 1
⊢ finrank.{u, v} K ↥S = 1

Tactic:
obtain ⟨v : V, hv : v ∈ S, hv_ne : v ≠ 0⟩ := S.ne_bot_iff.mp hS.ne_bot

Premises used: IsAtom.ne_bot, Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v = S
rw : finrank.{u, v} K ↥(K ∙ v) = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ finrank.{u, v} K ↥S = 1

Tactic:
rw [← this, finrank_span_singleton hv_ne]

Premises used: finrank_span_singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
refine_1 : K ∙ v = S
⊢ finrank.{u, v} K ↥S = 1

Tactic:
suffices K ∙ v = S by rw [← this, finrank_span_singleton hv_ne]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
rw : ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0
⊢ Ne (α := Submodule K V) (K ∙ v) ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Premises used: Submodule.ne_bot_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0

Tactic:
⟨v, mem_span_singleton_self v, hv_ne⟩

Premises used: Submodule.mem_span_singleton_self, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0

Tactic:
exact ⟨v, mem_span_singleton_self v, hv_ne⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ Ne (α := Submodule K V) (K ∙ v) ⊥

Tactic:
have : K ∙ v ≠ ⊥ := by
      rw [Submodule.ne_bot_iff]
      exact ⟨v, mem_span_singleton_self v, hv_ne⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : Ne (α := Submodule K V) (K ∙ v) ⊥
refine_1 : K ∙ v ≤ S
refine_1₁ : {v} ⊆ (↑S : Set V)
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : v ∈ (↑S : Set V)
⊢ K ∙ v = S

Tactic:
rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, IsAtom.le_iff_eq, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
⊢ FiniteDimensional.{u, v} K ↥S

Tactic:
have : FiniteDimensional K S := .of_finrank_eq_succ hS
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this : FiniteDimensional.{u, v} K ↥S
⊢ FiniteDimensional.{u, v} K ↥T

Tactic:
have : FiniteDimensional K T := .of_injective (inclusion hT.le) (inclusion_injective hT.le)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this_1 : FiniteDimensional.{u, v} K ↥S
this : FiniteDimensional.{u, v} K ↥T
refine_2 : finrank.{u, v} K ↥T = 0
⊢ T = ⊥

Tactic:
rw [← finrank_eq_zero (R := K)]

Premises used: Submodule.finrank_eq_zero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this_1 : FiniteDimensional.{u, v} K ↥S
this : FiniteDimensional.{u, v} K ↥T
refine_2 : ∀ (h : ¬finrank.{u, v} K ↥T = 0), False
⊢ finrank.{u, v} K ↥T = 0

Tactic:
by_contra h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this_1 : FiniteDimensional.{u, v} K ↥S
this : FiniteDimensional.{u, v} K ↥T
h : ¬finrank.{u, v} K ↥T = 0
⊢ finrank.{u, v} K ↥S ≤ finrank.{u, v} K ↥T

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Submodule K V
hS : finrank.{u, v} K ↥S = 1
T : Submodule K V
hT : T < S
this_1 : FiniteDimensional.{u, v} K ↥S
this : FiniteDimensional.{u, v} K ↥T
h : ¬finrank.{u, v} K ↥T = 0
⊢ False

Tactic:
exact hT.ne <| eq_of_le_of_finrank_le hT.le <| by lia

Premises used: Submodule.eq_of_le_of_finrank_le, LT.lt.le, LT.lt.ne
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ FiniteDimensional K V

Tactic:
have : FiniteDimensional K V := .of_finrank_eq_succ h
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
h₁ : finrank.{u, v} K ↥(K ∙ x) = finrank K V
⊢ Eq (α := Submodule K V) (K ∙ x) ⊤

Tactic:
apply eq_top_of_finrank_eq

Premises used: Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
h₁ : finrank.{u, v} K ↥(K ∙ x) = 1
⊢ finrank.{u, v} K ↥(K ∙ x) = finrank K V

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank.{u, v} K ↥(K ∙ x) = 1

Tactic:
finrank_span_singleton hx

Premises used: finrank_span_singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ finrank.{u, v} K ↥(K ∙ x) = 1

Tactic:
exact finrank_span_singleton hx

Premises used: finrank_span_singleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ Eq (α := Submodule K V) (K ∙ x) ⊤

Tactic:
have : Submodule.span K {x} = ⊤ := by
    have : FiniteDimensional K V := .of_finrank_eq_succ h
    apply eq_top_of_finrank_eq
    rw [h]
    exact finrank_span_singleton hx
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : Eq (α := Submodule K V) (K ∙ x) ⊤
rw : Membership.mem (γ := Submodule K V) ⊤ y
⊢ Membership.mem (γ := Submodule K V) (K ∙ x) y

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : Eq (α := Submodule K V) (K ∙ x) ⊤
⊢ Membership.mem (γ := Submodule K V) ⊤ y

Tactic:
mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : Eq (α := Submodule K V) (K ∙ x) ⊤
⊢ Membership.mem (γ := Submodule K V) ⊤ y

Tactic:
exact mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : Eq (α := Submodule K V) (K ∙ x) ⊤
⊢ Membership.mem (γ := Submodule K V) (K ∙ x) y

Tactic:
have : y ∈ Submodule.span K {x} := by rw [this]; exact mem_top
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this_1 : Eq (α := Submodule K V) (K ∙ x) ⊤
this : Membership.mem (γ := Submodule K V) (K ∙ x) y
⊢ ∃ (c : K), c • x = y

Tactic:
mem_span_singleton.1 this

Premises used: Submodule.mem_span_singleton, Iff.mp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this_1 : Eq (α := Submodule K V) (K ∙ x) ⊤
this : Membership.mem (γ := Submodule K V) (K ∙ x) y
⊢ ∃ (c : K), c • x = y

Tactic:
exact mem_span_singleton.1 this

Premises used: Submodule.mem_span_singleton, Iff.mp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
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 : Set V
h : s ⊆ t
⊢ Set.finrank K s ≤ Set.finrank K t

Tactic:
Submodule.finrank_mono (span_mono h)

Premises used: Set.finrank, Submodule.span_mono, Submodule.finrank_mono
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
nz : v ≠ 0
h : finrank K V = 1
⊢ Eq (α := Submodule K V) (K ∙ v) ⊤

Tactic:
simpa using (basisSingleton Unit h v nz).span_eq

Premises used: Unit, Module.Basis.span_eq, FiniteDimensional.basisSingleton
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
nz : v ≠ 0
s : Eq (α := Submodule K V) (K ∙ v) ⊤
⊢ LE.le (α := Submodule K V) ⊤ (span K (Set.range ![v]))

Tactic:
simp [← s]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
nz : v ≠ 0
rw : Eq (α := Submodule K V) (K ∙ v) ⊤ ↔ ∀ (w : V), ∃ (c : K), c • v = w
⊢ finrank K V = 1 ↔ ∀ (w : V), ∃ (c : K), c • v = w

Tactic:
rw [finrank_eq_one_iff_of_nonzero v nz]

Premises used: finrank_eq_one_iff_of_nonzero
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
nz : v ≠ 0
⊢ Eq (α := Submodule K V) (K ∙ v) ⊤ ↔ ∀ (w : V), ∃ (c : K), c • v = w

Tactic:
apply span_singleton_eq_top_iff

Premises used: Submodule.span_singleton_eq_top_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Type u_1
A : Type u_2
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : AddCommGroup W
inst_6 : Module K W
inst_7 : Module A W
inst_8 : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
change :
  Surjective.{v + 1, u_1 + 1} (α := V) (β := W)
    (⇑((↑K :
            {S : Type u_2} →
              {M : Type v} →
                {M₂ : Type u_1} →
                  [inst : Semiring K] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module K M] →
                            [inst_13 : Module K M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          f) :
      (a : V) → W)
⊢ Surjective.{v + 1, u_1 + 1} (α := V) (β := W) (⇑f : (a : V) → W)

Tactic:
change Surjective (f.restrictScalars K)

Premises used: LinearMap.restrictScalars, DFunLike.coe, Function.Surjective
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Type u_1
A : Type u_2
inst_3 : Semiring A
inst_4 : Module A V
inst_5 : AddCommGroup W
inst_6 : Module K W
inst_7 : Module A W
inst_8 : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
obtain :
  ∀ (v : V) (n : Ne.{u_1 + 1} (α := W) ((f : (a : V) → W) v : W) ((0 : (a : V) → W) v : W)),
    Surjective.{v + 1, u_1 + 1} (α := V) (β := W)
      (⇑((↑K :
              {S : Type u_2} →
                {M : Type v} →
                  {M₂ : Type u_1} →
                    [inst : Semiring K] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module K M] →
                              [inst_13 : Module K M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
            f) :
        (a : V) → W)
⊢ Surjective.{v + 1, u_1 + 1} (α := V) (β := W)
    (⇑((↑K :
            {S : Type u_2} →
              {M : Type v} →
                {M₂ : Type u_1} →
                  [inst : Semiring K] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module K M] →
                            [inst_13 : Module K M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          f) :
      (a : V) → W)

Tactic:
obtain ⟨v, n⟩ := DFunLike.ne_iff.mp w

Premises used: DFunLike.ne_iff, Iff.mp