awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R J) f
sum_f :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i) =
    -∑ x ∈ f.support.erase i, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) x : R) (v x)
f_ne : f ≠ 0
hfi : Ne.{u_2 + 1} (α := R) ((f : (a : ι) → R) i : R) (0 : R)
hfi' : i ∈ f.support
c : ι
hc : c ∈ f.support.erase i
⊢ c ∈ I

Tactic:
exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)

Premises used: Finset.ne_of_mem_erase, Or.resolve_left, Iff.mp, Finset.erase_subset
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_6
M : Type u_7
L : Type u_8
inst : CommSemiring K
inst_1 : Semiring M
inst_2 : Algebra K M
inst_3 : CommRing L
inst_4 : IsDomain L
inst_5 : Algebra K L
apply :
  LinearIndependent (ι := M →ₐ[K] L) L (M := M → L) ((⇑(ltoFun K M L L) : (a : M →ₗ[K] L) → M → L) ∘ AlgHom.toLinearMap)
⊢ LinearIndependent (ι := M →ₐ[K] L) L AlgHom.toLinearMap

Tactic:
apply LinearIndependent.of_comp (LinearMap.ltoFun K M L L)

Premises used: LinearMap.ltoFun, LinearIndependent.of_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_6
M : Type u_7
L : Type u_8
inst : CommSemiring K
inst_1 : Semiring M
inst_2 : Algebra K M
inst_3 : CommRing L
inst_4 : IsDomain L
inst_5 : Algebra K L
⊢ LinearIndependent (ι := M →ₐ[K] L) L (M := M → L) ((⇑(ltoFun K M L L) : (a : M →ₗ[K] L) → M → L) ∘ AlgHom.toLinearMap)

Tactic:
(linearIndependent_monoidHom M L).comp
    (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
    (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

Premises used: DFunLike.congr_fun, linearIndependent_monoidHom, Function.comp, AlgHom.ext, AlgHom.toRingHom, RingHom.toMonoidHom, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_6
M : Type u_7
L : Type u_8
inst : CommSemiring K
inst_1 : Semiring M
inst_2 : Algebra K M
inst_3 : CommRing L
inst_4 : IsDomain L
inst_5 : Algebra K L
⊢ LinearIndependent (ι := M →ₐ[K] L) L (M := M → L) ((⇑(ltoFun K M L L) : (a : M →ₗ[K] L) → M → L) ∘ AlgHom.toLinearMap)

Tactic:
exact (linearIndependent_monoidHom M L).comp
    (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
    (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

Premises used: DFunLike.congr_fun, linearIndependent_monoidHom, Function.comp, AlgHom.ext, AlgHom.toRingHom, RingHom.toMonoidHom, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_6
M : Type u_7
L : Type u_8
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Semiring M
inst_3 : Algebra K M
inst_4 : CommRing L
inst_5 : IsDomain L
inst_6 : Algebra K L
inst_7 : IsTorsionFree K L
⊢ LinearIndependent (ι := M →ₐ[K] L) K AlgHom.toLinearMap

Tactic:
(linearIndependent_algHom_toLinearMap K M L).restrict_scalars' K

Premises used: linearIndependent_algHom_toLinearMap, LinearIndependent.restrict_scalars'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
⊢ Injective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
(injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
refine : ∀ (x : M) (hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)), x = 0
⊢ Injective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
x : M
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
rw : Membership.mem (γ := Submodule R M) ⊤ x
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
rw [hv]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
x : M
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
x : M
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
⊢ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
exact mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
x : M
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
⊢ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x

Tactic:
have : x ∈ Submodule.span R (.range v) := by rw [hv]; exact mem_top
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
x : M
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
this : Membership.mem (γ := Submodule R M) (span R (Set.range v)) x
obtain :
  ∀ (c : ι →₀ R) (hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) (c.sum fun (i : ι) (a : R) ↦ a • v i) : N) (0 : N))
    (this : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (c.sum fun (i : ι) (a : R) ↦ a • v i)),
    Eq.{u_4 + 1} (α := M) (c.sum fun (i : ι) (a : R) ↦ a • v i) 0
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this

Premises used: Finsupp.mem_span_range_iff_exists_finsupp, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
c : ι →₀ R
hx : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) (c.sum fun (i : ι) (a : R) ↦ a • v i) : N) (0 : N)
this : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (c.sum fun (i : ι) (a : R) ↦ a • v i)
⊢ Eq.{u_6 + 1} (α := N) (c.sum fun (a : ι) (b : R) ↦ HSMul.hSMul (β := N) b ((f : (a : M) → N) (v a) : N)) 0

Tactic:
simp only [map_finsuppSum, map_smul] at hx

