awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h :
  Eq.{u_1 + 1} (α := K)
    ((((b.repr : (a : V) → (↑s : Type u_2) →₀ K) D'.rep : Finsupp.{u_2, u_1} (↑s : Type u_2) K) :
          (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)
⊢ D'.rep =
    D'.rep +
      HSMul.hSMul.{u_1, u_2, u_2} (α := K)
        ((((b.repr : (a : V) → (↑s : Type u_2) →₀ K) D'.rep : Finsupp.{u_2, u_1} (↑s : Type u_2) K) :
              (a : (↑s : Type u_2)) → K)
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
          K)
        (HSMul.hSMul (β := V) ((↑a : K) - 1)
          ((b : (a : (↑s : Type u_2)) → V) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) : V))

Tactic:
suffices (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0 by
        rw [Module.Basis.extend_apply_self]
        simp [this]
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ D'.rep = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) : V)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h :
  Eq.{u_1 + 1} (α := K)
    ((((b.repr : (a : V) → (↑s : Type u_2) →₀ K) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) : V) :
            Finsupp.{u_2, u_1} (↑s : Type u_2) K) :
          (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)
⊢ Eq.{u_1 + 1} (α := K)
    ((((b.repr : (a : V) → (↑s : Type u_2) →₀ K) D'.rep : Finsupp.{u_2, u_1} (↑s : Type u_2) K) :
          (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)

Tactic:
nth_rewrite 1 [show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) from by rfl]
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h :
  Eq.{u_1 + 1} (α := K)
    ((Finsupp.single (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) 1 : (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)
⊢ Eq.{u_1 + 1} (α := K)
    ((((b.repr : (a : V) → (↑s : Type u_2) →₀ K) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) : V) :
            Finsupp.{u_2, u_1} (↑s : Type u_2) K) :
          (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)

Tactic:
rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]

Premises used: Module.Basis.extend_apply_self, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem
⊢ Eq.{u_1 + 1} (α := K)
    ((Finsupp.single (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) 1 : (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)

Tactic:
apply Finsupp.single_eq_of_ne

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : ¬D.rep = D'.rep
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem

Tactic:
simp only [ne_eq, ← Subtype.coe_inj]

Premises used: Subtype.coe_inj, ne_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : D.rep = D'.rep
h₁ : Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 2)) 0 1
h₂ : ℕ
⊢ False

Tactic:
apply Fin.zero_ne_one

Premises used: Fin.zero_ne_one
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this_1 : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
s : Set V := ⋯.extend (s := {D.rep, D'.rep}) (t := Set.univ) ⋯
b : Module.Basis (↑s : Type u_2) K V := Module.Basis.extend (s := {D.rep, D'.rep}) this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : D.rep = D'.rep
⊢ ![D.rep, D'.rep] 0 = ![D.rep, D'.rep] 1

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
rw : Eq.{u_1 + 1} (α := K) ((LinearMap.det : (a : V →ₗ[K] V) → K) (↑g : V →ₗ[K] V) : K) ((↑1 : K) : K)
⊢ Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) g : Kˣ) (1 : Kˣ)

Tactic:
rw [← Units.val_inj, coe_det]

Premises used: Units.val_inj, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ Eq.{u_1 + 1} (α := K) ((LinearMap.det : (a : V →ₗ[K] V) → K) (↑g : V →ₗ[K] V) : K) ((↑1 : K) : K)

Tactic:
apply LinearMap.det_eq_one_of_not_module_finite hV

Premises used: LinearMap.det_eq_one_of_not_module_finite
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
h :
  HSMul.hSMul (α := SpecialLinearGroup K V)
        (Subtype.mk (p := fun (u : V ≃ₗ[K] V) ↦
          Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) u : Kˣ) (1 : Kˣ)) g ⋯)
        D =
      E ∧
    HSMul.hSMul (α := SpecialLinearGroup K V)
        (Subtype.mk (p := fun (u : V ≃ₗ[K] V) ↦
          Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) u : Kˣ) (1 : Kˣ)) g ⋯)
        D' =
      E'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'

Tactic:
use ⟨g, by
    rw [← Units.val_inj, coe_det]
    apply LinearMap.det_eq_one_of_not_module_finite hV⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : ¬FiniteDimensional K V
⊢ HSMul.hSMul (α := SpecialLinearGroup K V)
        (Subtype.mk (p := fun (u : V ≃ₗ[K] V) ↦
          Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) u : Kˣ) (1 : Kˣ)) g ⋯)
        D =
      E ∧
    HSMul.hSMul (α := SpecialLinearGroup K V)
        (Subtype.mk (p := fun (u : V ≃ₗ[K] V) ↦
          Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) u : Kˣ) (1 : Kˣ)) g ⋯)
        D' =
      E'

Tactic:
simp [← gD, ← gE, specialLinearGroup_smul_def, toLinearEquiv_eq_coe]

Premises used: Projectivization.specialLinearGroup_smul_def, SpecialLinearGroup.toLinearEquiv_eq_coe
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
⊢ IsPreprimitive.{u_2, u_2} (SpecialLinearGroup K V) (ℙ K V)

Tactic:
isPreprimitive_of_is_two_pretransitive inferInstance

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive, inferInstance
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
ι : Type u_3
inst_3 : Fintype ι
inst_4 : DecidableEq ι
φ : SpecialLinearGroup K (ι → K) →* Matrix.SpecialLinearGroup ι K :=
  MulEquiv.toMonoidHom (MulEquiv.symm Matrix.SpecialLinearGroup.toLin'_equiv)
g : SpecialLinearGroup K (ι → K)
D : ℙ K (ι → K)
⊢ id (g • D) =
    HSMul.hSMul (α := Matrix.SpecialLinearGroup ι K)
      ((φ : (a : SpecialLinearGroup K (ι → K)) → Matrix.SpecialLinearGroup ι K) g : Matrix.SpecialLinearGroup ι K)
      (id D)

Tactic:
simp [φ, matrixSpecialLinearGroup_smul_def]

Premises used: Projectivization.matrixSpecialLinearGroup_smul_def
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_1
V : Type u_2
inst : AddCommGroup V
inst_1 : Field K
inst_2 : Module K V
ι : Type u_3
inst_3 : Fintype ι
inst_4 : DecidableEq ι
⊢ IsPreprimitive (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))

Tactic:
isPreprimitive_of_is_two_pretransitive inferInstance

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive, inferInstance
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : { v : V // v ≠ 0 }
⊢ Eq (α := ℙ K V) (mk' K v) (mk K (↑v : V) ⋯)

Tactic:
rfl

Premises used: Projectivization.mk, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Nontrivial V
⊢ Nonempty.{u_2 + 1} (ℙ K V)

Tactic:
let ⟨v, hv⟩ := exists_ne (0 : V)
  ⟨mk K v hv⟩

Premises used: Projectivization.mk, exists_ne, _private.0.Projectivization.instNonemptyOfNontrivial.match_1, Nonempty.intro, Nonempty, OfNat.ofNat, Projectivization
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
α : Type u_3
f : { v : V // v ≠ 0 } → α
hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), (↑a : V) = t • (↑b : V) → f a = f b
x : ℙ K V
w : V
hw : w ≠ 0
t inv : K
val_inv : t * inv = 1
inv_val : inv * t = 1
hv :
  Ne.{u_2 + 1} (α := V)
    ((fun (m : Kˣ) ↦ m • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) w hw) : V))
      { val := t, inv := inv, val_inv := val_inv, inv_val := inv_val })
    0
