awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 0 1)) :
        V) =
      D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1)) :
        V) =
      D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional.{u_2, u_3} K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg :
  ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))),
    Eq (α := V)
      ((↑((f :
                (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) →
                  ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
              x) :
          V) :
        V)
      ((g : (a : V) → V) (↑x : V) : V)
⊢ Eq.{u_3 + 1} (α := V)
    (↑((hE.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
          (Finsupp.single 0 1)) :
      V)
    (↑((f : (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) → ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
          ((hD.linearCombinationEquiv :
              (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 0 1))) :
      V)

Tactic:
simp [f]
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 0 1)) :
        V) =
      D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1)) :
        V) =
      D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional.{u_2, u_3} K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg :
  ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))),
    Eq (α := V)
      ((↑((f :
                (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) →
                  ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
              x) :
          V) :
        V)
      ((g : (a : V) → V) (↑x : V) : V)
h : ∃ (a : Kˣ), a • E'.rep = g • D'.rep
⊢ g • D' = E'

Tactic:
rw [← mk_rep D', ← mk_rep E', smul_mk, mk_eq_mk_iff]

Premises used: Projectivization.mk_eq_mk_iff, Projectivization.mk_rep, Projectivization.smul_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 0 1)) :
        V) =
      D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1)) :
        V) =
      D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional.{u_2, u_3} K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg :
  ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))),
    Eq (α := V)
      ((↑((f :
                (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) →
                  ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
              x) :
          V) :
        V)
      ((g : (a : V) → V) (↑x : V) : V)
h : HSMul.hSMul.{u_2, u_3, u_3} (α := Kˣ) 1 E'.rep = g • D'.rep
⊢ ∃ (a : Kˣ), a • E'.rep = g • D'.rep

Tactic:
use 1
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 0 1)) :
        V) =
      D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1)) :
        V) =
      D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional.{u_2, u_3} K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg :
  ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))),
    Eq (α := V)
      ((↑((f :
                (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) →
                  ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
              x) :
          V) :
        V)
      ((g : (a : V) → V) (↑x : V) : V)
h :
  Eq.{u_3 + 1} (α := V)
    (↑((hE.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
          (Finsupp.single 1 1)) :
      V)
    (↑((f : (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) → ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
          ((hD.linearCombinationEquiv :
              (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1))) :
      V)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Kˣ) 1 E'.rep = g • D'.rep

Tactic:
simp only [one_smul, LinearEquiv.smul_def, ← qD' hD, ← hg, ← qD' hE]

Premises used: one_smul, LinearEquiv.smul_def
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : LinearIndependent K ![E.rep, E'.rep]
qD :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 0 1)) :
        V) =
      D.rep
qD' :
  ∀ {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]),
    (↑((hD.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1)) :
        V) =
      D'.rep
f : ↥(Submodule.span K (Set.range ![D.rep, D'.rep])) ≃ₗ[K] ↥(Submodule.span K (Set.range ![E.rep, E'.rep])) :=
  hD.linearCombinationEquiv.symm ≪≫ₗ hE.linearCombinationEquiv
