awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ g • D = E ∧ g • D' = E'
have h : g • D = E
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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 • D' = E'
have h₁ : g • D' = E'
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ g • D = E
have h : ∃ (a : Kˣ), a • E.rep = g • D.rep
Tactic: rw [← mk_rep D, ← mk_rep E, smul_mk, mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ ∃ (a : Kˣ), a • E.rep = g • D.rep
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := Kˣ) 1 E.rep = g • D.rep
Tactic: use 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Kˣ) 1 E.rep = g • D.rep
have 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)
Tactic: simp only [one_smul, LinearEquiv.smul_def, ← qD hD, ← hg, ← qD hE]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ g • D' = E'
have h : ∃ (a : Kˣ), a • E'.rep = g • D'.rep
Tactic: rw [← mk_rep D', ← mk_rep E', smul_mk, mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ ∃ (a : Kˣ), a • E'.rep = g • D'.rep
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := Kˣ) 1 E'.rep = g • D'.rep
Tactic: use 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := Kˣ) 1 E'.rep = g • D'.rep
have 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)
Tactic: simp only [one_smul, LinearEquiv.smul_def, ← qD' hD, ← hg, ← qD' hE]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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
⊢ id (e • D) = LinearMap.GeneralLinearGroup.ofLinearEquiv e • id D
have simp : e • D = LinearMap.GeneralLinearGroup.ofLinearEquiv e • D
Tactic: simp only [id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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
⊢ e • D = LinearMap.GeneralLinearGroup.ofLinearEquiv e • D
have rw : Eq (α := ℙ K V) (mk K (e • D.rep) sorry) (mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) sorry)
Tactic: rw [← mk_rep D, smul_mk, smul_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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} (SpecialLinearGroup K V) (ℙ K V) 2
have this : IsMultiplyPretransitive.{u_2, u_2} (V ≃ₗ[K] V) (ℙ K V) 2
Tactic: have := linearEquiv_is_two_pretransitive K V
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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
⊢ IsMultiplyPretransitive.{u_2, u_2} (SpecialLinearGroup K V) (ℙ K V) 2
have 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
Tactic: rw [is_two_pretransitive_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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 : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
have obtain : ∀ (g : V ≃ₗ[K] V) (gD : g • D = E) (gE : g • D' = E'), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
Tactic: obtain ⟨g, gD, gE⟩ := this hD hE
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
have pos : ∀ (hV : FiniteDimensional K V), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
Tactic: by_cases hV : FiniteDimensional K V
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
have neg : ∀ (hV : ¬FiniteDimensional K V), ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
Tactic: by_cases hV : FiniteDimensional K V
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
have 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'
Tactic: obtain ⟨h, hdet, hD, hE⟩ := this (g.det)⁻¹
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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'
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
have 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) sorry)
      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) sorry)
      D' =
    E'
Tactic: use ⟨g * h, by simp [hdet]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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
⊢ ∃ (g : SpecialLinearGroup K V), g • D = E ∧ g • D' = E'
have pos : ∀ (a : Kˣ), ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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ˣ
⊢ ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
have 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'
Tactic: rw [← linearIndependent_pair_iff_ne] at hD
Cleared hypotheses: hD, hE, g, gD, gE, hV, a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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ˣ
⊢ ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
have this₁ : LinearIndepOn (ι := V) K id {D.rep, D'.rep}
Tactic: have := linearIndepOn_pair D D'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (goal)
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
⊢ ∃ (h : V ≃ₗ[K] V), (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧ h • D = D ∧ h • D' = D'
have pos : ∃ (h : V ≃ₗ[K] V),
  (LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) h = a ∧
    HSMul.hSMul (β := ℙ K V) h (mk K D.rep sorry) = mk K D.rep sorry ∧
      HSMul.hSMul (β := ℙ K V) h (mk K D'.rep sorry) = mk K D'.rep sorry
Tactic: rw [← mk_rep D, ← mk_rep D']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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
⊢ ∃ (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 ⋯
have hD_mem : D.rep ∈ s
Tactic: have hD_mem : D.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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
⊢ ∃ (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 ⋯
have hD'_mem : D'.rep ∈ s
Tactic: have hD'_mem : D'.rep ∈ s := LinearIndepOn.subset_extend _ _ (by simp)