awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
x : ↥A
i : ι
this :
  Eq (α := ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A : Submodule ℤ M) →ₗ[ℤ] ι →₀ R)
    (mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (↑(addSubgroupOfClosure A b h).repr :
        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A) →ₗ[ℤ] ι →₀ ℤ))
    (LinearMap.domRestrict
      ((↑ℤ :
          {S : Type u_8} →
            {M : Type u_7} →
              {M₂ : Type (max u_8 u_9)} →
                [inst : Semiring ℤ] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module ℤ M] →
                          [inst_9 : Module ℤ M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (↑b.repr : M →ₗ[R] ι →₀ R))
      ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))
⊢ Eq.{u_8 + 1} (α := R)
    ((↑(((((addSubgroupOfClosure A b h).repr :
                    (a : ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)) → ι →₀ ℤ)
                  x :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        R) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) (↑x : M) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this x) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
x : ↥A
i : ι
suffices :
  Eq (α := ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A : Submodule ℤ M) →ₗ[ℤ] ι →₀ R)
    (mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (↑(addSubgroupOfClosure A b h).repr :
        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A) →ₗ[ℤ] ι →₀ ℤ))
    (LinearMap.domRestrict
      ((↑ℤ :
          {S : Type u_8} →
            {M : Type u_7} →
              {M₂ : Type (max u_8 u_9)} →
                [inst : Semiring ℤ] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module ℤ M] →
                          [inst_9 : Module ℤ M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (↑b.repr : M →ₗ[R] ι →₀ R))
      ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))
⊢ Eq.{u_8 + 1} (α := R)
    ((↑(((((addSubgroupOfClosure A b h).repr :
                    (a : ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)) → ι →₀ ℤ)
                  x :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        R) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) (↑x : M) : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
suffices Finsupp.mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (b.addSubgroupOfClosure A h).repr.toLinearMap =
        ((b.repr : M →ₗ[R] ι →₀ R).restrictScalars ℤ).domRestrict A.toIntSubmodule by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
x : ↥A
i x_1 : ι
⊢ Eq (α := ι →₀ R)
    ((mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
            (↑(addSubgroupOfClosure A b h).repr :
              ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A) →ₗ[ℤ] ι →₀ ℤ) :
          (a : ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)) → ι →₀ R)
        ((addSubgroupOfClosure A b h :
            (a : ι) → ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))
          x_1) :
      ι →₀ R)
    ((LinearMap.domRestrict
            ((↑ℤ :
                {S : Type u_8} →
                  {M : Type u_7} →
                    {M₂ : Type (max u_8 u_9)} →
                      [inst : Semiring ℤ] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module ℤ M] →
                                [inst_9 : Module ℤ M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (↑b.repr : M →ₗ[R] ι →₀ R))
            ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A) :
          (a : ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A)) → ι →₀ R)
        ((addSubgroupOfClosure A b h :
            (a : ι) → ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))
          x_1) :
      ι →₀ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
M : Type u_7
R : Type u_8
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsAddTorsionFree R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range.{u_7, u_9 + 1} (ι := ι) (⇑b : (a : ι) → M))
x : ↥A
i : ι
⊢ Eq (α := ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A : Submodule ℤ M) →ₗ[ℤ] ι →₀ R)
    (mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (↑(addSubgroupOfClosure A b h).repr :
        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A) →ₗ[ℤ] ι →₀ ℤ))
    (LinearMap.domRestrict
      ((↑ℤ :
          {S : Type u_8} →
            {M : Type u_7} →
              {M₂ : Type (max u_8 u_9)} →
                [inst : Semiring ℤ] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module ℤ M] →
                          [inst_9 : Module ℤ M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
        (↑b.repr : M →ₗ[R] ι →₀ R))
      ((AddSubgroup.toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) A))

Tactic:
exact (b.addSubgroupOfClosure A h).ext fun _ ↦ by simp

Premises used: Module.Basis.addSubgroupOfClosure, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
hs : LinearIndepOn K id s
⊢ (↑⊤ : Set V) ⊆ (↑(span K (range ((hs.extend (s := s) (t := univ) ⋯).restrict (π := fun (a : V) ↦ V) id))) : Set V)

Tactic:
simpa using hs.subset_span_extend (subset_univ s)

Premises used: Set.subset_univ, LinearIndepOn.subset_span_extend
-- 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
s : Set V
hs : LinearIndepOn K id s
x : (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4)
⊢ (extend (s := s) hs : (a : (↑(hs.extend ⋯) : Type u_4)) → V) x = (↑x : V)

Tactic:
Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply, Set.restrict
-- 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
s : Set V
hs : LinearIndepOn K id s
⊢ Eq.{u_4 + 1} (α := (a : (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4)) → V)
    (⇑(extend (s := s) hs) : (a : (↑(hs.extend ⋯) : Type u_4)) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := univ) ⋯))

