ι✝ : Type u'
ι' : Type ?u.1222999
R : Type ?u.1223002
K : Type u_2
M : Type ?u.1223008
M' : Type ?u.1223011
M'' : Type ?u.1223014
V : Type u
V' : Type ?u.1223019
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι✝ → V
s✝ t : Set V
x y z : V
ι : Type u_1
s : Set ι
a : ι
f : ι → V
has : ¬a ∈ s
⊢ LinearIndependent K (((fun x => f ↑x) ∘ ↑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ∘ some) ∧
      ¬((fun x => f ↑x) ∘ ↑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) none ∈
          span K
            (range (((fun x => f ↑x) ∘ ↑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ∘ some)) ↔
    (LinearIndependent K fun x => f ↑x) ∧ ¬f a ∈ span K (f '' s)
ι✝ : Type u'
ι' : Type ?u.1222999
R : Type ?u.1223002
K : Type u_2
M : Type ?u.1223008
M' : Type ?u.1223011
M'' : Type ?u.1223014
V : Type u
V' : Type ?u.1223019
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι✝ → V
s✝ t : Set V
x y z : V
ι : Type u_1
s : Set ι
a : ι
f : ι → V
has : ¬a ∈ s
⊢ (LinearIndependent K fun x => f ↑x) ↔ (LinearIndependent K fun x => f ↑x) ∧ ¬f a ∈ span K (f '' s)
rw [← linearIndependent_equiv ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm),
  linearIndependent_option]
ι✝ : Type u'
ι' : Type ?u.1222999
R : Type ?u.1223002
K : Type u_2
M : Type ?u.1223008
M' : Type ?u.1223011
M'' : Type ?u.1223014
V : Type u
V' : Type ?u.1223019
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι✝ → V
s✝ t : Set V
x y z : V
ι : Type u_1
s : Set ι
a : ι
f : ι → V
has : ¬a ∈ s
⊢ (LinearIndependent K fun x => f ↑x) → (¬f a ∈ span K (f '' range Subtype.val) ↔ ¬f a ∈ span K (f '' s))
ι✝ : Type u'
ι' : Type ?u.1222999
R : Type ?u.1223002
K : Type u_2
M : Type ?u.1223008
M' : Type ?u.1223011
M'' : Type ?u.1223014
V : Type u
V' : Type ?u.1223019
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι✝ → V
s✝ t : Set V
x y z : V
ι : Type u_1
s : Set ι
a : ι
f : ι → V
has : ¬a ∈ s
⊢ (LinearIndependent K fun x => f ↑x) → (¬f a ∈ span K (range fun x => f ↑x) ↔ ¬f a ∈ span K (f '' s))
erw [range_comp f ((↑) : s → ι)]
no goals
ι✝ : Type u'
ι' : Type ?u.1222999
R : Type ?u.1223002
K : Type u_2
M : Type ?u.1223008
M' : Type ?u.1223011
M'' : Type ?u.1223014
V : Type u
V' : Type ?u.1223019
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι✝ → V
s✝ t : Set V
x y z : V
ι : Type u_1
s : Set ι
a : ι
f : ι → V
has : ¬a ∈ s
⊢ (LinearIndependent K fun x => f ↑x) → (¬f a ∈ span K (f '' range Subtype.val) ↔ ¬f a ∈ span K (f '' s))
simp