awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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)
⊢ x = 0
have this : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ x = 0
have 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
Tactic: obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this
Cleared hypotheses: x, hx, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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_4 + 1} (α := M) (c.sum fun (i : ι) (a : R) ↦ a • v i) 0
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ Eq.{u_4 + 1} (α := M) (c.sum fun (i : ι) (a : R) ↦ a • v i) 0
have 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
Tactic: obtain rfl := linearIndependent_iff.mp hli c hx
Cleared hypotheses: c, this, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
have refine : Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: refine ⟨LinearMap.injective_of_linearIndependent hv hli, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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))) ⊤
⊢ Surjective.{u_4 + 1, u_6 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
have hsp₁ : f.range = ⊤
Tactic: rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp
Cleared hypotheses: hsp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndepOn R v (insert i s)
have rw : LinearIndepOn R v (s ∪ {i})
Tactic: rw [← Set.union_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
⊢ LinearIndepOn R v (s ∪ {i})
have refine : Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' {i}))
Tactic: refine hs.union (.singleton' fun r hr ↦ hx _ <| by simp [hr]) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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
have 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
Tactic: refine linearIndependent_iff'.mpr fun s g hrel i hi ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
⊢ g i = 0
have aux : ∀ (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]
-- 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
x y : V
⊢ 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
have 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
Tactic: simp only [mem_span_insert, forall_exists_index, and_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
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
have refine : y = a⁻¹ • (a • y + z) + -a⁻¹ • z
Tactic: refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
have a0 : a ≠ 0
Tactic: have a0 : a ≠ 0 := by
    rintro rfl
    simp_all
-- 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
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
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
have match_scalars : 1 = a⁻¹ * (a * 1)
Tactic: match_scalars
-- 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
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)
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
have match_scalars₁ : 0 = a⁻¹ * 1 + -a⁻¹ * 1
Tactic: match_scalars
-- 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
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ LinearIndepOn K v (insert x s)
have rw : LinearIndepOn K v (s ∪ {x})
Tactic: rw [← union_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
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)
⊢ LinearIndepOn K v (s ∪ {x})
have x0 : v x ≠ 0
Tactic: have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)
-- 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
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ LinearIndepOn K v (s ∪ {x})
have apply : Disjoint (α := Submodule K V) (span K (v '' s)) (span K (v '' {x}))
Tactic: apply hs.union (LinearIndepOn.singleton x0)
-- 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
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
x0 : v x ≠ 0
⊢ Disjoint (α := Submodule K V) (span K (v '' s)) (span K (v '' {x}))
have rwa : Disjoint (α := Submodule K V) (span K (v '' s)) (K ∙ v x)
Tactic: rwa [image_singleton, disjoint_span_singleton' x0]
-- 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
v : ι → V
x : V
⊢ (LinearIndependent.{u', u_3, u} K (M := V) fun (o : Option ι) ↦ o.casesOn' x v) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
have rw : LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
      (comp (β := ι ⊕ PUnit.{u' + 1})
        ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
          (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
        Sum.inl) ∧
    Ne.{u + 1} (α := V)
        (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inr default)
        0 ∧
      (Membership.mem (γ := Submodule K V)
          (span K
            (range (ι := ι)
              (comp (β := ι ⊕ PUnit.{u' + 1})
                ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                  (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                Sum.inl)))
          (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
            ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
              (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
            Sum.inr default) →
        Eq.{u + 1} (α := V)
          (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
            ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
              (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
            Sum.inr default)
          0) ↔
  LinearIndependent K v ∧ x ∉ span K (range v)
Tactic: rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{u'} ι).symm, linearIndependent_sum,
    @range_unique _ PUnit, @linearIndependent_unique_iff PUnit, disjoint_span_singleton]
-- 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
v : ι → V
x : V
⊢ LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      Ne.{u + 1} (α := V)
          (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
            ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
              (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
            Sum.inr default)
          0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
              ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
              Sum.inr default) →
          Eq.{u + 1} (α := V)
            (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
              ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
              Sum.inr default)
            0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
have dsimp : LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
      (comp (β := ι ⊕ PUnit.{u' + 1})
        ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
          (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
        Sum.inl) ∧
    ¬x = 0 ∧
      (Membership.mem (γ := Submodule K V)
          (span K
            (range (ι := ι)
              (comp (β := ι ⊕ PUnit.{u' + 1})
                ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                  (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                Sum.inl)))
          x →
        x = 0) ↔
  LinearIndependent K v ∧ x ∉ span K (range v)
Tactic: dsimp [(· ∘ ·)]
-- 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
v : ι → V
x : V
⊢ LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      ¬x = 0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            x →
          x = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
have refine : ∀ (h : LinearIndependent K v ∧ x ∉ span K (range v)), ¬x = 0
Tactic: refine ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩
-- 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
⊢ 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: rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
-- 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
⊢ 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)
have simp : (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦
      f
        (↑((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 x)) :
          ι)) ∧
    f
        (↑((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 fun (x : (↑s : Type u')) ↦
          f
            (↑((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 x)) :
              ι)) ↔
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
Tactic: simp only [comp_def]
-- 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
⊢ (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦
        f
          (↑((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 x)) :
            ι)) ∧
      f
          (↑((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 fun (x : (↑s : Type u')) ↦
            f
              (↑((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 x)) :
                ι)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
have rw : (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦
      f
        (↑((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 x)) :
          ι)) ∧
    f
        (↑((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
        (f ''
          range fun (x : (↑s : Type u')) ↦
            (↑((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 x)) :
              ι)) ↔
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
Tactic: rw [range_comp']
-- 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
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
have 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)
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)
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
have 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)
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