awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x y : V
hx : x ≠ 0
rw : (∀ (c : K), c • ![x, y] 0 ≠ ![x, y] 1) ↔ ∀ (a : K), a • x ≠ y
⊢ LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y

Tactic:
rw [← linearIndepOn_univ_iff, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0,1} from rfl,
    Finset.coe_insert, Finset.coe_singleton, linearIndepOn_pair_iff _ (by simp) (by simpa)]

Premises used: Finset.coe_singleton, Finset.coe_univ, linearIndepOn_univ_iff, linearIndepOn_pair_iff, Finset.coe_insert, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (c : K), c • ![x, y] 0 ≠ ![x, y] 1) ↔ ∀ (a : K), a • x ≠ y

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : V
n : ℕ
v : Fin n → V
rw :
  LinearIndependent.{0, u_3, u} (ι := Fin n) K (M := V)
        (comp (β := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)
            (⇑(finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) ∘
          some) ∧
      comp (α := Option (Fin n)) (β := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)
          (⇑(finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none ∉
        span K
          (range (ι := Fin n)
            (comp (β := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)
                (⇑(finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) ∘
              some)) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
⊢ LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]

Premises used: linearIndependent_option, linearIndependent_equiv, finSuccEquiv, Equiv.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent.{0, u_3, u} (ι := Fin n) K (M := V)
        (comp (β := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)
            (⇑(finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) ∘
          some) ∧
      comp (α := Option (Fin n)) (β := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)
          (⇑(finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) none ∉
        span K
          (range (ι := Fin n)
            (comp (β := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)
                (⇑(finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) ∘
              some)) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : V
n : ℕ
v : Fin n → V
rw :
  (LinearIndependent.{0, u_3, u} K (M := V) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ V) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
rw₁ :
  LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V)
      (comp (β := Fin (n + 1)) (Fin.cons (α := fun (x : Fin (n + 1)) ↦ V) x v)
        (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
rw₂ :
  LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V) (Fin.cons (α := fun (x : Fin (n + 1)) ↦ V) x v) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
rw₃ rw₄ : LinearIndependent K v ∧ x ∉ span K (range v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
⊢ LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ V) v x) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
    linearIndependent_finCons]

Premises used: linearIndependent_finCons, Fin.snoc_eq_cons_rotate, linearIndependent_equiv, Function.comp_def
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : V
n : ℕ
v : Fin n → V
hv : LinearIndependent K v
hx : x ∉ span K (range v)
⊢ LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v)

Tactic:
linearIndependent_finCons.2 ⟨hv, hx⟩

Premises used: Iff.mpr, linearIndependent_finCons, And.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : V
n : ℕ
v : Fin n → V
hv : LinearIndependent K v
hx : x ∉ span K (range v)
⊢ LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ V) v x)

Tactic:
linearIndependent_finSnoc.2 ⟨hv, hx⟩

Premises used: Iff.mpr, linearIndependent_finSnoc, And.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
apply : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
⊢ LinearIndependent.{0, u_6, u_8} (ι := Fin (n + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) v x)

Tactic:
apply hv.finSnoc' v x

Premises used: LinearIndependent.finSnoc'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
by_contra : ∀ (hc : ¬c = 0), False
⊢ c = 0

Tactic:
by_contra hc
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
hc : ¬c = 0
apply : Membership.mem (γ := Submodule K M) (span K (range v)) x
⊢ False

Tactic:
apply hx
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
hc : ¬c = 0
rwa : ¬Eq.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
rwa₁ rwa₂ rwa₃ rwa₄ : ¬c = 0
⊢ Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)

Tactic:
rwa [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]

Premises used: ne_eq, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
hc : ¬c = 0
⊢ Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)

Tactic:
have hc' : algebraMap R K c ≠ 0 := by
    rwa [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
hc : ¬c = 0
hc' : Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := K) ((algebraMap R K : (a : R) → K) c : K) x + y = 0

Tactic:
rw [← algebraMap_smul K c x] at heq

Premises used: algebraMap_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
hc : ¬c = 0
hc' : Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
heq₁ : HSMul.hSMul.{u_7, u_8, u_8} (α := K) ((algebraMap R K : (a : R) → K) c : K) x + y = 0
⊢ ¬c = 0

Tactic:
rw [← algebraMap_smul K c x] at heq

Premises used: algebraMap_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : c • x + y = 0
hc : ¬c = 0
hc' : Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
heq₁ : HSMul.hSMul.{u_7, u_8, u_8} (α := K) ((algebraMap R K : (a : R) → K) c : K) x + y = 0
hc₁ : ¬c = 0
⊢ Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)