⊢ f
      (Subtype.mk (p := fun (v : V) ↦ v ≠ 0)
        ((fun (m : Kˣ) ↦ m • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) w hw) : V))
          { val := t, inv := inv, val_inv := val_inv, inv_val := inv_val : Kˣ })
        hv) =
    f (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) w hw)

Tactic:
hf ⟨_, hv⟩ ⟨w, hw⟩ t rfl

Premises used: Subtype.mk, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
α : Type u_3
f : { v : V // v ≠ 0 } → α
hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), (↑a : V) = t • (↑b : V) → f a = f b
x : ℙ K V
w : V
hw : w ≠ 0
t inv : K
val_inv : t * inv = 1
inv_val : inv * t = 1
hv :
  Ne.{u_2 + 1} (α := V)
    ((fun (m : Kˣ) ↦ m • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) w hw) : V))
      { val := t, inv := inv, val_inv := val_inv, inv_val := inv_val })
    0
⊢ f
      (Subtype.mk (p := fun (v : V) ↦ v ≠ 0)
        ((fun (m : Kˣ) ↦ m • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) w hw) : V))
          { val := t, inv := inv, val_inv := val_inv, inv_val := inv_val : Kˣ })
        hv) =
    f (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) w hw)

Tactic:
exact hf ⟨_, hv⟩ ⟨w, hw⟩ t rfl

