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
⊢ Dependent f → ¬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 : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent 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
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : ¬LinearIndependent K ff
⊢ ¬LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
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
⊢ Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)
rintro ⟨ff, hff, hh1⟩
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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K ff
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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : ¬LinearIndependent K ff
⊢ ¬LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
contrapose! hh1
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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K ff
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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K ff
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
case h.e'_4
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ ff = a⁻¹ • Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)
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
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K ff
convert hh1.units_smul a⁻¹
case h.e'_4.h
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
i : ι
⊢ ff i = (a⁻¹ • Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)) i
case h.e'_4
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ ff = a⁻¹ • Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)
ext i
no goals
case h.e'_4.h
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
i : ι
⊢ ff i = (a⁻¹ • Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)) i
simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]
case h.e'_7.h
ι : 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 : ¬LinearIndependent K (Projectivization.rep ∘ f)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) x✝) (_ : ?m.31145 x✝ ≠ 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 : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (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 : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f
convert Dependent.mk _ _ h
no goals
case h.e'_7.h
ι : 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 : ¬LinearIndependent K (Projectivization.rep ∘ f)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) x✝) (_ : ?m.31145 x✝ ≠ 0)
simp only [mk_rep, Function.comp_apply]
no goals
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 : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
exact fun i => rep_nonzero (f i)