Tactic:
funext (extend_apply_self hs)

Premises used: Module.Basis.extend_apply_self, funext
-- 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
s : Set V
hs : LinearIndepOn K id s
rw :
  range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := univ) ⋯)) =
    hs.extend (s := s) (t := univ) ⋯
rw₁ : {x : V | x ∈ hs.extend (s := s) (t := univ) ⋯} = hs.extend (s := s) (t := univ) ⋯
rw₂ rw₃ : hs.extend (s := s) (t := univ) ⋯ = hs.extend (s := s) (t := univ) ⋯
⊢ range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (⇑(extend (s := s) hs) : (a : (↑(hs.extend ⋯) : Type u_4)) → V) =
    hs.extend (s := s) (t := univ) ⋯

Tactic:
rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, Module.Basis.coe_extend
-- 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
s : Set V
hs : LinearIndepOn K id s
⊢ s ⊆ hs.extend (s := s) (t := univ) ⋯

Tactic:
hs.subset_extend _

Premises used: LinearIndepOn.subset_extend
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
⊢ t ⊆ (↑(span K (range fun (x : (↑(hs.extend (s := s) (t := t) hst) : Type u_4)) ↦ id (↑x : V))) : Set V)

Tactic:
simpa using hs.subset_span_extend hst

Premises used: LinearIndepOn.subset_span_extend
-- 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
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
x : (↑(hs.extend (s := s) (t := t) hst) : Type u_4)
⊢ (extendLe (s := s) (t := t) hs hst ht : (a : (↑(hs.extend hst) : Type u_4)) → V) x = (↑x : V)

Tactic:
Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply
-- 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
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
⊢ Eq.{u_4 + 1} (α := (a : (↑(hs.extend (s := s) (t := t) hst) : Type u_4)) → V)
    (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := t) hst))

Tactic:
funext (extendLe_apply_self hs hst ht)

Premises used: funext, Module.Basis.extendLe_apply_self
-- 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
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
rw :
  range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := t) hst)) =
    hs.extend (s := s) (t := t) hst
rw₁ : {x : V | x ∈ hs.extend (s := s) (t := t) hst} = hs.extend (s := s) (t := t) hst
rw₂ rw₃ : hs.extend (s := s) (t := t) hst = hs.extend (s := s) (t := t) hst
⊢ range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V) =
    hs.extend (s := s) (t := t) hst

Tactic:
rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Module.Basis.coe_extendLe, Subtype.range_coe_subtype, Set.setOf_mem_eq
-- 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
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
⊢ s ⊆
    range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V)

Tactic:
(range_extendLe hs hst ht).symm ▸ hs.subset_extend hst

Premises used: Module.Basis.range_extendLe, Eq.rec, LinearIndepOn.subset_extend, Eq.symm
-- 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
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
⊢ range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V) ⊆
    t

Tactic:
(range_extendLe hs hst ht).symm ▸ hs.extend_subset hst

Premises used: LinearIndepOn.extend_subset, Module.Basis.range_extendLe, Eq.rec, Eq.symm
-- 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
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
x : (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4)
⊢ (ofSpan (s := s) hs : (a : (↑(⋯.extend ⋯) : Type u_4)) → V) x = (↑x : V)

Tactic:
extendLe_apply_self (linearIndependent_empty K V) (empty_subset s) hs x

Premises used: Set.empty_subset, Module.Basis.extendLe_apply_self, linearIndependent_empty
-- 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
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
⊢ Eq.{u_4 + 1} (α := (a : (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4)) → V)
    (⇑(ofSpan (s := s) hs) : (a : (↑(⋯.extend ⋯) : Type u_4)) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯))

Tactic:
funext (ofSpan_apply_self hs)

Premises used: funext, Module.Basis.ofSpan_apply_self
-- 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
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
rw :
  range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯)) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
rw₁ :
  {x : V | x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯} =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
rw₂ rw₃ : LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯ = LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
⊢ range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (⇑(ofSpan (s := s) hs) : (a : (↑(⋯.extend ⋯) : Type u_4)) → V) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯

Tactic:
rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, Module.Basis.coe_ofSpan
-- 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
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
⊢ range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (⇑(ofSpan (s := s) hs) : (a : (↑(⋯.extend ⋯) : Type u_4)) → V) ⊆
    s

Tactic:
extendLe_subset (linearIndependent_empty K V) (empty_subset s) hs

Premises used: Module.Basis.extendLe_subset, Set.empty_subset, linearIndependent_empty
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ Free K V

Tactic:
Module.Free.of_basis (ofVectorSpace K V)