Premises used: map_finsuppSum, map_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
c : ι →₀ R
this : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (c.sum fun (i : ι) (a : R) ↦ a • v i)
hx : Eq.{u_6 + 1} (α := N) (c.sum fun (a : ι) (b : R) ↦ HSMul.hSMul (β := N) b ((f : (a : M) → N) (v a) : N)) 0
obtain :
  ∀ (this : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (Finsupp.sum 0 fun (i : ι) (a : R) ↦ a • v i))
    (hx :
      Eq.{u_6 + 1} (α := N) (Finsupp.sum 0 fun (a : ι) (b : R) ↦ HSMul.hSMul (β := N) b ((f : (a : M) → N) (v a) : N))
        0),
    Eq.{u_4 + 1} (α := M) (Finsupp.sum 0 fun (i : ι) (a : R) ↦ a • v i) 0
⊢ Eq.{u_4 + 1} (α := M) (c.sum fun (i : ι) (a : R) ↦ a • v i) 0

Tactic:
obtain rfl := linearIndependent_iff.mp hli c hx

Premises used: linearIndependent_iff, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
this : Membership.mem (γ := Submodule R M) (span R (Set.range v)) (Finsupp.sum 0 fun (i : ι) (a : R) ↦ a • v i)
hx : Eq.{u_6 + 1} (α := N) (Finsupp.sum 0 fun (a : ι) (b : R) ↦ HSMul.hSMul (β := N) b ((f : (a : M) → N) (v a) : N)) 0
⊢ Eq.{u_4 + 1} (α := M) (Finsupp.sum 0 fun (i : ι) (a : R) ↦ a • v i) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
hsp : Eq.{u_6 + 1} (α := Submodule R N) (span R (Set.range ((⇑f : (a : M) → N) ∘ v))) ⊤
⊢ Bijective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
⟨LinearMap.injective_of_linearIndependent hv hli, ?_⟩

Premises used: LinearMap.injective_of_linearIndependent, And.intro, Function.Bijective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
hsp : Eq.{u_6 + 1} (α := Submodule R N) (span R (Set.range ((⇑f : (a : M) → N) ∘ v))) ⊤
refine : Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Bijective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
refine ⟨LinearMap.injective_of_linearIndependent hv hli, ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
hsp : Eq.{u_6 + 1} (α := Submodule R N) (span R (Set.range ((⇑f : (a : M) → N) ∘ v))) ⊤
⊢ f.range = ⊤

Tactic:
rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp

Premises used: Set.range_comp, Submodule.map_top, Submodule.map_span
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
hli : LinearIndependent.{u_7, u_2, u_6} R (M := N) ((⇑f : (a : M) → N) ∘ v)
hsp rwa rwa₁ rwa₂ rwa₃ : f.range = ⊤
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
rwa [← range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), Membership.mem (γ := Submodule R M) (span R (v '' s)) (r • v i) → r = 0
rw : LinearIndepOn R v (s ∪ {i})
⊢ LinearIndepOn R v (insert i s)

Tactic:
rw [← Set.union_singleton]

Premises used: Set.union_singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), Membership.mem (γ := Submodule R M) (span R (v '' s)) (r • v i) → r = 0
r : R
hr : r • v i = 0
⊢ Membership.mem (γ := Submodule R M) (span R (v '' s)) (r • v i)

Tactic:
simp [hr]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), Membership.mem (γ := Submodule R M) (span R (v '' s)) (r • v i) → r = 0
refine : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' {i}))
⊢ LinearIndepOn R v (s ∪ {i})

Tactic:
refine hs.union (.singleton' fun r hr ↦ hx _ <| by simp [hr]) ?_

Premises used: LinearIndepOn.union, LinearIndepOn.singleton'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), Membership.mem (γ := Submodule R M) (span R (v '' s)) (r • v i) → r = 0
⊢ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' {i}))

Tactic:
simp +contextual [disjoint_span_singleton'', hx]

Premises used: Submodule.disjoint_span_singleton''
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
x : M
hs : LinearIndepOn R _root_.id s
hx : ∀ (r : R), Membership.mem (γ := Submodule R M) (span R s) (r • x) → r = 0
⊢ ∀ (r : R), Membership.mem (γ := Submodule R M) (span R (_root_.id '' s)) (r • _root_.id x) → r = 0

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun (i j : ι) ↦ Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v j) : R) (0 : R)
h2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v i) : R) (1 : R)
⊢ LinearIndependent R v

Tactic:
linearIndependent_iff'.mpr fun s g hrel i hi ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun (i j : ι) ↦ Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v j) : R) (0 : R)
h2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v i) : R) (1 : R)
refine :
  ∀ (s : Finset ι) (g : ι → R) (hrel : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι) (hi : i ∈ s), g i = 0
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff'.mpr fun s g hrel i hi ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun (i j : ι) ↦ Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v j) : R) (0 : R)
h2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v i) : R) (1 : R)
s : Finset ι
g : ι → R
hrel : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ HMul.hMul (β := R) (g j) ((f i : (a : M) → R) (v j) : R) = 0

Tactic:
simp [h1 hji.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun (i j : ι) ↦ Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v j) : R) (0 : R)
h2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v i) : R) (1 : R)
s : Finset ι
g : ι → R
hrel : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ ∀ (j : ι) (hjs : j ∈ s) (hji : j ≠ i), HMul.hMul (β := R) (g j) ((f i : (a : M) → R) (v j) : R) = 0

