awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
i : ι
⊢ Function.comp (β := ℙ K V) Projectivization.rep (fun (i : ι) ↦ mk K (ff i) ⋯) i = (a • ff) i

Tactic:
exact (ha i).symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ Independent.{u_1, u_2, u_3} (K := K) (V := V) fun (i : ι) ↦ mk K ((Projectivization.rep ∘ f) i) ⋯

Tactic:
Independent.mk _ _ h

Premises used: Projectivization.Independent.mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
h₁ : ∀ (x : ι), f x = mk K ((Projectivization.rep ∘ f) x) ⋯
refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
⊢ Independent f

Tactic:
convert! Independent.mk _ _ h

Premises used: Projectivization.Independent.mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
x : ι
⊢ f x = mk K ((Projectivization.rep ∘ f) x) ⋯

Tactic:
simp only [mk_rep, Function.comp_apply]

Premises used: Projectivization.mk_rep, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0

Tactic:
apply rep_nonzero

Premises used: Projectivization.rep_nonzero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule

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

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
refine_1 : Independent f → iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
refine_2 : ∀ (h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule), Independent f
⊢ Independent f ↔ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule

Tactic:
refine ⟨?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
refine_1 : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ K ∙ f i
⊢ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦
    Projectivization.submodule ((fun (i : ι) ↦ (mk K (f i) ⋯ : ℙ K V)) i)

Tactic:
simp only [submodule_mk]

Premises used: Projectivization.submodule_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ K ∙ f i

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

Premises used: Iff.mpr, iSupIndep_iff_linearIndependent_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ K ∙ f i

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

Premises used: Iff.mpr, iSupIndep_iff_linearIndependent_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
refine_2 : LinearIndependent K (Projectivization.rep ∘ f)
⊢ Independent f

Tactic:
rw [independent_iff]

Premises used: Projectivization.independent_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
⊢ LinearIndependent K (Projectivization.rep ∘ f)

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

Premises used: Function.comp, iSupIndep.linearIndependent, Projectivization.submodule
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i
refine_2₁ : ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
⊢ LinearIndependent K (Projectivization.rep ∘ f)

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

Premises used: Function.comp, iSupIndep.linearIndependent, Projectivization.submodule
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) 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 _

Premises used: Projectivization.submodule_eq, Submodule.mem_span_singleton_self, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0

Tactic:
rep_nonzero (f i)

Premises used: Projectivization.rep, Projectivization.rep_nonzero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : iSupIndep.{u_1 + 1, u_3} (α := Submodule K V) fun (i : ι) ↦ (f i).submodule
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0

Tactic:
exact rep_nonzero (f i)

Premises used: Projectivization.rep_nonzero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)

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

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
refine_1 : Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)
refine_2 : ∀ (h : ¬LinearIndependent K (Projectivization.rep ∘ f)), Dependent f
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
refine ⟨?_, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : ¬LinearIndependent K ff
refine_1 :
  ∀
    (hh1 :
      LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
        (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)),
    LinearIndependent K ff
⊢ ¬LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
      (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)

Tactic:
contrapose hh1
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
refine_1 :
  ∀ (a : (i : ι) → Kˣ) (ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)), LinearIndependent K ff
⊢ LinearIndependent K ff

Tactic:
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)

Premises used: Projectivization.exists_smul_eq_mk_rep
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
⊢ LinearIndependent K
    (HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯))

Tactic:
hh1.units_smul a⁻¹

Premises used: Inv.inv, LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
h : ff = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
⊢ LinearIndependent K ff

Tactic:
convert! hh1.units_smul a⁻¹

Premises used: Inv.inv, LinearIndependent.units_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
h :
  ∀ (i : ι),
    ff i = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯) i
⊢ ff = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 :
  LinearIndependent.{u_1, u_2, u_3} (ι := ι) K (M := V)
    (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯)
a : (i : ι) → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) ⋯)
i : ι
⊢ ff i = HSMul.hSMul (β := ι → V) a⁻¹ (Function.comp (β := ℙ K V) Projectivization.rep fun (i : ι) ↦ mk K (ff i) ⋯) i

Tactic:
simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]

