[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
hs : LinearIndependent K Subtype.val
⊢ ↑⊤ ⊆ ↑(span K (range (restrict (LinearIndependent.extend hs (_ : s ⊆ univ)) id)))
[PROOFSTEP]
simpa using hs.subset_span_extend (subset_univ s)
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
hs : LinearIndependent K Subtype.val
⊢ range ↑(extend hs) = LinearIndependent.extend hs (_ : s ⊆ univ)
[PROOFSTEP]
rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
x : ↑(ofVectorSpaceIndex K V)
⊢ ↑(ofVectorSpace K V) x = ↑x
[PROOFSTEP]
unfold ofVectorSpace
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
x : ↑(ofVectorSpaceIndex K V)
⊢ ↑(extend (_ : LinearIndependent K fun x => ↑x)) x = ↑x
[PROOFSTEP]
exact Basis.mk_apply _ _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
⊢ LinearIndependent K Subtype.val
[PROOFSTEP]
convert (ofVectorSpace K V).linearIndependent
[GOAL]
case h.e'_4
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
⊢ Subtype.val = ↑(ofVectorSpace K V)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_4.h
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = ↑(ofVectorSpace K V) x
[PROOFSTEP]
rw [ofVectorSpace_apply_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n
[PROOFSTEP]
classical exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n
[PROOFSTEP]
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
⊢ IsAtom (span K {v})
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
⊢ span K {v} ≠ ⊥
[PROOFSTEP]
rw [Submodule.ne_bot_iff]
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
⊢ ∃ x, x ∈ span K {v} ∧ x ≠ 0
[PROOFSTEP]
exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
⊢ ∀ (b : Submodule K V), b < span K {v} → b = ⊥
[PROOFSTEP]
intro T hT
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
⊢ T = ⊥
[PROOFSTEP]
by_contra h
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ False
[PROOFSTEP]
apply hT.2
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ ↑(span K {v}) ⊆ ↑T
[PROOFSTEP]
change span K { v } ≤ T
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ span K {v} ≤ T
[PROOFSTEP]
simp_rw [span_singleton_le_iff_mem, ← Ne.def, Submodule.ne_bot_iff] at *
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ∃ x, x ∈ T ∧ x ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rcases h with ⟨s, ⟨hs, hz⟩⟩
[GOAL]
case right.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
s : V
hs : s ∈ T
hz : s ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
[GOAL]
case right.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rcases eq_or_ne a 0 with rfl | h
[GOAL]
case right.intro.intro.intro.inl
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
hs : 0 • v ∈ T
hz : 0 • v ≠ 0
⊢ v ∈ T
[PROOFSTEP]
simp only [zero_smul, ne_eq, not_true] at hz 
[GOAL]
case right.intro.intro.intro.inr
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rwa [T.smul_mem_iff h] at hs 
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
⊢ IsAtom W ↔ ∃ v x, W = span K {v}
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
h : IsAtom W
⊢ ∃ v x, W = span K {v}
[PROOFSTEP]
cases' h with hbot h
[GOAL]
case refine'_1.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
⊢ ∃ v x, W = span K {v}
[PROOFSTEP]
rcases(Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v x, W = span K {v}
[PROOFSTEP]
refine' ⟨v, ⟨hv, _⟩⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = span K {v}
[PROOFSTEP]
by_contra heq
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
⊢ False
[PROOFSTEP]
specialize h (span K { v })
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} < W → span K {v} = ⊥
⊢ False
[PROOFSTEP]
rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h 
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} ≤ W ∧ span K {v} ≠ W → v = 0
⊢ False
[PROOFSTEP]
exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
h : ∃ v x, W = span K {v}
⊢ IsAtom W
[PROOFSTEP]
rcases h with ⟨v, ⟨hv, rfl⟩⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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 : V
hv : v ≠ 0
⊢ IsAtom (span K {v})
[PROOFSTEP]
exact nonzero_span_atom v hv
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
⊢ ∃ s, W = sSup s ∧ ∀ (a : Submodule K V), a ∈ s → IsAtom a
[PROOFSTEP]
refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
⊢ ∀ (a : Submodule K V), a ∈ {T | ∃ m x x, T = span K {m}} → IsAtom a
[PROOFSTEP]
rintro _ ⟨w, ⟨_, ⟨hw, rfl⟩⟩⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
W : Submodule K V
w : V
w✝ : w ∈ W
hw : w ≠ 0
⊢ IsAtom (span K {w})
[PROOFSTEP]
exact nonzero_span_atom w hw
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let B := Basis.ofVectorSpaceIndex K V
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let hB := Basis.ofVectorSpace K V
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ ∃ g, comp g f = id
[PROOFSTEP]
have hB₀ : _ := hB.linearIndependent.to_subtype_range
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ ∃ g, comp g f = id
[PROOFSTEP]
have : LinearIndependent K (fun x => x : f '' B → V') :=
  by
  have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
    @LinearIndependent.image_subtype _ _ _ _ _ _ _ _ _ f hB₀ (show Disjoint _ _ by simp [hf_inj])
  rwa [Basis.range_ofVectorSpace K V] at h₁ 
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
[PROOFSTEP]
have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
  @LinearIndependent.image_subtype _ _ _ _ _ _ _ _ _ f hB₀ (show Disjoint _ _ by simp [hf_inj])
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ Disjoint (span K (Set.range ↑(Basis.ofVectorSpace K V))) (ker f)
[PROOFSTEP]
simp [hf_inj]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
h₁ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
[PROOFSTEP]
rwa [Basis.range_ofVectorSpace K V] at h₁ 
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let C := this.extend (subset_univ _)
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
[PROOFSTEP]
have BC := this.subset_extend (subset_univ _)
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let hC := Basis.extend this
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
⊢ ∃ g, comp g f = id
[PROOFSTEP]
haveI Vinh : Inhabited V := ⟨0⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
⊢ ∃ g, comp g f = id
[PROOFSTEP]
refine' ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
[PROOFSTEP]
rw [image_subset_iff] at BC 
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
[PROOFSTEP]
have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
  change f b = Basis.extend this _
  simp_rw [Basis.extend_apply_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
[PROOFSTEP]
change f b = Basis.extend this _
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b =
    ↑(Basis.extend this)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
[PROOFSTEP]
simp_rw [Basis.extend_apply_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
[PROOFSTEP]
dsimp []
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(↑(Basis.constr (Basis.extend this) ℕ)
          (Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)))
      (↑f (↑(Basis.ofVectorSpace K V) b)) =
    ↑(Basis.ofVectorSpace K V) b
[PROOFSTEP]
rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) } =
    ↑b
[PROOFSTEP]
exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_surj : range f = ⊤
⊢ ∃ g, comp f g = id
[PROOFSTEP]
let C := Basis.ofVectorSpaceIndex K V'
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
⊢ ∃ g, comp f g = id
[PROOFSTEP]
let hC := Basis.ofVectorSpace K V'
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
⊢ ∃ g, comp f g = id
[PROOFSTEP]
haveI : Inhabited V := ⟨0⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
this : Inhabited V
⊢ ∃ g, comp f g = id
[PROOFSTEP]
refine' ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hC.ext fun c => _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
this : Inhabited V
c : ↑(Basis.ofVectorSpaceIndex K V')
⊢ ↑(comp f (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f)))) (↑hC c) = ↑id (↑hC c)
[PROOFSTEP]
rw [LinearMap.comp_apply, hC.constr_basis]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
this : Inhabited V
c : ↑(Basis.ofVectorSpaceIndex K V')
⊢ ↑f (Set.restrict C (invFun ↑f) c) = ↑id (↑hC c)
[PROOFSTEP]
simp [rightInverse_invFun (LinearMap.range_eq_top.1 hf_surj) c]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
f : { x // x ∈ p } →ₗ[K] V'
g : V →ₗ[K] { x // x ∈ p }
hg : comp g (Submodule.subtype p) = id
⊢ comp (comp f g) (Submodule.subtype p) = f
[PROOFSTEP]
rw [LinearMap.comp_assoc, hg, f.comp_id]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
hp : p < ⊤
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
hp : p < ⊤
v : V
hpv : ¬v ∈ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
clear hp
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
rcases(LinearPMap.supSpanSingleton ⟨p, 0⟩ v (1 : K) hpv).toFun.exists_extend with ⟨f, hf⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
refine' ⟨f, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ f ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
hf :
  LinearMap.comp 0 (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ False
[PROOFSTEP]
rw [LinearMap.zero_comp] at hf 
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
hf : 0 = (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ False
[PROOFSTEP]
have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv 0 p.zero_mem 1
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
hf : 0 = (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
this :
  ↑(LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv)
      { val := 0 + 1 • v,
        property :=
          (_ :
            0 + 1 • v ∈
              { domain := p, toFun := 0 }.domain ⊔ (LinearPMap.mkSpanSingleton v 1 (_ : v = 0 → False)).domain) } =
    ↑{ domain := p, toFun := 0 } { val := 0, property := (_ : 0 ∈ p) } + 1 • 1
⊢ False
[PROOFSTEP]
simpa using (LinearMap.congr_fun hf _).trans this
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ p ≤ ker f
[PROOFSTEP]
refine' fun x hx => mem_ker.2 _
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
x : V
hx : x ∈ p
⊢ ↑f x = 0
[PROOFSTEP]
have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv x hx 0
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
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
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
x : V
hx : x ∈ p
this :
  ↑(LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv)
      { val := x + 0 • v,
        property :=
          (_ :
            x + 0 • v ∈
              { domain := p, toFun := 0 }.domain ⊔ (LinearPMap.mkSpanSingleton v 1 (_ : v = 0 → False)).domain) } =
    ↑{ domain := p, toFun := 0 } { val := x, property := hx } + 0 • 1
⊢ ↑f x = 0
[PROOFSTEP]
simpa using (LinearMap.congr_fun hf _).trans this
