awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
rw :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ↔
    LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
rw₁ :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
have rw₂ : LinearIndependent.{u', u_3, u} (ι := Option (↑s : Type u')) K (M := V)
    ((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
      (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
        (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ↔
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
Tactic: classical
  rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
  simp only [comp_def]
  rw [range_comp']
  simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
rw :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ↔
    LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
rw₁ :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
rw₂ :
  LinearIndependent.{u', u_3, u} (ι := Option (↑s : Type u')) K (M := V)
      ((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
        (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
          (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
have rw₃ : LinearIndependent.{u', u_3, u} (ι := (↑s : Type u')) K (M := V)
      (((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
          (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
            (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ∘
        some) ∧
    comp (α := Option (↑s : Type u')) (fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι))
        (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
          (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
        none ∉
      span K
        (range (ι := (↑s : Type u'))
          (((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
              (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
                (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ∘
            some)) ↔
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
Tactic: classical
  rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
  simp only [comp_def]
  rw [range_comp']
  simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
⊢ LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
have pos : ∀ (has : a ∈ s),
  LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
pos :
  ∀ (has : a ∈ s),
    LinearIndepOn K f (insert a s) ↔
      LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
⊢ LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
have neg : ∀ (has : a ∉ s),
  LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
⊢ Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
have pos : ∀ (has : a ∈ s), Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
pos :
  ∀ (has : a ∈ s), Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
⊢ Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
have neg : ∀ (has : a ∉ s), Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
⊢ f a ∉ span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
have rw : ¬(LinearIndepOn K f (insert a s) → a ∈ s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
Tactic: rw [h.mem_span_iff, Classical.not_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
h : LinearIndepOn K f s
rw : ¬(LinearIndepOn K f (insert a s) → a ∈ s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
⊢ f a ∉ span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
have rw₁ : LinearIndepOn K f (insert a s) ∧ a ∉ s ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
Tactic: rw [h.mem_span_iff, Classical.not_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
a : V
h : LinearIndepOn K id s
⊢ a ∉ span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
have rw : ¬(LinearIndepOn K id (insert a s) → a ∈ s) ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
Tactic: rw [h.mem_span_iff_id, Classical.not_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
a : V
h : LinearIndepOn K id s
rw : ¬(LinearIndepOn K id (insert a s) → a ∈ s) ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
⊢ a ∉ span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
have rw₁ : LinearIndepOn K id (insert a s) ∧ a ∉ s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
Tactic: rw [h.mem_span_iff_id, Classical.not_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
hy : ∀ (a : K), a • x ≠ y
⊢ LinearIndepOn (ι := V) K id {x, y}
have rw : LinearIndepOn (ι := V) K id {y, x}
Tactic: rw [pair_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
⊢ LinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j
have rw : LinearIndepOn K v {j, i} ↔ ∀ (c : K), c • v i ≠ v j
Tactic: rw [pair_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
⊢ LinearIndepOn K v {j, i} ↔ ∀ (c : K), c • v i ≠ v j
have h : (∀ (c : K), c • v i ≠ v j) ↔ LinearIndepOn K v {i} ∧ v j ∉ span K (v '' {i})
Tactic: convert! linearIndepOn_insert (s := { i }) (a := j) hij.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y
have rw : (∀ (c : K), c • ![x, y] 0 ≠ ![x, y] 1) ↔ ∀ (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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 + 1)) K (M := V) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ V) x v) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
have 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)
Tactic: rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 + 1)) K (M := V) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ V) v x) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
have 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)
Tactic: rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
    linearIndependent_finCons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
    linearIndependent_finCons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
    linearIndependent_finCons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
⊢ 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)
have rw₃ : LinearIndependent K v ∧ x ∉ span K (range v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
Tactic: rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
    linearIndependent_finCons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
⊢ LinearIndependent.{0, u_6, u_8} (ι := Fin (n + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) v x)
have apply : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
Tactic: apply hv.finSnoc' v x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ c = 0
have by_contra : ∀ (hc : ¬c = 0), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ False
have apply : Membership.mem (γ := Submodule K M) (span K (range v)) x
Tactic: apply hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
have rwa : ¬Eq.{u_7 + 1} (α := K) ((algebraMap R K : (a : R) → K) c : K) (0 : K)
Tactic: rwa [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
⊢ Membership.mem (γ := Submodule K M) (span K (range v)) x
have hc' : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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)
⊢ Membership.mem (γ := Submodule K M) (span K (range v)) x
have heq₁ : 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
Cleared hypotheses: heq, hc, hc'
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)) x
have 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)
Tactic: rw [(eq_inv_smul_iff₀ hc').mpr (eq_neg_of_add_eq_zero_left heq), smul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ 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))
have 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))
Tactic: rw [← linearIndependent_finCons, Fin.cons_self_tail]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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))
⊢ 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))
have rw₁ : LinearIndependent K v ↔ LinearIndependent K v
Tactic: rw [← linearIndependent_finCons, Fin.cons_self_tail]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ 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))
have 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)))
Tactic: rw [← linearIndependent_finSnoc, Fin.snoc_init_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)))
⊢ 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))
have rw₁ : LinearIndependent K v ↔ LinearIndependent K v
Tactic: rw [← linearIndependent_finSnoc, Fin.snoc_init_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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 1
have rw : Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f (Fin.succ 0)
Tactic: rw [← Fin.succ_zero_eq_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
have 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
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]