awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ Eq.{u_1 + 1} (α := K)
    ((((b.repr : (a : V) → (↑s : Type u_2) →₀ K) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) : V) :
            Finsupp.{u_2, u_1} (↑s : Type u_2) K) :
          (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)
have h : Eq.{u_1 + 1} (α := K)
  ((Finsupp.single (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) 1 : (a : (↑s : Type u_2)) → K)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
    K)
  (0 : K)
Tactic: rw [← Module.Basis.extend_apply_self, Module.Basis.repr_self]
-- 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
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ Eq.{u_1 + 1} (α := K)
    ((Finsupp.single (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem) 1 : (a : (↑s : Type u_2)) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem) :
      K)
    (0 : K)
have h : Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem
Tactic: apply Finsupp.single_eq_of_ne
-- 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
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ s) D.rep hD_mem ≠ Subtype.mk (p := fun (x : V) ↦ x ∈ s) D'.rep hD'_mem
have h : ¬D.rep = D'.rep
Tactic: simp only [ne_eq, ← Subtype.coe_inj]
-- 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
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : D.rep = D'.rep
⊢ False
have h₁ : Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 2)) 0 1
Tactic: apply Fin.zero_ne_one
-- 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
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
h : D.rep = D'.rep
h₁ : Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 2)) 0 1
⊢ False
have h₂ : ℕ
Tactic: apply Fin.zero_ne_one
-- 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
⊢ Eq.{u_1 + 1} (α := Kˣ) ((LinearEquiv.det : (a : V ≃ₗ[K] V) → Kˣ) g : Kˣ) (1 : Kˣ)
have rw : Eq.{u_1 + 1} (α := K) ((LinearMap.det : (a : V →ₗ[K] V) → K) (↑g : V →ₗ[K] V) : K) ((↑1 : K) : K)
Tactic: rw [← Units.val_inj, coe_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 : ∀ {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 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 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 sorry)
      D' =
    E'
Tactic: use ⟨g, by
    rw [← Units.val_inj, coe_det]
    apply LinearMap.det_eq_one_of_not_module_finite hV⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ Eq (α := ℙ K V) (mk K v hv) (mk K w hw) ↔ ∃ (a : K), a • w = v
have rw : (∃ (a : Kˣ), a • w = v) ↔ ∃ (a : K), a • w = v
Tactic: rw [mk_eq_mk_iff K v w hv hw]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ (a : Kˣ), a • w = v) ↔ ∃ (a : K), a • w = v
have mp : (∃ (a : Kˣ), a • w = v) → ∃ (a : K), a • w = v
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
mp : (∃ (a : Kˣ), a • w = v) → ∃ (a : K), a • w = v
⊢ (∃ (a : Kˣ), a • w = v) ↔ ∃ (a : K), a • w = v
have mpr : (∃ (a : K), a • w = v) → ∃ (a : Kˣ), a • w = v
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ (a : Kˣ), a • w = v
have mpr : ∀ (c : a = 0), 0 = v
Tactic: refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v
have mpr : ∀ (ha : HSMul.hSMul.{u_1, u_2, u_2} (α := K) 0 w = v) (c : a = 0), 0 = v
Tactic: rwa [c, zero_smul] at ha
Cleared hypotheses: ha, c
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
mpr : ∀ (ha : HSMul.hSMul.{u_1, u_2, u_2} (α := K) 0 w = v) (c : a = 0), 0 = v
⊢ 0 = v
have mpr₁ : ∀ (ha : 0 = v) (c : a = 0), 0 = v
Tactic: rwa [c, zero_smul] at ha
Cleared hypotheses: ha, c
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
| v.submodule
have rw : Projectivization.submodule (mk K v.rep sorry)
Tactic: rw [← v.mk_rep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ v.submodule = K ∙ v.rep
have conv_lhs : Eq (α := Submodule K V) (Projectivization.submodule (mk K v.rep sorry)) (K ∙ v.rep)
Tactic: conv_lhs => rw [← v.mk_rep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ finrank.{u_1, u_2} K ↥v.submodule = 1
have rw : finrank.{u_1, u_2} K ↥(K ∙ v.rep) = 1
Tactic: rw [submodule_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ FiniteDimensional.{u_1, u_2} K ↥v.submodule
have rw : FiniteDimensional.{u_1, u_2} K ↥(Projectivization.submodule (mk K v.rep sorry))
Tactic: rw [← v.mk_rep]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ FiniteDimensional.{u_1, u_2} K ↥(Projectivization.submodule (mk K v.rep ⋯))
have change : FiniteDimensional.{u_1, u_2} K ↥(K ∙ v.rep)
Tactic: change FiniteDimensional K (K ∙ v.rep)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : Eq (α := Submodule K V) (Projectivization.submodule (mk K u hu)) (Projectivization.submodule (mk K v hv))
⊢ Eq (α := ℙ K V) (mk K u hu) (mk K v hv)
have h₁ : ∃ (z : Kˣ), z • u = v
Tactic: rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
u : V
hu : u ≠ 0
h : Projectivization.submodule (mk K u hu) = v.submodule
⊢ mk K u hu = v
have h₁ : ∀ (v : V) (hv : v ≠ 0)
  (h : Eq (α := Submodule K V) (Projectivization.submodule (mk K u hu)) (Projectivization.submodule (mk K v hv))),
  Eq (α := ℙ K V) (mk K u hu) (mk K v hv)
Tactic: induction v using ind with | h v hv =>
  rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
  exact ((mk_eq_mk_iff K v u hv hu).2 h).symm
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
u v : ℙ K V
h : u.submodule = v.submodule
⊢ u = v
have h₁ : ∀ (u : V) (hu : u ≠ 0) (h : Projectivization.submodule (mk K u hu) = v.submodule), mk K u hu = v
Tactic: induction u using ind with | h u hu =>
  induction v using ind with | h v hv =>
  rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
  exact ((mk_eq_mk_iff K v u hv hu).2 h).symm
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
H : Submodule K V
⊢ Membership.mem (γ := Set (Submodule K V)) (Set.range Projectivization.submodule) H ↔
    finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1
have refine : ∀
  (h :
    finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1),
  Membership.mem (γ := Set (Submodule K V)) (Set.range Projectivization.submodule) H
Tactic: refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
H : Submodule K V
h : finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1
⊢ Membership.mem (γ := Set (Submodule K V)) (Set.range Projectivization.submodule) H
have rcases : ∀ (v : ↥H) (hv₀ : v ≠ 0) (hv : ∀ (w : ↥H), ∃ (c : K), c • v = w),
  Membership.mem (γ := Set (Submodule K V)) (Set.range Projectivization.submodule) H
Tactic: rcases finrank_eq_one_iff'.1 h with ⟨v : H, hv₀, hv : ∀ w : H, _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
H : Submodule K V
h : finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ (c : K), c • v = w
⊢ Membership.mem (γ := Set (Submodule K V)) (Set.range Projectivization.submodule) H
have h₁ : Projectivization.submodule (mk K (↑v : V) sorry) = H
Tactic: use mk K (v : V) (Subtype.coe_injective.ne hv₀)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
H : Submodule K V
h : finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ (c : K), c • v = w
⊢ Projectivization.submodule (mk K (↑v : V) ⋯) = H
have h₁ : (Set.range fun (x : K) ↦ x • (↑v : V)) = (↑H : Set V)
Tactic: rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
H : Submodule K V
h : finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ (c : K), c • v = w
⊢ (Set.range fun (x : K) ↦ x • (↑v : V)) = (↑H : Set V)
have h₁ : ∀ (x : V) (hx : x ∈ (↑H : Set V)), Membership.mem (γ := Set V) (Set.range fun (x : K) ↦ x • (↑v : V)) x
Tactic: refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
H : Submodule K V
h : finrank.{u_1, u_2} K ↥((Equiv.refl (Submodule K V) : (a : Submodule K V) → Submodule K V) H : Submodule K V) = 1
v : ↥H
hv₀ : v ≠ 0
hv : ∀ (w : ↥H), ∃ (c : K), c • v = w
x : V
hx : x ∈ (↑H : Set V)
⊢ Membership.mem (γ := Set V) (Set.range fun (x : K) ↦ x • (↑v : V)) x
have h₁ : ∀ (c : K) (hc : c • v = Subtype.mk (p := fun (x : V) ↦ x ∈ H) x hx),
  Membership.mem (γ := Set V) (Set.range fun (x : K) ↦ x • (↑v : V)) x
Tactic: rcases hv ⟨x, hx⟩ with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha :
  (fun (m : Kˣ) ↦ m • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v hv) : V)) a =
    (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) u hu) : V)