Tactic:
rw [← algebraMap_smul K c x] at heq

Premises used: algebraMap_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : HSMul.hSMul.{u_7, u_8, u_8} (α := K) ((algebraMap R K : (a : R) → K) c : K) x + y = 0
hc : ¬c = 0
hc' : Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
rw :
  Membership.mem (γ := Submodule K M) (span K (range v))
    (-HSMul.hSMul.{u_7, u_8, u_8} (α := K) (((algebraMap R K : (a : R) → K) c)⁻¹ : K) y)
⊢ Membership.mem (γ := Submodule K M) (span K (range v)) x

Tactic:
rw [(eq_inv_smul_iff₀ hc').mpr (eq_neg_of_add_eq_zero_left heq), smul_neg]

Premises used: Iff.mpr, smul_neg, eq_neg_of_add_eq_zero_left, eq_inv_smul_iff₀
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : HSMul.hSMul.{u_7, u_8, u_8} (α := K) ((algebraMap R K : (a : R) → K) c : K) x + y = 0
hc : ¬c = 0
hc' : Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
⊢ Membership.mem (γ := Submodule K M) (span K (range v))
    (-HSMul.hSMul.{u_7, u_8, u_8} (α := K) (((algebraMap R K : (a : R) → K) c)⁻¹ : K) y)

Tactic:
Submodule.neg_mem _ (Submodule.smul_mem _ _ (Submodule.span_subset_span R K _ hcy))

Premises used: Submodule.span_subset_span, Set.Mem, Submodule.neg_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_6
K : Type u_7
M : Type u_8
inst : CommRing R
inst_1 : DivisionRing K
inst_2 : AddCommGroup M
inst_3 : Algebra R K
inst_4 : Module K M
inst_5 : Module R M
inst_6 : IsScalarTower R K M
inst_7 : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : Membership.mem (γ := Submodule R M) (span R (range v)) y
heq : HSMul.hSMul.{u_7, u_8, u_8} (α := K) ((algebraMap R K : (a : R) → K) c : K) x + y = 0
hc : ¬c = 0
hc' : Ne.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
⊢ Membership.mem (γ := Submodule K M) (span K (range v))
    (-HSMul.hSMul.{u_7, u_8, u_8} (α := K) (((algebraMap R K : (a : R) → K) c)⁻¹ : K) y)

Tactic:
exact Submodule.neg_mem _ (Submodule.smul_mem _ _ (Submodule.span_subset_span R K _ hcy))

Premises used: Submodule.span_subset_span, Submodule.neg_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
v : Fin (n + 1) → V
rw :
  LinearIndependent K v ↔
    LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) (v 0) (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) v))
rw₁ rw₂ : LinearIndependent K v ↔ LinearIndependent K v
⊢ LinearIndependent K v ↔
    LinearIndependent K (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) v) ∧
      v 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) v))

Tactic:
rw [← linearIndependent_finCons, Fin.cons_self_tail]

Premises used: linearIndependent_finCons, Fin.cons_self_tail
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
v : Fin (n + 1) → V
rw :
  LinearIndependent K v ↔
    LinearIndependent.{0, u_3, u} (ι := Fin (n + 1)) K (M := V)
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ V) (Fin.init (α := fun (i : Fin (n + 1)) ↦ V) v) (v (Fin.last n)))
rw₁ rw₂ : LinearIndependent K v ↔ LinearIndependent K v
⊢ LinearIndependent K v ↔
    LinearIndependent K (Fin.init (α := fun (i : Fin (n + 1)) ↦ V) v) ∧
      v (Fin.last n) ∉ span K (range (Fin.init (α := fun (i : Fin (n + 1)) ↦ V) v))

Tactic:
rw [← linearIndependent_finSnoc, Fin.snoc_init_self]