Tactic:
have aux (j : ι) (hjs : j ∈ s) (hji : j ≠ i) : g j * (f i) (v j) = 0 := by simp [h1 hji.symm]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun (i j : ι) ↦ Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v j) : R) (0 : R)
h2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v i) : R) (1 : R)
s : Finset ι
g : ι → R
hrel : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
aux : ∀ (j : ι) (hjs : j ∈ s) (hji : j ≠ i), HMul.hMul (β := R) (g j) ((f i : (a : M) → R) (v j) : R) = 0
⊢ i ∉ s → HMul.hMul (β := R) (g i) ((f i : (a : M) → R) (v i) : R) = 0

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun (i j : ι) ↦ Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v j) : R) (0 : R)
h2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((f i : (a : M) → R) (v i) : R) (1 : R)
s : Finset ι
g : ι → R
hrel : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
aux : ∀ (j : ι) (hjs : j ∈ s) (hji : j ≠ i), HMul.hMul (β := R) (g j) ((f i : (a : M) → R) (v j) : R) = 0
⊢ g i = 0

Tactic:
simpa [s.sum_eq_single i aux (by lia), h2 i] using congr_arg (f i) hrel

Premises used: Finset.sum_eq_single, congr_arg, DFunLike.coe
-- 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
s : Set V
x y : V
simp :
  ∀ (x_1 : K) (x_2 : V),
    Membership.mem (γ := Submodule K V) (span K s) x_2 →
      x = x_1 • y + x_2 →
        x ∉ span K s → ∃ (a : K) (z : V), Membership.mem (γ := Submodule K V) (span K s) z ∧ y = a • x + z
⊢ Membership.mem (γ := Submodule K V) (span K (insert y s)) x →
    x ∉ span K s → Membership.mem (γ := Submodule K V) (span K (insert x s)) y

Tactic:
simp only [mem_span_insert, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, Submodule.mem_span_insert
-- 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
s : Set V
y : V
a : K
z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : a • y + z ∉ span K s
⊢ ∃ (a_1 : K) (z_1 : V), Membership.mem (γ := Submodule K V) (span K s) z_1 ∧ y = a_1 • (a • y + z) + z_1

Tactic:
⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩

Premises used: Inv.inv, And.intro, Exists.intro, HSMul.hSMul, Neg.neg, 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
s : Set V
y : V
a : K
z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : a • y + z ∉ span K s
refine : y = a⁻¹ • (a • y + z) + -a⁻¹ • z
⊢ ∃ (a_1 : K) (z_1 : V), Membership.mem (γ := Submodule K V) (span K s) z_1 ∧ y = a_1 • (a • y + z) + z_1

Tactic:
refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩
-- 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
s : Set V
y z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : HSMul.hSMul.{u_3, u, u} (α := K) 0 y + z ∉ span K s
⊢ False

Tactic:
simp_all
-- 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
s : Set V
y : V
a : K
z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : a • y + z ∉ span K s
⊢ a ≠ 0

Tactic:
have a0 : a ≠ 0 := by
    rintro rfl
    simp_all
-- 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
s : Set V
y : V
a : K
z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : a • y + z ∉ span K s
a0 : a ≠ 0
match_scalars : 1 = a⁻¹ * (a * 1)
match_scalars₁ : 0 = a⁻¹ * 1 + -a⁻¹ * 1
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z

Tactic:
match_scalars
-- 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
s : Set V
y : V
a : K
z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 1 = a⁻¹ * (a * 1)

Tactic:
simp [a0]
-- 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
s : Set V
y : V
a : K
z : V
hz : Membership.mem (γ := Submodule K V) (span K s) z
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 0 = a⁻¹ * 1 + -a⁻¹ * 1

Tactic:
simp [a0]
-- 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 : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
rw : LinearIndepOn K v (s ∪ {x})
⊢ LinearIndepOn K v (insert x s)

Tactic:
rw [← union_singleton]

Premises used: Set.union_singleton
-- 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 : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ v x ≠ 0

Tactic:
have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)
-- 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 : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
apply : Disjoint (α := Submodule K V) (span K (v '' s)) (span K (v '' {x}))
⊢ LinearIndepOn K v (s ∪ {x})

Tactic:
apply hs.union (LinearIndepOn.singleton x0)

Premises used: LinearIndepOn.union, LinearIndepOn.singleton
-- 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 : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
rwa : Disjoint (α := Submodule K V) (span K (v '' s)) (K ∙ v x)
rwa₁ rwa₂ rwa₃ rwa₄ : v x ∉ span K (v '' s)
⊢ Disjoint (α := Submodule K V) (span K (v '' s)) (span K (v '' {x}))

Tactic:
rwa [image_singleton, disjoint_span_singleton' x0]

Premises used: Submodule.disjoint_span_singleton', Set.image_singleton
-- 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
s : Set V
x : V
hs : LinearIndepOn K id s
hx : x ∉ span K s
⊢ LinearIndepOn K id (insert x s)

Tactic:
hs.insert ((image_id s).symm ▸ hx)

Premises used: LinearIndepOn.insert, Eq.rec, Eq.symm, Set.image_id