⊢ (projectivizationSetoid L W : { v : W // v ≠ 0 } → { v : W // v ≠ 0 } → Prop)
    ((fun (v : { v : V // v ≠ 0 }) ↦
        (Subtype.mk (p := fun (v : W) ↦ v ≠ 0) ((f : (a : V) → W) (↑v : V)) ⋯ : { v : W // v ≠ 0 }))
      (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) u hu))
    ((fun (v : { v : V // v ≠ 0 }) ↦
        (Subtype.mk (p := fun (v : W) ↦ v ≠ 0) ((f : (a : V) → W) (↑v : V)) ⋯ : { v : W // v ≠ 0 }))
      (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v hv))
have h : Eq.{u_4 + 1} (α := W)
  ((fun (m : Lˣ) ↦
      HSMul.hSMul (β := W) m
        (↑((fun (v : { v : V // v ≠ 0 }) ↦
                (Subtype.mk (p := fun (v : W) ↦ v ≠ 0) ((f : (a : V) → W) (↑v : V)) sorry : { v : W // v ≠ 0 }))
              (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v hv)) :
          W))
    ((Units.map (↑σ : K →* L) : (a : Kˣ) → Lˣ) a))
  (↑((fun (v : { v : V // v ≠ 0 }) ↦
          (Subtype.mk (p := fun (v : W) ↦ v ≠ 0) ((f : (a : V) → W) (↑v : V)) sorry : { v : W // v ≠ 0 }))
        (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) u hu)) :
    W)
Tactic: use Units.map σ.toMonoidHom a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha :
  (fun (m : Kˣ) ↦ m • (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v hv) : V)) a =
    (↑(Subtype.mk (p := fun (v : V) ↦ v ≠ 0) u hu) : V)
⊢ Eq.{u_4 + 1} (α := W)
    ((fun (m : Lˣ) ↦
        HSMul.hSMul (β := W) m
          (↑((fun (v : { v : V // v ≠ 0 }) ↦
                  (Subtype.mk (p := fun (v : W) ↦ v ≠ 0) ((f : (a : V) → W) (↑v : V)) ⋯ : { v : W // v ≠ 0 }))
                (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v hv)) :
            W))
      ((Units.map (↑σ : K →* L) : (a : Kˣ) → Lˣ) a))
    (↑((fun (v : { v : V // v ≠ 0 }) ↦
            (Subtype.mk (p := fun (v : W) ↦ v ≠ 0) ((f : (a : V) → W) (↑v : V)) ⋯ : { v : W // v ≠ 0 }))
          (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) u hu)) :
      W)
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := Lˣ) (β := W)
    (((Units.map (↑σ : K →* L) : MonoidHom.{u_1, u_3} Kˣ Lˣ) : (a : Kˣ) → Lˣ) a : Lˣ) ((f : (a : V) → W) v : W) =
  (f : (a : V) → W) u
Tactic: dsimp at ha ⊢
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
τ : L →+* K
inst_6 : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : map f hf (mk K u hu) = map f hf (mk K v hv)
⊢ Eq (α := ℙ K V) (mk K u hu) (mk K v hv)
have h₁ : ∀ (h : ∃ (a : L), HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u), ∃ (a : K), a • v = u
Tactic: simp only [map_mk, mk_eq_mk_iff'] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
τ : L →+* K
inst_6 : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : ∃ (a : L), HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u
⊢ ∃ (a : K), a • v = u
have h₁ : ∀ (a : L) (ha : HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u), ∃ (a : K), a • v = u
Tactic: rcases h with ⟨a, ha⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
τ : L →+* K
inst_6 : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : L
ha : HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u
⊢ ∃ (a : K), a • v = u
have h : Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) (HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((τ : (a : L) → K) a : K) v) : W)
  ((f : (a : V) → W) u : W)
Tactic: refine ⟨τ a, hf ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
τ : L →+* K
inst_6 : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : L
ha : HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u
⊢ Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) (HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((τ : (a : L) → K) a : K) v) : W)
    ((f : (a : V) → W) u : W)
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := L) (β := W) ((σ : (a : K) → L) ((τ : (a : L) → K) a : K) : L)
    ((f : (a : V) → W) v : W) =
  (f : (a : V) → W) u
Tactic: rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
τ : L →+* K
inst_6 : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
v : ℙ K V
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v
have h₁ : ∀ (v : V) (hv : v ≠ 0) (h : map f hf (mk K u hu) = map f hf (mk K v hv)), Eq (α := ℙ K V) (mk K u hu) (mk K v hv)
Tactic: induction v using ind with | h v hv =>
  simp only [map_mk, mk_eq_mk_iff'] at h ⊢
  rcases h with ⟨a, ha⟩
  refine ⟨τ a, hf ?_⟩
  rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
L : Type u_3
W : Type u_4
inst_3 : DivisionRing L
inst_4 : AddCommGroup W
inst_5 : Module L W
σ : K →+* L
τ : L →+* K
inst_6 : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
u v : ℙ K V
h : map f hf u = map f hf v
⊢ u = v
have h₁ : ∀ (u : V) (hu : u ≠ 0) (h : map f hf (mk K u hu) = map f hf v), mk K u hu = v
Tactic: induction u using ind with | h u hu => induction v using ind with | h v hv =>
  simp only [map_mk, mk_eq_mk_iff'] at h ⊢
  rcases h with ⟨a, ha⟩
  refine ⟨τ a, hf ?_⟩
  rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq (α := ℙ K V → ℙ K V) (map LinearMap.id ⋯) id
have h : ∀ (x : ℙ K V) (v : { v : V // v ≠ 0 }),
  Eq (α := ℙ K V)
    (map LinearMap.id sorry (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop) v))
    (id (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop) v))
Tactic: ext ⟨v⟩