Premises used: Pi.smul_apply', inv_smul_smul, Function.comp_apply, Pi.inv_apply
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent.{u_1, u_2, u_3} (K := K) (V := V) fun (i : ι) ↦ mk K ((Projectivization.rep ∘ f) i) ⋯

Tactic:
Dependent.mk _ _ h

Premises used: Projectivization.Dependent.mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
h₁ : ∀ (x : ι), f x = mk K ((Projectivization.rep ∘ f) x) ⋯
refine_2 : ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
⊢ Dependent f

Tactic:
convert! Dependent.mk _ _ h

Premises used: Projectivization.Dependent.mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
x : ι
⊢ f x = mk K ((Projectivization.rep ∘ f) x) ⋯

Tactic:
simp only [mk_rep, Function.comp_apply]

Premises used: Projectivization.mk_rep, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0

Tactic:
fun i => rep_nonzero (f i)

Premises used: Projectivization.rep, Projectivization.rep_nonzero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0

Tactic:
exact fun i => rep_nonzero (f i)

Premises used: Projectivization.rep_nonzero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
rw : ¬LinearIndependent K (Projectivization.rep ∘ f) ↔ ¬Independent f
rw₁ rw₂ : ¬LinearIndependent K (Projectivization.rep ∘ f) ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f ↔ ¬Independent f

Tactic:
rw [dependent_iff, independent_iff]

Premises used: Projectivization.dependent_iff, Projectivization.independent_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : ι → ℙ K V
rw : Independent f ↔ ¬¬Independent f
rw₁ rw₂ : Independent f ↔ Independent f
⊢ Independent f ↔ ¬Dependent f

Tactic:
rw [dependent_iff_not_independent, Classical.not_not]

Premises used: Classical.not_not, Projectivization.dependent_iff_not_independent
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
rw :
  ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v
⊢ Dependent ![u, v] ↔ u = v

Tactic:
rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2]

Premises used: linearIndependent_fin2, Projectivization.dependent_iff_not_independent, Projectivization.independent_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
dsimp : ¬(v.rep ≠ 0 ∧ ∀ (a : K), a • v.rep ≠ u.rep) ↔ u = v
⊢ ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v

Tactic:
dsimp only [Function.comp_def, Matrix.cons_val]

Premises used: Function.comp_def, Matrix.cons_val
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
simp : v.rep ≠ 0 ∨ u = v
⊢ ¬(v.rep ≠ 0 ∧ ∀ (a : K), a • v.rep ≠ u.rep) ↔ u = v

Tactic:
simp only [not_and, not_forall, not_not, ← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v),
    mk_rep, Classical.imp_iff_right_iff]

Premises used: Classical.not_not, Projectivization.mk_rep, Projectivization.rep_nonzero, Classical.imp_iff_right_iff, Projectivization.mk_eq_mk_iff', not_and, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
⊢ v.rep ≠ 0 ∨ u = v

Tactic:
Or.inl (rep_nonzero v)

Premises used: Projectivization.rep_nonzero, Or.inl
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
⊢ v.rep ≠ 0 ∨ u = v

Tactic:
exact Or.inl (rep_nonzero v)

Premises used: Projectivization.rep_nonzero, Or.inl
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
rw : ¬Dependent ![u, v] ↔ u ≠ v
rw₁ rw₂ : ¬u = v ↔ u ≠ v
⊢ Independent ![u, v] ↔ u ≠ v

Tactic:
rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]

