awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
hp : p < ⊤
rcases : ∀ (v : V) (hpv : v ∉ p), ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker
⊢ ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker

Tactic:
rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩

Premises used: SetLike.exists_of_lt
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
rcases :
  ∀ (f : V →ₗ[K] K) (hfv : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)) (hpf : p ≤ f.ker),
    ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker
⊢ ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker

Tactic:
rcases exists_le_ker_of_notMem hpv with ⟨f, hfv, hpf⟩

Premises used: Submodule.exists_le_ker_of_notMem
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hfv : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hpf : p ≤ f.ker
⊢ ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker

Tactic:
⟨f, ne_of_apply_ne (· v) hfv, hpf⟩

Premises used: ne_of_apply_ne, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hfv : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
hpf : p ≤ f.ker
⊢ ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker

Tactic:
exact ⟨f, ne_of_apply_ne (· v) hfv, hpf⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
⊢ Nonempty.{u_4 + 1} (((V ⧸ p) × ↥p) ≃ₗ[K] V)

Tactic:
let ⟨q, hq⟩ := p.exists_isCompl
  Nonempty.intro <|
    ((quotientEquivOfIsCompl p q hq).prodCongr (LinearEquiv.refl _ _)).trans
      (prodEquivOfIsCompl q p hq.symm)

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.prodCongr, _private.0.quotient_prod_linearEquiv.match_1, Membership.mem, Subtype, Submodule.quotientEquivOfIsCompl, Nonempty.intro, HasQuotient.Quotient, Submodule.exists_isCompl, LinearEquiv, Nonempty, LinearEquiv.refl, Prod, RingHom.id, LinearEquiv.trans, IsCompl.symm
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
simp :
  map f.ker.subtype
      (span K
        (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
          (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))) =
    f.ker
⊢ span K s = f.ker

Tactic:
simp only [s, span_image]

Premises used: Submodule.span_image
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
⊢ map f.ker.subtype
      (span K
        (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
          (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))) =
    f.ker

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
⊢ span K s = f.ker

Tactic:
have hs : span K s = ker f := by
    simp only [s, span_image]
    simp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
hs₁ : LinearIndepOn K _root_.id s
hx : v ∉ span K s
⊢ LinearIndepOn K _root_.id n

Tactic:
apply LinearIndepOn.id_insert

Premises used: LinearIndepOn.id_insert
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
hs₁ :
  LinearIndepOn.{u_7, u_6, u_7} (ι := ↥f.ker) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs₂ :
  Disjoint
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
        (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker)))
    f.ker.subtype.ker
⊢ LinearIndepOn K _root_.id s

Tactic:
apply LinearIndepOn.image

Premises used: LinearIndepOn.image
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ LinearIndepOn.{u_7, u_6, u_7} (ι := ↥f.ker) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))

Tactic:
b₁.linearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ LinearIndepOn.{u_7, u_6, u_7} (ι := ↥f.ker) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))

Tactic:
exact b₁.linearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ Disjoint
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
        (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker)))
    f.ker.subtype.ker

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ v ∉ span K s

Tactic:
simp [hs, hfv]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ LinearIndepOn K _root_.id n

Tactic:
have H₁ : LinearIndepOn K _root_.id n := by
    apply LinearIndepOn.id_insert
    · apply LinearIndepOn.image
      · exact b₁.linearIndependent.linearIndepOn_id
      · simp
    · simp [hs, hfv]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
x : V
simp : ∃ (a : K), Membership.mem (γ := Submodule K V) (span K s) (x + a • v)
⊢ Membership.mem (γ := Submodule K V) (span K n) x

Tactic:
simp only [n, mem_span_insert']

Premises used: Submodule.mem_span_insert'
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
x : V
h :
  Membership.mem (γ := Submodule K V) (span K s)
    (x + HDiv.hDiv (α := K) (β := K) (-(f : (a : V) → K) x : K) ((f : (a : V) → K) v : K) • v)
⊢ ∃ (a : K), Membership.mem (γ := Submodule K V) (span K s) (x + a • v)

Tactic:
use -f x / f v

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
x : V
h :
  HAdd.hAdd (α := K) ((f : (a : V) → K) x : K)
      (HMul.hMul (β := K) (HDiv.hDiv (α := K) (β := K) (-(f : (a : V) → K) x : K) ((f : (a : V) → K) v : K))
        ((f : (a : V) → K) v : K)) =
    0
⊢ Membership.mem (γ := Submodule K V) (span K s)
    (x + HDiv.hDiv (α := K) (β := K) (-(f : (a : V) → K) x : K) ((f : (a : V) → K) v : K) • v)

Tactic:
simp only [hs, mem_ker, map_add, map_smul, smul_eq_mul]

Premises used: map_add, LinearMap.mem_ker, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
x : V
⊢ HAdd.hAdd (α := K) ((f : (a : V) → K) x : K)
      (HMul.hMul (β := K) (HDiv.hDiv (α := K) (β := K) (-(f : (a : V) → K) x : K) ((f : (a : V) → K) v : K))
        ((f : (a : V) → K) v : K)) =
    0

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
⊢ LE.le (α := Submodule K V) ⊤ (span K n)

Tactic:
have H₂ : ⊤ ≤ span K n := by
    rintro x -
    simp only [n, mem_span_insert']
    use -f x / f v
    simp only [hs, mem_ker, map_add, map_smul, smul_eq_mul]
    field
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
⊢ LE.le.{u_7} (α := Submodule K V) ⊤ (span K (Set.range fun (x : (↑n : Type u_7)) ↦ _root_.id (↑x : V)))

Tactic:
simpa using H₂
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
⊢ (b : (a : (↑n : Type u_7)) → V) i = v

Tactic:
simp [b, i]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
⊢ (b : (a : (↑n : Type u_7)) → V) i = v

Tactic:
have hi : b i = v := by simp [b, i]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
⊢ v = (b : (a : (↑n : Type u_7)) → V) i

Tactic:
simp [b, i]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
refine : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
⊢ ∃ (n : Set V) (b : Basis (↑n : Type u_7) K V) (i : (↑n : Type u_7)),
    v = (b : (a : (↑n : Type u_7)) → V) i ∧ f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)

Tactic:
refine ⟨n, b, i, by simp [b, i], ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
rw : f = HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i)
⊢ f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)

Tactic:
rw [← hi]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
apply :
  ∀ (i_1 : (↑n : Type u_7)),
    Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i_1 : V) : K)
      ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
          ((b : (a : (↑n : Type u_7)) → V) i_1 : V) :
        K)
⊢ f = HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i)

Tactic:
apply b.ext

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
pos :
  ∀ (h : i = j),
    Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K)
      ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
          ((b : (a : (↑n : Type u_7)) → V) j : V) :
        K)
neg :
  ∀ (h : ¬i = j),
    Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K)
      ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
          ((b : (a : (↑n : Type u_7)) → V) j : V) :
        K)
⊢ Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K)
    ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
        ((b : (a : (↑n : Type u_7)) → V) j : V) :
      K)

Tactic:
by_cases h : i = j