Premises used: Subtype.mk, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
α : Type u_3
f : { v : V // v ≠ 0 } → α
hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), (↑a : V) = t • (↑b : V) → f a = f b
v : V
hv : v ≠ 0
⊢ Projectivization.lift f hf (mk K v hv) = f (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v hv)

Tactic:
rfl

Premises used: Projectivization.lift, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ v.rep ≠ 0

Tactic:
v.out.2

Premises used: Projectivization.rep, Quotient.out, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ mk K v.rep ⋯ = v

Tactic:
Quotient.out_eq' _

Premises used: Projectivization.mk, Quotient.out_eq', Quot.out, Projectivization.rep, Quotient.out, Classical.choose, Projectivization
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
b : V
hb : b ≠ 0
x : Kˣ
ha : x • b ≠ 0
⊢ Eq (α := Submodule K V) (K ∙ (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) (x • b) ha) : V))
    (K ∙ (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) b hb) : V))

Tactic:
Submodule.span_singleton_group_smul_eq _ x _

Premises used: Submodule.span_singleton_group_smul_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
b : V
hb : b ≠ 0
x : Kˣ
ha : x • b ≠ 0
⊢ Eq (α := Submodule K V) (K ∙ (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) (x • b) ha) : V))
    (K ∙ (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) b hb) : V))

Tactic:
exact Submodule.span_singleton_group_smul_eq _ x _

Premises used: Submodule.span_singleton_group_smul_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ Eq (α := ℙ K V) (mk K v hv) (mk K w hw) ↔ ∃ (a : Kˣ), a • w = v

Tactic:
Quotient.eq''

Premises used: Projectivization.mk, Set.Mem, Quotient.eq'', setOf, MulAction.orbit, Set.range, Projectivization
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
rw : (∃ (a : Kˣ), a • w = v) ↔ ∃ (a : K), a • w = v
⊢ Eq (α := ℙ K V) (mk K v hv) (mk K w hw) ↔ ∃ (a : K), a • w = v

Tactic:
rw [mk_eq_mk_iff K v w hv hw]

Premises used: Projectivization.mk_eq_mk_iff
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
mp : (∃ (a : Kˣ), a • w = v) → ∃ (a : K), a • w = v
mpr : (∃ (a : K), a • w = v) → ∃ (a : Kˣ), a • w = v
⊢ (∃ (a : Kˣ), a • w = v) ↔ ∃ (a : K), a • w = v

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ (a : K), a • w = v

Tactic:
⟨a, ha⟩

Premises used: Units.val, Exists.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ (a : K), a • w = v

Tactic:
exact ⟨a, ha⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ (a : Kˣ), a • w = v

