awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ p = q ↔ p.range = q.range ∧ p.ker = q.ker
have refine : p.range = q.range ∧ p.ker = q.ker → ∀ (hr : p.range = q.range) (hk : p.ker = q.ker), p = q
Tactic: refine ⟨fun h => ⟨congrArg range h, congrArg ker h⟩, fun ⟨hr, hk⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
⊢ p = q
have h : ∀ (x : E), Eq (α := E) ((p : (a : E) → E) x : E) ((q : (a : E) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
x : E
⊢ Eq (α := E) ((p : (a : E) → E) x : E) ((q : (a : E) → E) x : E)
have h : ∀ (v : E) (hv : v ∈ p.ker) (w : E) (hw : w ∈ p.range),
  (∀ (r : ↥p.ker) (s : ↥p.range),
      (↑r : E) + (↑s : E) =
          (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
            (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E) →
        r = Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv ∧ s = Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) →
    Eq (α := E)
      ((p : (a : E) → E)
          ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
            (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E)) :
        E)
      ((q : (a : E) → E)
          ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
            (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E)) :
        E)
Tactic: obtain ⟨⟨v, hv⟩, ⟨w, hw⟩, rfl, _⟩ :=
    (ker p).existsUnique_add_of_isCompl hp.isCompl.symm x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
R : Type u_1
inst : CommRing R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    ((LinearEquiv.conj.{u_1, u_1, u_2, u_2} (R₁' := R) (R₂' := R) (M₁' := ↥p × ↥f.ker) (M₂' := E) (σ₁'₂' :=
            RingHom.id R) (σ₂'₁' := RingHom.id R) (p.prodEquivOfIsCompl f.ker ⋯) :
          Module.End R (↥p × ↥f.ker) ≃ₗ[R] Module.End R E) :
        (a : Module.End R (↥p × ↥f.ker)) → Module.End R E)
      (prodMap id 0)
have rw : f =
  ((↑(p.prodEquivOfIsCompl f.ker sorry) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ
    (↑(p.prodEquivOfIsCompl f.ker sorry).symm : E →ₗ[R] ↥p × ↥f.ker)
Tactic: rw [LinearEquiv.conj_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f
have rw : f.range ∈ Module.End.invtSubmodule T ↔ (T ∘ₗ f).range ≤ f.range
Tactic: rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.range ∈ Module.End.invtSubmodule T ↔ (T ∘ₗ f).range ≤ f.range
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f
have rw₁ : f.range ∈ Module.End.invtSubmodule T ↔ map T f.range ≤ f.range
Tactic: rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.range ∈ Module.End.invtSubmodule T ↔ (T ∘ₗ f).range ≤ f.range
rw₁ : f.range ∈ Module.End.invtSubmodule T ↔ map T f.range ≤ f.range
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f
have rw₂ : map T f.range ≤ f.range ↔ map T f.range ≤ f.range
Tactic: rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T
have rw : f.ker ∈ Module.End.invtSubmodule T ↔ (f ∘ₗ T) ∘ₗ f = f ∘ₗ T
Tactic: rw [← comp_assoc, hf.comp_eq_left_iff, ker_comp, Module.End.mem_invtSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.ker ∈ Module.End.invtSubmodule T ↔ (f ∘ₗ T) ∘ₗ f = f ∘ₗ T
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T
have rw₁ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ (f ∘ₗ T).ker
Tactic: rw [← comp_assoc, hf.comp_eq_left_iff, ker_comp, Module.End.mem_invtSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.ker ∈ Module.End.invtSubmodule T ↔ (f ∘ₗ T) ∘ₗ f = f ∘ₗ T
rw₁ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ (f ∘ₗ T).ker
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T
have rw₂ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ comap T f.ker
Tactic: rw [← comp_assoc, hf.comp_eq_left_iff, ker_comp, Module.End.mem_invtSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.ker ∈ Module.End.invtSubmodule T ↔ (f ∘ₗ T) ∘ₗ f = f ∘ₗ T
rw₁ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ (f ∘ₗ T).ker
rw₂ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ comap T f.ker
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T
have rw₃ : f.ker ≤ comap T f.ker ↔ f.ker ≤ comap T f.ker
Tactic: rw [← comp_assoc, hf.comp_eq_left_iff, ker_comp, Module.End.mem_invtSubmodule]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T
have simp_rw : Commute f T ↔ f * (T * f) = T * f ∧ f * (T * f) = f * T
Tactic: simp_rw [hf.range_mem_invtSubmodule_iff, hf.ker_mem_invtSubmodule_iff, ← Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hT : IsUnit T
hf : IsIdempotentElem f
⊢ Commute f T ↔ map T f.range = f.range ∧ map T f.ker = f.ker
have lift : ∀ (T : (E →ₗ[R] E)ˣ),
  Commute f (↑T : E →ₗ[R] E) ↔ map (↑T : E →ₗ[R] E) f.range = f.range ∧ map (↑T : E →ₗ[R] E) f.ker = f.ker
Tactic: lift T to GeneralLinearGroup R E using hT
Cleared hypotheses: T, hT
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f (↑T : E →ₗ[R] E) ↔ map (↑T : E →ₗ[R] E) f.range = f.range ∧ map (↑T : E →ₗ[R] E) f.ker = f.ker
have simp_rw : Commute f (↑T : E →ₗ[R] E) →
  Commute f
    (↑(LinearEquiv.symm ((GeneralLinearGroup.generalLinearEquiv R E : (a : GeneralLinearGroup R E) → E ≃ₗ[R] E) T)) :
      E →ₗ[R] E)
Tactic: simp_rw [← GeneralLinearGroup.generalLinearEquiv_to_linearMap, le_antisymm_iff,
    ← Module.End.mem_invtSubmodule_iff_map_le, ← Module.End.mem_invtSubmodule_symm_iff_le_map,
    and_and_and_comm (c := (ker f ∈ _)), ← hf.commute_iff,
    GeneralLinearGroup.generalLinearEquiv_to_linearMap, iff_self_and]
-- 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
g g' : G
x : ℙ K V
⊢ map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) (g * 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)
have simp_rw : map
    ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g ∘ₗ
      (DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g')
    sorry x =
  map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) sorry
    (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') sorry x)
Tactic: simp_rw [map_mul, Module.End.mul_eq_comp]
-- 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
g g' : G
x : ℙ K 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)
have rw : (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) sorry ∘
      map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') sorry)
    x =
  map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) sorry
    (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') sorry x)
Tactic: rw [map_comp, Function.comp_apply]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_comp, Function.comp_apply]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_comp, Function.comp_apply]
-- 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
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)
⊢ 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)
have rw₁ : map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) sorry
    (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') sorry x) =
  map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) sorry
    (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') sorry x)
Tactic: rw [map_comp, Function.comp_apply]
-- 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
⊢ IsMultiplyPretransitive.{u_3, u_3} (V ≃ₗ[K] V) (ℙ K V) 2
have rw : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ (g : V ≃ₗ[K] V), g • a = c ∧ g • b = d
Tactic: rw [is_two_pretransitive_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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'
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
have 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
Tactic: have qD {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]) :
    hD.linearCombinationEquiv (Finsupp.single 0 1) = D.rep := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
have 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
Tactic: have qD' {D D' : ℙ K V} (hD : LinearIndependent K ![D.rep, D'.rep]) :
    hD.linearCombinationEquiv (Finsupp.single 1 1) = D'.rep := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
have hD₁ : LinearIndependent K ![D.rep, D'.rep]
Tactic: rw [← linearIndependent_pair_iff_ne] at hD hE
Cleared hypotheses: hD, hE, qD, qD'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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]
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
have hE₁ : LinearIndependent K ![E.rep, E'.rep]
Tactic: rw [← linearIndependent_pair_iff_ne] at hD hE
Cleared hypotheses: hD, hE, qD, qD'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Action (hypothesis)
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
⊢ ∃ (g : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
have this : 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 _)
-- 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), g • D = E ∧ g • D' = E'
have 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'
Tactic: obtain ⟨g, hg⟩ := Submodule.exists_linearEquiv_restrict_eq f
-- 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 : V ≃ₗ[K] V), g • D = E ∧ g • D' = E'
have h : g • D = E ∧ g • D' = E'
Tactic: use g