Premises used: Projectivization.dependent_pair_iff_eq, Projectivization.independent_iff_not_dependent
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
rw : (¬∃ (a : K), a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0
⊢ Independent ![mk K u hu, mk K v hv] ↔ LinearIndependent K ![u, v]

Tactic:
rw [independent_pair_iff_ne, ne_eq, mk_eq_mk_iff' K u v hu hv, linearIndependent_fin2]

Premises used: linearIndependent_fin2, ne_eq, Projectivization.independent_pair_iff_ne, Projectivization.mk_eq_mk_iff'
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
simp : (¬∃ (a : K), a • v = u) ↔ v ≠ 0 ∧ ∀ (a : K), a • v ≠ u
⊢ (¬∃ (a : K), a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0

Tactic:
simp only [Matrix.cons_val_zero, Matrix.cons_val_one]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ (a : K), a • v = u) ↔ v ≠ 0 ∧ ∀ (a : K), a • v ≠ u

Tactic:
⟨fun h ↦ ⟨hv, fun a ha ↦ h ⟨a, ha⟩⟩, fun ⟨_, h⟩ ⟨a, ha⟩ ↦ h a ha⟩

Premises used: False, _private.0.Projectivization.independent_mk_iff_LinearIndependent.match_1, _private.0.Projectivization.independent_mk_iff_LinearIndependent.match_2, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Independence
Goal:
K : Type u_2
V : Type u_3
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ (a : K), a • v = u) ↔ v ≠ 0 ∧ ∀ (a : K), a • v ≠ u

Tactic:
exact ⟨fun h ↦ ⟨hv, fun a ha ↦ h ⟨a, ha⟩⟩, fun ⟨_, h⟩ ⟨a, ha⟩ ↦ h a ha⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A B : Subspace K V
mk :
  ∀ (carrier : Set (ℙ K V))
    (mem_add' :
      ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
        Projectivization.mk K v hv ∈ carrier →
          Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier),
    { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier = B.carrier →
      { carrier := carrier, mem_add' := mem_add' : Subspace K V } = B
⊢ A.carrier = B.carrier → A = B

Tactic:
cases A
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : Subspace K V
carrier : Set (ℙ K V)
mem_add' :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier →
      Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier
mk :
  ∀ (carrier_1 : Set (ℙ K V))
    (mem_add'_1 :
      ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
        Projectivization.mk K v hv ∈ carrier_1 →
          Projectivization.mk K w hw ∈ carrier_1 → Projectivization.mk K (v + w) hvw ∈ carrier_1),
    { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier =
        { carrier := carrier_1, mem_add' := mem_add'_1 }.carrier →
      { carrier := carrier, mem_add' := mem_add' : Subspace K V } = { carrier := carrier_1, mem_add' := mem_add'_1 }
⊢ { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier = B.carrier →
    { carrier := carrier, mem_add' := mem_add' : Subspace K V } = B

Tactic:
cases B
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
carrier : Set (ℙ K V)
mem_add' :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier →
      Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier
carrier_1 : Set (ℙ K V)
mem_add'_1 :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier_1 →
      Projectivization.mk K w hw ∈ carrier_1 → Projectivization.mk K (v + w) hvw ∈ carrier_1
⊢ { carrier := carrier, mem_add' := mem_add' : Subspace K V }.carrier =
      { carrier := carrier_1, mem_add' := mem_add'_1 }.carrier →
    { carrier := carrier, mem_add' := mem_add' : Subspace K V } = { carrier := carrier_1, mem_add' := mem_add'_1 }

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Subspace K V
x : ℙ K V
⊢ x ∈ A.carrier ↔ x ∈ A

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
T : Subspace K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
⊢ Projectivization.mk K v hv ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.mk K (v + w) hvw ∈ T

Tactic:
T.mem_add' v w hv hw hvw

Premises used: Projectivization.Subspace.mem_add', Set.Mem
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
⊢ S ⊆ (↑(span S) : Set (ℙ K V))

Tactic:
fun _x hx => spanCarrier.of _ hx

Premises used: Projectivization.Subspace.spanCarrier.of, Set.Mem, Set.Subset
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ (↑B : Set (ℙ K V))
x x_1 : ℙ K V
hx of : x_1 ∈ A
⊢ x_1 ∈ B

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ (↑B : Set (ℙ K V))
x x_1 : ℙ K V
hx : x_1 ∈ A
⊢ x_1 ∈ A

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ (↑B : Set (ℙ K V))
x : ℙ K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h_1 : spanCarrier A (Projectivization.mk K v hv)
h_2 : spanCarrier A (Projectivization.mk K w hw)
a_ih : Projectivization.mk K v hv ∈ B
a_ih_1 : Projectivization.mk K w hw ∈ B
mem_add : Projectivization.mk K v hv ∈ B
mem_add₁ : Projectivization.mk K w hw ∈ B
mem_add₂ : v ≠ 0
mem_add₃ : w ≠ 0
⊢ Projectivization.mk K (v + w) hvw ∈ B

Tactic:
apply B.mem_add

Premises used: Projectivization.Subspace.mem_add