this : FiniteDimensional.{u_2, u_3} K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))
g : V ≃ₗ[K] V
hg :
  ∀ (x : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))),
    Eq (α := V)
      ((↑((f :
                (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) →
                  ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
              x) :
          V) :
        V)
      ((g : (a : V) → V) (↑x : V) : V)
⊢ Eq.{u_3 + 1} (α := V)
    (↑((hE.linearCombinationEquiv : (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
          (Finsupp.single 1 1)) :
      V)
    (↑((f : (a : ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))) → ↥(Submodule.span K (Set.range ![E.rep, E'.rep])))
          ((hD.linearCombinationEquiv :
              (a : Fin (Nat.succ 0).succ →₀ K) → ↥(Submodule.span K (Set.range ![D.rep, D'.rep])))
            (Finsupp.single 1 1))) :
      V)

Tactic:
simp [f]
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
simp : e • D = LinearMap.GeneralLinearGroup.ofLinearEquiv e • D
⊢ id (e • D) = LinearMap.GeneralLinearGroup.ofLinearEquiv e • id D

Tactic:
simp only [id_eq]

Premises used: id_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
rw : Eq (α := ℙ K V) (mk K (e • D.rep) ⋯) (mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) ⋯)
⊢ e • D = LinearMap.GeneralLinearGroup.ofLinearEquiv e • D

Tactic:
rw [← mk_rep D, smul_mk, smul_mk]

Premises used: Projectivization.mk_rep, Projectivization.smul_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ Eq (α := ℙ K V) (mk K (e • D.rep) ⋯) (mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) ⋯)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
f : MulActionHom (M := V ≃ₗ[K] V) LinearMap.GeneralLinearGroup.ofLinearEquiv (ℙ K V) (ℙ K V) :=
  { toFun := id, map_smul' := ⋯ }
⊢ IsMultiplyPretransitive.{u_3, u_3} (LinearMap.GeneralLinearGroup K V) (ℙ K V) 2

Tactic:
IsPretransitive.of_embedding (f := f) Function.surjective_id

Premises used: MulAction.IsPretransitive.of_embedding, Function.surjective_id
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
f : MulActionHom (M := V ≃ₗ[K] V) LinearMap.GeneralLinearGroup.ofLinearEquiv (ℙ K V) (ℙ K V) :=
  { toFun := id, map_smul' := ⋯ }
⊢ IsMultiplyPretransitive.{u_3, u_3} (LinearMap.GeneralLinearGroup K V) (ℙ K V) 2

Tactic:
exact IsPretransitive.of_embedding (f := f) Function.surjective_id

Premises used: MulAction.IsPretransitive.of_embedding, Function.surjective_id
-- 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
g : SpecialLinearGroup K V
D : ℙ K V
⊢ g • D = HSMul.hSMul (α := V ≃ₗ[K] V) ((toLinearEquiv : (a : SpecialLinearGroup K V) → V ≃ₗ[K] V) g : V ≃ₗ[K] V) D

Tactic:
rfl

Premises used: DistribSMul.toLinearMap, SMul.comp.smul, 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
⊢ IsMultiplyPretransitive.{u_2, u_2} (V ≃ₗ[K] V) (ℙ K V) 2

Tactic:
have := linearEquiv_is_two_pretransitive K V
-- 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 : IsMultiplyPretransitive.{u_2, u_2} (V ≃ₗ[K] V) (ℙ K V) 2
rw :
  ∀ (this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d) {a b c d : ℙ K V},
    a ≠ b → c ≠ d → ∃ (g : SpecialLinearGroup K V), g • a = c ∧ g • b = d
⊢ IsMultiplyPretransitive.{u_2, u_2} (SpecialLinearGroup K V) (ℙ K V) 2

Tactic:
rw [is_two_pretransitive_iff] at this ⊢

Premises used: MulAction.is_two_pretransitive_iff
-- 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'
obtain : ∀ (g : V ≃ₗ[K] V) (gD : g • D = E) (gE : g • D' = E'), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'

Tactic:
obtain ⟨g, gD, gE⟩ := this hD hE
-- 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'
pos : ∀ (hV : FiniteDimensional K V), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
neg : ∀ (hV : ¬FiniteDimensional K V), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'

Tactic:
by_cases hV : FiniteDimensional K V

Premises used: FiniteDimensional
-- 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 : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
obtain :
  ∀ (h : V ≃ₗ[K] V)
    (hdet :
      Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h : Kˣ)
        (((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) g)⁻¹ : Kˣ))
    (hD : h • D = D) (hE : h • D' = D'), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'

Tactic:
obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹

Premises used: LinearEquiv.det, Inv.inv, DFunLike.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_1 : D ≠ D'
hE_1 : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
h : V ≃ₗ[K] V
hdet :
  Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h : Kˣ)
    (((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) g)⁻¹ : Kˣ)
hD : h • D = D
hE : h • D' = D'
⊢ Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) (g * h) : Kˣ) (1 : Kˣ)

Tactic:
simp [hdet]
-- 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_1 : D ≠ D'
hE_1 : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
h : V ≃ₗ[K] V
hdet :
  Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h : Kˣ)
    (((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) g)⁻¹ : Kˣ)
hD : h • D = D
hE : h • D' = D'
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 * h) ⋯)
        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 * h) ⋯)
        D' =
      E'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'

Tactic:
use ⟨g * h, by simp [hdet]⟩
-- 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_1 : D ≠ D'
hE_1 : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
this : ∀ (a : Kˣ), ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
h : V ≃ₗ[K] V
hdet :
  Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h : Kˣ)
    (((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) g)⁻¹ : Kˣ)
hD : h • D = D
hE : h • D' = D'
⊢ 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 * h) ⋯)
        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 * h) ⋯)
        D' =
      E'

Tactic:
simp [specialLinearGroup_smul_def, toLinearEquiv_eq_coe, mul_smul, gD, hD, gE, hE]

Premises used: Projectivization.specialLinearGroup_smul_def, SpecialLinearGroup.toLinearEquiv_eq_coe, SemigroupAction.mul_smul
-- 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
pos : ∀ (a : Kˣ), ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'

Tactic:
suffices ∀ a : Kˣ, ∃ h : V ≃ₗ[K] V, h.det = a ∧ h • D = D ∧ h • D' = D' by
      obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹
      use ⟨g * h, by simp [hdet]⟩
      simp [specialLinearGroup_smul_def, toLinearEquiv_eq_coe, mul_smul, gD, hD, gE, hE]
-- 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
a : Kˣ
pos :
  ∀ (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ˣ),
    ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
⊢ ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'

Tactic:
rw [← linearIndependent_pair_iff_ne] at hD

Premises used: Projectivization.linearIndependent_pair_iff_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 : ∀ {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ˣ
⊢ LinearIndepOn (ι := V) K id {D.rep, D'.rep}

Tactic:
have := linearIndepOn_pair D D'
-- 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
pos :
  ∃ (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 ⋯
⊢ ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'

Tactic:
rw [← mk_rep D, ← mk_rep D']

Premises used: Projectivization.mk_rep
-- 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
⊢ Membership.mem (γ := Set V) {D.rep, D'.rep} D.rep

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
⊢ D.rep ∈ s

Tactic:
have hD_mem : D.rep ∈ s := LinearIndepOn.subset_extend _ _ (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
⊢ Membership.mem (γ := Set V) {D.rep, D'.rep} D'.rep

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
⊢ D'.rep ∈ s

Tactic:
have hD'_mem : D'.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)