Premises used: linearIndependent_finSnoc, Fin.snoc_init_self
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s_1 : Set ι
M : Type u_4
M' : Type u_5
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set V
x y : V
n : ℕ
x_1 : { s : Fin (n + 1) → V // LinearIndependent K s }
⊢ (fun
          (s :
            (s : { s : Fin n → V // LinearIndependent K s }) ×
              (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)) ↦
        (Subtype.mk (p := fun (s : Fin (n + 1) → V) ↦ LinearIndependent K s)
            (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V)
              (↑(s.snd (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
                    (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))) :
                V)
              (↑(s.fst (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
                    (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))) :
                Fin n → V))
            ⋯ :
          { s : Fin (n + 1) → V // LinearIndependent K s }))
      ((fun (s : { s : Fin (n + 1) → V // LinearIndependent K s }) ↦
          (Sigma.mk (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
              (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))
              (Subtype.mk (p := fun (s : Fin n → V) ↦ LinearIndependent K s)
                (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) (↑s : Fin (n + 1) → V)) ⋯)
              (Subtype.mk (p := fun (x : V) ↦
                x ∈
                  (↑(span K
                          (range
                            (↑(Subtype.mk (p := fun (s : Fin n → V) ↦ LinearIndependent K s)
                                  (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) (↑s : Fin (n + 1) → V)) ⋯) :
                              Fin n → V))) :
                      Set V)ᶜ)
                ((↑s : Fin (n + 1) → V) 0) ⋯) :
            (s : { s : Fin n → V // LinearIndependent K s }) ×
              (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)))
        x_1) =
    x_1

Tactic:
simp only [Fin.cons_self_tail, Subtype.coe_eta]

Premises used: Fin.cons_self_tail, Subtype.coe_eta
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s_1 : Set ι
M : Type u_4
M' : Type u_5
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set V
x y : V
n : ℕ
x_1 : (s : { s : Fin n → V // LinearIndependent K s }) × (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)
fst : { s : Fin n → V // LinearIndependent K s }
snd : (↑(↑(span K (range (↑fst : Fin n → V))) : Set V)ᶜ : Type u)
⊢ Eq (α := (s : { s : Fin n → V // LinearIndependent K s }) × (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))
    ((fun (s : { s : Fin (n + 1) → V // LinearIndependent K s }) ↦
        (Sigma.mk (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
            (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))
            (Subtype.mk (p := fun (s : Fin n → V) ↦ LinearIndependent K s)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) (↑s : Fin (n + 1) → V)) ⋯)
            (Subtype.mk (p := fun (x : V) ↦
              x ∈
                (↑(span K
                        (range
                          (↑(Subtype.mk (p := fun (s : Fin n → V) ↦ LinearIndependent K s)
                                (Fin.tail (α := fun (i : Fin (n + 1)) ↦ V) (↑s : Fin (n + 1) → V)) ⋯) :
                            Fin n → V))) :
                    Set V)ᶜ)
              ((↑s : Fin (n + 1) → V) 0) ⋯) :
          (s : { s : Fin n → V // LinearIndependent K s }) × (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)))
      ((fun
            (s :
              (s : { s : Fin n → V // LinearIndependent K s }) ×
                (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)) ↦
          (Subtype.mk (p := fun (s : Fin (n + 1) → V) ↦ LinearIndependent K s)
              (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V)
                (↑(s.snd (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
                      (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))) :
                  V)
                (↑(s.fst (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
                      (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u))) :
                  Fin n → V))
              ⋯ :
            { s : Fin (n + 1) → V // LinearIndependent K s }))
        (Sigma.mk (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
          (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)) fst snd)))
    (Sigma.mk (β := fun (s : { s : Fin n → V // LinearIndependent K s }) ↦
      (↑(↑(span K (range (↑s : Fin n → V))) : Set V)ᶜ : Type u)) fst snd)

Tactic:
simp only [Fin.cons_zero, Subtype.coe_eta, Sigma.mk.inj_iff,
    Fin.tail_cons, heq_eq_eq, and_self]

Premises used: and_self, heq_eq_eq, Subtype.coe_eta, Sigma.mk.inj_iff, Fin.cons_zero, Fin.tail_cons
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
rw : Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f (Fin.succ 0)
⊢ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 1

Tactic:
rw [← Fin.succ_zero_eq_one]

Premises used: Fin.succ_zero_eq_one
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
⊢ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f (Fin.succ 0)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
rw :
  LinearIndependent K (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f) ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₁ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₂ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ K ∙ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₃ :
  (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      ¬∃ (a : K), a • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₄ :
  (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      ∀ (x : K), ¬x • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₅ rw₆ : (f 1 ≠ 0 ∧ ∀ (x : K), ¬x • f 1 = f 0) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0

Tactic:
rw [linearIndependent_finSucc, linearIndependent_unique_iff, range_unique, mem_span_singleton,
    not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]

Premises used: Set.range_unique, Submodule.mem_span_singleton, not_exists, linearIndependent_unique_iff, linearIndependent_finSucc
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∃ (m : Set ι),
    s ⊆ m ∧ Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) m

Tactic:
zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩

Premises used: setOf, HasSubset.Subset, And, zorn_subset_nonempty, And.intro, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
refine :
  ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub
⊢ ∃ (m : Set ι),
    s ⊆ m ∧ Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) m

Tactic:
refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩

Premises used: setOf, HasSubset.Subset, And, zorn_subset_nonempty, And.intro, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub

Tactic:
fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩

Premises used: Set.sUnion, And.intro, Exists.intro