Premises used: Module.Free.of_basis, Module.Basis.ofVectorSpace
-- 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
x : (↑(ofVectorSpaceIndex K V) : Type u_4)
unfold : (extend (s := ∅) ⋯ : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x = (↑x : V)
⊢ (ofVectorSpace K V : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x = (↑x : V)

Tactic:
unfold ofVectorSpace

Premises used: Module.Basis.ofVectorSpace
-- 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
x : (↑(ofVectorSpaceIndex K V) : Type u_4)
⊢ (extend (s := ∅) ⋯ : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x = (↑x : V)

Tactic:
Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply, Module.Basis.ofVectorSpaceIndex, Set.restrict
-- 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
x : (↑(ofVectorSpaceIndex K V) : Type u_4)
⊢ (extend (s := ∅) ⋯ : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x = (↑x : V)

Tactic:
exact Basis.mk_apply _ _ _

Premises used: Module.Basis.mk_apply
-- 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
⊢ Eq.{u_4 + 1} (α := (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)
    (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))

Tactic:
funext fun x => ofVectorSpace_apply_self K V x

Premises used: funext, Module.Basis.ofVectorSpace_apply_self
-- 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
⊢ LinearIndependent.{u_4, u_3, u_4} (ι := (↑(ofVectorSpaceIndex K V) : Type u_4)) K (M := V)
    (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)

Tactic:
(ofVectorSpace K V).linearIndependent

Premises used: Module.Basis.ofVectorSpace, Module.Basis.linearIndependent
-- 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
h :
  Eq.{u_4 + 1} (α := { x : V // x ∈ ofVectorSpaceIndex K V } → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))
    (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)
⊢ LinearIndependent.{u_4, u_3, u_4} (ι := { x : V // x ∈ ofVectorSpaceIndex K V }) K
    (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))

Tactic:
convert! (ofVectorSpace K V).linearIndependent

Premises used: Module.Basis.ofVectorSpace, Module.Basis.linearIndependent
-- 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
h :
  ∀ (x : { x : V // x ∈ ofVectorSpaceIndex K V }),
    (↑x : V) = (ofVectorSpace K V : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x
⊢ Eq.{u_4 + 1} (α := { x : V // x ∈ ofVectorSpaceIndex K V } → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))
    (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)

Tactic:
ext x
-- 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
x : { x : V // x ∈ ofVectorSpaceIndex K V }
h h₁ : (↑x : V) = (↑x : V)
⊢ (↑x : V) = (ofVectorSpace K V : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x

Tactic:
rw [ofVectorSpace_apply_self]

Premises used: Module.Basis.ofVectorSpace_apply_self
-- 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
⊢ range (ι := (↑(ofVectorSpaceIndex K V) : Type u_4))
      (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) =
    ofVectorSpaceIndex K V

Tactic:
range_extend _

Premises used: Module.Basis.range_extend, Module.Basis.ofVectorSpaceIndex
-- 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
⊢ ∃ (s : Set V), Nonempty (Basis (↑s : Type u_4) K V)

Tactic:
⟨ofVectorSpaceIndex K V, ⟨ofVectorSpace K V⟩⟩

Premises used: Nonempty.intro, Module.Basis.ofVectorSpace, Exists.intro, Module.Basis.ofVectorSpaceIndex
-- 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
inst_3 : Fintype K
inst_4 : Fintype V
⊢ ∃ (n : ℕ), card V = card K ^ n

Tactic:
⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩

Premises used: Set.Elem, Fintype.card, Module.Basis.ofVectorSpace, Exists.intro, Module.card_fintype, Module.Basis.ofVectorSpaceIndex
-- 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
inst_3 : Fintype K
inst_4 : Fintype V
⊢ ∃ (n : ℕ), card V = card K ^ n

Tactic:
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
-- 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
inst_3 : Fintype K
inst_4 : Fintype V
⊢ ∃ (n : ℕ), card V = card K ^ n

Tactic:
classical
  exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
-- 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
v : V
hv : v ≠ 0
left : Ne (α := Submodule K V) (K ∙ v) ⊥
right : ∀ b < K ∙ v, b = ⊥
⊢ IsAtom (α := Submodule K V) (K ∙ v)

Tactic:
constructor
-- 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
v : V
hv : v ≠ 0
left : ∃ (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.Basis.VectorSpace
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0

Tactic:
⟨v, ⟨mem_span_singleton_self v, hv⟩⟩

Premises used: Submodule.mem_span_singleton_self, 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
v : V
hv : v ≠ 0
⊢ ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0

Tactic:
exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
-- 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
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
right : ∀ (h : ¬T = ⊥), False
⊢ T = ⊥

Tactic:
by_contra h
-- 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
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
right : (↑(K ∙ v) : Set V) ⊆ (↑T : Set V)
⊢ False

Tactic:
apply hT.2

Premises used: And.right