awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
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
⊢ ∃ (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)
have H₁ : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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
⊢ Membership.mem (γ := Submodule K V) (span K n) x
have simp : ∃ (a : K), Membership.mem (γ := Submodule K V) (span K s) (x + a • v)
Tactic: simp only [n, mem_span_insert']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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
⊢ ∃ (a : K), Membership.mem (γ := Submodule K V) (span K s) (x + a • v)
have 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)
Tactic: use -f x / f v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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
⊢ 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)
have 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
Tactic: simp only [hs, mem_ker, map_add, map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
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
⊢ ∃ (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)
have H₂ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
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 ⋯
⊢ ∃ (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)
have hi : (b : (a : (↑n : Type u_7)) → V) i = v
Tactic: have hi : b i = v := by simp [b, i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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
⊢ ∃ (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)
have refine : f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
Tactic: refine ⟨n, b, i, by simp [b, i], ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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
⊢ f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
have rw : f = HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i)
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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
⊢ f = HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i)
have 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)
Tactic: apply b.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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)
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)
have neg : Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K) (0 : K)
Tactic: suffices f (b j) = 0 by
      simp [Finsupp.single_eq_of_ne h, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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)
h : ¬i = j
⊢ Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K) (0 : K)
have neg : Membership.mem (γ := Submodule K V) (span K s) (_root_.id (↑j : V))
Tactic: rw [← mem_ker, ← hs, Basis.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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)
h : ¬i = j
⊢ Membership.mem (γ := Submodule K V) (span K s) (_root_.id (↑j : V))
have neg : _root_.id (↑j : V) ∈ s
Tactic: apply subset_span
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
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)
h : ¬i = j
⊢ _root_.id (↑j : V) ∈ s
have neg : ¬(↑j : V) = v
Tactic: apply Or.resolve_left (Set.mem_insert_iff.mpr j.prop)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
⊢ (((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have rw : (((B : (a : M) → M →ₗ[R] R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x) :
        M →ₗ[R] R) :
      (a : M) → R)
    y =
  HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
rw :
  (((B : (a : M) → M →ₗ[R] R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x) :
          M →ₗ[R] R) :
        (a : M) → R)
      y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
  HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
rw :
  (((B : (a : M) → M →ₗ[R] R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x) :
          M →ₗ[R] R) :
        (a : M) → R)
      y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have rw₂ : HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have rw : (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) y) =
  HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
  HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have rw₂ : HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B D : BilinForm R M
h :
  Eq (α := (x y : M) → R)
    ((fun (B : BilinForm R M) (x y : M) ↦ ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) B)
    ((fun (B : BilinForm R M) (x y : M) ↦ ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) D)
⊢ B = D
have h₁ : ∀ (x y : M),
  Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: ext x y