Tactic:
⟨Units.mk0 a fun c => hv.symm ?_, ha⟩

Premises used: Ne.symm, Units.mk0, Exists.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
mpr : ∀ (c : a = 0), 0 = v
⊢ ∃ (a : Kˣ), a • w = v

Tactic:
refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
mpr : ∀ (ha : HSMul.hSMul.{u_1, u_2, u_2} (α := K) 0 w = v) (c : a = 0), 0 = v
mpr₁ mpr₂ mpr₃ mpr₄ : ∀ (ha : 0 = v) (c : a = 0), 0 = v
⊢ 0 = v

Tactic:
rwa [c, zero_smul] at ha

Premises used: zero_smul
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ ∃ (a : Kˣ), a • v = Projectivization.rep (mk K v hv)

Tactic:
(mk_eq_mk_iff K _ _ (rep_nonzero _) hv).1 (mk_rep _)

Premises used: Projectivization.mk_eq_mk_iff, Projectivization.mk_rep, Projectivization.rep_nonzero, Iff.mp
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
P : ℙ K V → Prop
h : ∀ (v : V) (h : v ≠ 0), P (mk K v h)
⊢ ∀ (p : ℙ K V), P p

Tactic:
Quotient.ind' <| Subtype.rec <| h

Premises used: Quotient.ind', Projectivization
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ Eq (α := Submodule K V) (Projectivization.submodule (mk K v hv)) (K ∙ v)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, setOf, Submodule.span, Projectivization.submodule, rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
rw : Projectivization.submodule (mk K v.rep ⋯)
| v.submodule

Tactic:
rw [← v.mk_rep]

Premises used: Projectivization.mk_rep
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
conv_lhs : Eq (α := Submodule K V) (Projectivization.submodule (mk K v.rep ⋯)) (K ∙ v.rep)
⊢ v.submodule = K ∙ v.rep

Tactic:
conv_lhs => rw [← v.mk_rep]

Premises used: Projectivization.mk_rep
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ Eq (α := Submodule K V) (Projectivization.submodule (mk K v.rep ⋯)) (K ∙ v.rep)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
rw : finrank.{u_1, u_2} K ↥(K ∙ v.rep) = 1
⊢ finrank.{u_1, u_2} K ↥v.submodule = 1

Tactic:
rw [submodule_eq]

Premises used: Projectivization.submodule_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ finrank.{u_1, u_2} K ↥(K ∙ v.rep) = 1

Tactic:
finrank_span_singleton v.rep_nonzero

Premises used: Projectivization.rep_nonzero, finrank_span_singleton
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ finrank.{u_1, u_2} K ↥(K ∙ v.rep) = 1

Tactic:
exact finrank_span_singleton v.rep_nonzero

Premises used: Projectivization.rep_nonzero, finrank_span_singleton
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
rw : FiniteDimensional.{u_1, u_2} K ↥(Projectivization.submodule (mk K v.rep ⋯))
⊢ FiniteDimensional.{u_1, u_2} K ↥v.submodule

Tactic:
rw [← v.mk_rep]

Premises used: Projectivization.mk_rep
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
change : FiniteDimensional.{u_1, u_2} K ↥(K ∙ v.rep)
⊢ FiniteDimensional.{u_1, u_2} K ↥(Projectivization.submodule (mk K v.rep ⋯))

Tactic:
change FiniteDimensional K (K ∙ v.rep)

Premises used: Projectivization.rep, Membership.mem, Subtype, FiniteDimensional, Submodule.span, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ FiniteDimensional.{u_1, u_2} K ↥(K ∙ v.rep)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : Eq (α := Submodule K V) (Projectivization.submodule (mk K u hu)) (Projectivization.submodule (mk K v hv))
⊢ ∃ (z : Kˣ), z • u = v

Tactic:
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h

Premises used: Projectivization.submodule_mk, Submodule.span_singleton_eq_span_singleton