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
g g' : G
x : ℙ K V
rw :
  (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯ ∘
        map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯)
      x =
    map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x)
hf :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := V) (β := V)
    (⇑((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g' : Module.End K V) : (a : V) → V)
hg :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := V) (β := V)
    (⇑((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g : Module.End K V) : (a : V) → V)
rw₁ :
  map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x) =
    map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x)
hf₁ :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := V) (β := V)
    (⇑((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g' : Module.End K V) : (a : V) → V)
hg₁ :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := V) (β := V)
    (⇑((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g : Module.End K V) : (a : V) → V)
rw₂ :
  map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x) =
    map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x)
hf₂ :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := V) (β := V)
    (⇑((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g' : Module.End K V) : (a : V) → V)
hg₂ :
  Function.Injective.{u_3 + 1, u_3 + 1} (α := V) (β := V)
    (⇑((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g : Module.End K V) : (a : V) → V)
⊢ map
      ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g ∘ₗ
        (DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g')
      ⋯ x =
    map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x)

Tactic:
rw [map_comp, Function.comp_apply]

Premises used: Function.Injective.comp, Projectivization.map_comp, Function.comp_apply
-- 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
x : ℙ K V
⊢ map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) 1) ⋯ x = x

Tactic:
simp [map_one, Module.End.one_eq_id]

Premises used: Module.End.one_eq_id, map_one
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
g : LinearMap.GeneralLinearGroup K V
x : ℙ K V
⊢ g • x = map (↑g.toLinearEquiv : V →ₗ[K] V) ⋯ x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
ι : Type u_4
F : Type u_5
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field F
g : Matrix.SpecialLinearGroup ι F
x : ℙ F (ι → F)
⊢ g • x =
    HSMul.hSMul (α := SpecialLinearGroup F (ι → F))
      ((Matrix.SpecialLinearGroup.toLin'_equiv : (a : Matrix.SpecialLinearGroup ι F) → SpecialLinearGroup F (ι → F)) g :
        SpecialLinearGroup F (ι → F))
      x

Tactic:
rfl
-- 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
g : G
v : V
hv : v ≠ 0
⊢ HSMul.hSMul (β := ℙ K V) g (mk K v hv) = mk K (g • v) ⋯

Tactic:
rfl

Premises used: Projectivization.mk, Quot.map, Quotient.map', Projectivization.map, rfl
-- 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
rw : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
⊢ IsMultiplyPretransitive.{u_3, u_3} (V ≃ₗ[K] V) (ℙ K V) 2

Tactic:
rw [is_two_pretransitive_iff]

Premises used: MulAction.is_two_pretransitive_iff
-- 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_1 D'_1 E E' : ℙ K V
hD_1 : D_1 ≠ D'_1
hE : E ≠ E'
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

Tactic:
simp
-- 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 : D ≠ D'
hE : E ≠ E'
⊢ ∀ {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

Tactic:
have qD {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]) :
    hD.linearCombinationEquiv (Finsupp.single 0 1) = D.rep := by simp
-- 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_1 D'_1 E E' : ℙ K V
hD_1 : D_1 ≠ D'_1
hE : E ≠ E'
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
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

Tactic:
simp
-- 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 : D ≠ D'
hE : E ≠ E'
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
⊢ ∀ {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

Tactic:
have qD' {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]) :
    hD.linearCombinationEquiv (Finsupp.single 1 1) = D'.rep := by simp
-- 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 : D ≠ D'
hE : E ≠ E'
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
⊢ LinearIndependent K ![D.rep, D'.rep]

Tactic:
rw [← linearIndependent_pair_iff_ne] at hD hE

Premises used: Projectivization.linearIndependent_pair_iff_ne
-- 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 : D ≠ D'
hE : E ≠ E'
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
hD₁ : LinearIndependent K ![D.rep, D'.rep]
⊢ LinearIndependent K ![E.rep, E'.rep]

Tactic:
rw [← linearIndependent_pair_iff_ne] at hD hE

Premises used: Projectivization.linearIndependent_pair_iff_ne
-- 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 : D ≠ D'
hE : E ≠ E'
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
hD₁ : LinearIndependent K ![D.rep, D'.rep]
hE₁ : LinearIndependent K ![E.rep, E'.rep]
⊢ ∀ {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

Tactic:
rw [← linearIndependent_pair_iff_ne] at hD hE

Premises used: Projectivization.linearIndependent_pair_iff_ne
-- 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 : D ≠ D'
hE : E ≠ E'
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
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
⊢ ∀ {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

Tactic:
rw [← linearIndependent_pair_iff_ne] at hD hE

Premises used: Projectivization.linearIndependent_pair_iff_ne
-- 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
⊢ FiniteDimensional.{u_2, u_3} K ↥(Submodule.span K (Set.range ![D.rep, D'.rep]))

Tactic:
have : FiniteDimensional K (Submodule.span K (Set.range ![D.rep, D'.rep])) :=
    span_of_finite K (Set.finite_range _)
-- 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]))
obtain :
  ∀ (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)),
    ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'

Tactic:
obtain ⟨g, hg⟩ := Submodule.exists_linearEquiv_restrict_eq f

Premises used: Submodule.exists_linearEquiv_restrict_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
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 : g • D = E ∧ g • D' = E'
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'

Tactic:
use g
-- 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 : g • D = E
h₁ : g • D' = E'
⊢ g • D = E ∧ g • D' = E'

Tactic:
constructor
-- 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 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)
⊢ 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