-- Mathlib/LinearAlgebra/Projectivization/Independence.lean
theorem independent_iff_iSupIndep : Independent f ↔ iSupIndep fun i => (f i).submodule

Proof state:
case refine_2.refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0

Tactic:
exact rep_nonzero (f i)

Result:
no goals

Proof state:
case refine_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep fun i => Submodule.span K {f i}

Tactic:
exact (iSupIndep_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi

Result:
no goals

Proof state:
case refine_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep fun i => ((fun i => mk K (f i) ⋯) i).submodule

Tactic:
simp only [submodule_mk]

Result:
case refine_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep fun i => Submodule.span K {f i}

Proof state:
case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
⊢ Independent f

Tactic:
rw [independent_iff]

Result:
case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
⊢ LinearIndependent K (Projectivization.rep ∘ f)

Proof state:
case refine_2.refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
i : ι
⊢ (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i

Tactic:
simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _

Result:
no goals

Proof state:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ iSupIndep fun i => (f i).submodule

Tactic:
refine ⟨?_, fun h => ?_⟩

Result:
case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → iSupIndep fun i => (f i).submodule

case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
⊢ Independent f

Proof state:
case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
⊢ LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
refine h.linearIndependent (Projectivization.submodule ∘ f) (fun i => ?_) fun i => ?_

Result:
case refine_2.refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
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✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i => (f i).submodule
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0

Proof state:
case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → iSupIndep fun i => (f i).submodule

Tactic:
rintro ⟨f, hf, hi⟩

Result:
case refine_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep fun i => ((fun i => mk K (f i) ⋯) i).submodule