case refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → CompleteLattice.Independent fun i => Projectivization.submodule (f i)

case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
⊢ Independent f
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ CompleteLattice.Independent fun i => Projectivization.submodule (f i)
refine' ⟨_, fun h => _⟩
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ CompleteLattice.Independent fun i => Projectivization.submodule ((fun i => mk K (f i) (_ : f i ≠ 0)) i)
case refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → CompleteLattice.Independent fun i => Projectivization.submodule (f i)
rintro ⟨f, hf, hi⟩
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ CompleteLattice.Independent fun i => Submodule.span K {f i}
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ CompleteLattice.Independent fun i => Projectivization.submodule ((fun i => mk K (f i) (_ : f i ≠ 0)) i)
simp only [submodule_mk]
no goals
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ CompleteLattice.Independent fun i => Submodule.span K {f i}
exact (CompleteLattice.independent_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
⊢ LinearIndependent K (Projectivization.rep ∘ f)
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
⊢ Independent f
rw [independent_iff]
case refine'_2.refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
i : ι
⊢ (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i

case refine'_2.refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
⊢ LinearIndependent K (Projectivization.rep ∘ f)
refine' h.linearIndependent (Projectivization.submodule ∘ f) (fun i => _) fun i => _
no goals
case refine'_2.refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
i : ι
⊢ (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i
simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _
no goals
case refine'_2.refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0
exact rep_nonzero (f i)