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
⊢ IsUnit
    (HAdd.hAdd (α := K) (β := K) (1 : K)
      ((b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) : (a : V) → 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)) :
        K))

Tactic:
simp
-- 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
pos :
  (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ)
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
        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))
        ⋯) =
    a
pos₁ :
  HSMul.hSMul (α := V ≃ₗ[K] V) (β := ℙ K V)
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
        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))
        ⋯)
      (mk K D.rep ⋯) =
    mk K D.rep ⋯
pos₂ :
  HSMul.hSMul (α := V ≃ₗ[K] V) (β := ℙ K V)
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
        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))
        ⋯)
      (mk K D'.rep ⋯) =
    mk K D'.rep ⋯
⊢ ∃ (h : V ≃ₗ[K] V),
    (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧
      HSMul.hSMul (β := ℙ K V) h (mk K D.rep ⋯) = mk K D.rep ⋯ ∧
        HSMul.hSMul (β := ℙ K V) h (mk K D'.rep ⋯) = mk K D'.rep ⋯

Tactic:
refine ⟨dilatransvection (f := b.coord ⟨D.rep, hD_mem⟩)
      (v := (a.val - 1) • b ⟨D.rep, hD_mem⟩) (by simp), ?_, ?_, ?_⟩
-- 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
⊢ (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ)
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
        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))
        ⋯) =
    a

Tactic:
simp [← Units.val_inj, coe_det, LinearMap.transvection.det]

Premises used: Units.val_inj, LinearMap.transvection.det, 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_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
pos :
  ∃ (a_1 : Kˣ),
    a_1 • D.rep =
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
            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))
            ⋯ :
          (a : V) → V)
        D.rep
⊢ HSMul.hSMul (α := V ≃ₗ[K] V) (β := ℙ K V)
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
        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))
        ⋯)
      (mk K D.rep ⋯) =
    mk K D.rep ⋯

Tactic:
rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]

Premises used: Projectivization.mk_eq_mk_iff, LinearEquiv.smul_def, Projectivization.smul_mk
-- 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 :
  a • D.rep =
    (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
          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))
          ⋯ :
        (a : V) → V)
      D.rep
⊢ ∃ (a_1 : Kˣ),
    a_1 • D.rep =
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
            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))
            ⋯ :
          (a : V) → V)
        D.rep

Tactic:
use a
-- 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 :
  a • 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))
⊢ a • D.rep =
    (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
          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))
          ⋯ :
        (a : V) → V)
      D.rep

Tactic:
rw [← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]

Premises used: LinearEquiv.dilatransvection.coe_toLinearMap, LinearMap.transvection.apply, Module.Basis.coord_apply, LinearEquiv.coe_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
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_2 : 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_2
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this :
  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)
    (1 : K)
rw :
  (↑a : K) • D.rep =
    D.rep +
      HSMul.hSMul.{u_1, u_2, u_2} (α := K) 1
        (((↑a : K) - 1) • (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) : V))
⊢ a • 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:
rw [this, Module.Basis.extend_apply_self, Units.smul_def]

Premises used: Module.Basis.extend_apply_self, Units.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
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_2 : 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_2
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this :
  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)
    (1 : K)
⊢ (↑a : K) • D.rep =
    D.rep +
      HSMul.hSMul.{u_1, u_2, u_2} (α := K) 1
        (((↑a : K) - 1) • (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) : V))

Tactic:
module
-- 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)
    (1 : K)
⊢ a • 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⟩ = 1 by
        rw [this, Module.Basis.extend_apply_self, Units.smul_def]
        module
-- 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)
    (1 : 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)
    (1 : 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)
    (1 : 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)
    (1 : 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
⊢ 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)
    (1 : K)

Tactic:
simp
-- 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
pos :
  ∃ (a_1 : Kˣ),
    a_1 • D'.rep =
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
            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))
            ⋯ :
          (a : V) → V)
        D'.rep
⊢ HSMul.hSMul (α := V ≃ₗ[K] V) (β := ℙ K V)
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
        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))
        ⋯)
      (mk K D'.rep ⋯) =
    mk K D'.rep ⋯

Tactic:
rw [smul_mk, mk_eq_mk_iff, LinearEquiv.smul_def]

Premises used: Projectivization.mk_eq_mk_iff, LinearEquiv.smul_def, Projectivization.smul_mk
-- 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 :
  HSMul.hSMul.{u_1, u_2, u_2} (α := Kˣ) 1 D'.rep =
    (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
          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))
          ⋯ :
        (a : V) → V)
      D'.rep
⊢ ∃ (a_1 : Kˣ),
    a_1 • D'.rep =
      (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
            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))
            ⋯ :
          (a : V) → V)
        D'.rep

Tactic:
use 1
-- 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 +
      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))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Kˣ) 1 D'.rep =
    (dilatransvection (f := b.coord (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem)) (v :=
          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))
          ⋯ :
        (a : V) → V)
      D'.rep

Tactic:
rw [one_smul, ← coe_coe, dilatransvection.coe_toLinearMap,
        LinearMap.transvection.apply, Module.Basis.coord_apply]

Premises used: LinearEquiv.dilatransvection.coe_toLinearMap, LinearMap.transvection.apply, one_smul, Module.Basis.coord_apply, LinearEquiv.coe_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
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_2 : 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_2
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this :
  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)
rw :
  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)
        (((↑a : K) - 1) • (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) : V))
⊢ 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:
rw [Module.Basis.extend_apply_self]

Premises used: Module.Basis.extend_apply_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_2 : 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_2
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
this :
  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)
        (((↑a : K) - 1) • (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) : V))

Tactic:
simp [this]