awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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 : ∃ (z : Kˣ), z • u = v
⊢ Eq (α := ℙ K V) (mk K u hu) (mk K v hv)

Tactic:
((mk_eq_mk_iff K v u hv hu).2 h).symm

Premises used: Iff.mpr, Projectivization.mk_eq_mk_iff, Eq.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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 : ∃ (z : Kˣ), z • u = v
⊢ Eq (α := ℙ K V) (mk K u hu) (mk K v hv)

Tactic:
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Premises used: Iff.mpr, Projectivization.mk_eq_mk_iff, Eq.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
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)
⊢ mk K u hu = v

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

Premises used: Projectivization.submodule_mk, Submodule.span_singleton_eq_span_singleton
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
h₁ : ∀ (u : V) (hu : u ≠ 0) (h : Projectivization.submodule (mk K u hu) = v.submodule), mk K u hu = v
⊢ u = 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

Premises used: Projectivization.submodule_mk, Submodule.span_singleton_eq_span_singleton
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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

Tactic:
⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩

Premises used: _private.0.Projectivization.equivSubmodule.match_1, Submodule, Projectivization.finrank_submodule, Membership.mem, Eq.rec, Subtype, Iff.intro, OfNat.ofNat, Equiv.refl, Eq, DFunLike.coe, Module.finrank
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
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
⊢ 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

Tactic:
refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
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
⊢ 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, _⟩

Premises used: finrank_eq_one_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
h₁ : Projectivization.submodule (mk K (↑v : V) ⋯) = H
⊢ Membership.mem (γ := Set (Submodule K V)) (Set.range Projectivization.submodule) H

Tactic:
use mk K (v : V) (Subtype.coe_injective.ne hv₀)

Premises used: Projectivization.mk, Function.Injective.ne, Subtype.coe_injective, Subtype.val
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
h₁ : (Set.range fun (x : K) ↦ x • (↑v : V)) = (↑H : Set V)
⊢ Projectivization.submodule (mk K (↑v : V) ⋯) = H

Tactic:
rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]

Premises used: Projectivization.submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)

Tactic:
(Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_

Premises used: Iff.mpr, HasSubset.Subset.antisymm, Set.range_subset_iff, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
h₁ : ∀ (x : V) (hx : x ∈ (↑H : Set V)), Membership.mem (γ := Set V) (Set.range fun (x : K) ↦ x • (↑v : V)) x
⊢ (Set.range fun (x : K) ↦ x • (↑v : V)) = (↑H : Set V)

Tactic:
refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_

Premises used: Iff.mpr, HasSubset.Subset.antisymm, Set.range_subset_iff, Submodule.smul_mem, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
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
⊢ Membership.mem (γ := Set V) (Set.range fun (x : K) ↦ x • (↑v : V)) x

Tactic:
rcases hv ⟨x, hx⟩ with ⟨c, hc⟩

Premises used: Subtype.mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
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:
⟨c, congr_arg Subtype.val hc⟩

Premises used: Set.Mem, setOf, congr_arg, Exists.intro, Set.range, Subtype.val
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
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:
exact ⟨c, congr_arg Subtype.val hc⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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 ↥H = 1
⊢ (mk'' H h).submodule = H

Tactic:
congr_arg Subtype.val <| (equivSubmodule K V).apply_symm_apply ⟨H, h⟩

Premises used: Equiv.apply_symm_apply, Quotient.liftOn', Subtype.mk, congr_arg, Projectivization.mk'', Projectivization.equivSubmodule, Subtype.val, Projectivization.submodule
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ℙ K V
⊢ mk'' v.submodule ⋯ = v

Tactic:
(equivSubmodule K V).symm_apply_apply v

Premises used: Quotient.liftOn', Equiv.symm_apply_apply, Projectivization.mk'', Projectivization.equivSubmodule, Projectivization.submodule
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
v : { v : V // v ≠ 0 }
c : Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) (↑v : V) : W) (0 : W)
⊢ Eq.{u_4 + 1} (α := W) ((f : (a : V) → W) (↑v : V) : W) ((f : (a : V) → W) 0 : W)

Tactic:
simp [c]
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
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)) ⋯ : { 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)
⊢ (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))

Tactic:
use Units.map σ.toMonoidHom a

Premises used: RingHom.toMonoidHom, DFunLike.coe, Units.map
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
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
⊢ 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)

Tactic:
dsimp at ha ⊢
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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 : a • v = u
⊢ 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:
simp [f.map_smulₛₗ, ← ha, Units.smul_def]

Premises used: Units.smul_def, LinearMap.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
v : V
hv : v ≠ 0
⊢ map f hf (mk K v hv) = mk L ((f : (a : V) → W) v) ⋯

Tactic:
rfl

Premises used: Projectivization.mk, Quotient.map', rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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)
h₁ : ∀ (h : ∃ (a : L), HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u), ∃ (a : K), a • v = u
⊢ Eq (α := ℙ K V) (mk K u hu) (mk K v hv)

Tactic:
simp only [map_mk, mk_eq_mk_iff'] at h ⊢

Premises used: Projectivization.mk_eq_mk_iff', Projectivization.map_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
h₁ : ∀ (a : L) (ha : HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W) = (f : (a : V) → W) u), ∃ (a : K), a • v = u
⊢ ∃ (a : K), a • v = u

Tactic:
rcases h with ⟨a, ha⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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

Tactic:
⟨τ a, hf ?_⟩

Premises used: Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
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)
⊢ ∃ (a : K), a • v = u

Tactic:
refine ⟨τ a, hf ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
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
h₁ h₂ h₃ h₄ : 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)

Tactic:
rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]

Premises used: RingHomInvPair.comp_apply_eq₂, LinearMap.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
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)
⊢ mk K u hu = v

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₂]

Premises used: RingHomInvPair.comp_apply_eq₂, LinearMap.map_smulₛₗ, Projectivization.mk_eq_mk_iff', Projectivization.map_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
h₁ : ∀ (u : V) (hu : u ≠ 0) (h : map f hf (mk K u hu) = map f hf v), mk K u hu = v
⊢ u = 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₂]

Premises used: RingHomInvPair.comp_apply_eq₂, LinearMap.map_smulₛₗ, Projectivization.mk_eq_mk_iff', Projectivization.map_mk
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h :
  ∀ (x : ℙ K V) (v : { v : V // v ≠ 0 }),
    Eq (α := ℙ K V)
      (map LinearMap.id ⋯ (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))
⊢ Eq (α := ℙ K V → ℙ K V) (map LinearMap.id ⋯) id

Tactic:
ext ⟨v⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : ℙ K V
v : { v : V // v ≠ 0 }
⊢ Eq (α := ℙ K V)
    (map LinearMap.id ⋯ (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:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
F : Type u_5
U : Type u_6
inst_6 : DivisionRing F
inst_7 : AddCommGroup U
inst_8 : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst_9 : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
g : W →ₛₗ[τ] U
hg : Function.Injective.{u_4 + 1, u_6 + 1} (α := W) (β := U) (⇑g : (a : W) → U)
hgf : Function.Injective.{u_2 + 1, u_6 + 1} (α := V) (β := U) (⇑(g ∘ₛₗ f) : (a : V) → U)
h :
  ∀ (x : ℙ K V) (v : { v : V // v ≠ 0 }),
    map (g ∘ₛₗ f) hgf (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop) v) =
      (map g hg ∘ map f hf) (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop) v)
⊢ map (g ∘ₛₗ f) hgf = map g hg ∘ map f hf

Tactic:
ext ⟨v⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
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
F : Type u_5
U : Type u_6
inst_6 : DivisionRing F
inst_7 : AddCommGroup U
inst_8 : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst_9 : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective.{u_2 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
g : W →ₛₗ[τ] U
hg : Function.Injective.{u_4 + 1, u_6 + 1} (α := W) (β := U) (⇑g : (a : W) → U)
hgf : Function.Injective.{u_2 + 1, u_6 + 1} (α := V) (β := U) (⇑(g ∘ₛₗ f) : (a : V) → U)
x : ℙ K V
v : { v : V // v ≠ 0 }
⊢ map (g ∘ₛₗ f) hgf (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop) v) =
    (map g hg ∘ map f hf) (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop) v)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
D D' : ℙ K V
rw : (∀ (a : K), a • D.rep ≠ D'.rep) ↔ D ≠ D'
⊢ LinearIndependent K ![D.rep, D'.rep] ↔ D ≠ D'

Tactic:
rw [LinearIndependent.pair_iff' (rep_nonzero _)]

Premises used: LinearIndependent.pair_iff', Projectivization.rep_nonzero
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
D D' : ℙ K V
h : ∀ (a : K), a • D.rep ≠ D'.rep
hD : D = D'
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) 1 D.rep = D'.rep

Tactic:
simp [hD]
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
D D' : ℙ K V
refine : ∀ (h : D ≠ D') (a : K) (hD : a • D.rep = D'.rep), D = D'
⊢ (∀ (a : K), a • D.rep ≠ D'.rep) ↔ D ≠ D'

Tactic:
refine ⟨fun h hD ↦ h 1 (by simp [hD]), fun h a hD ↦ h ?_⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
rw : ∃ (a : Kˣ), a • D.rep = D'.rep
⊢ D = D'

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

Premises used: Projectivization.mk_eq_mk_iff, eq_comm, Projectivization.mk_rep
-- Module: Mathlib.LinearAlgebra.Projectivization.Basic
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
this : a ≠ 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Kˣ) (IsUnit.unit (a := a) ⋯ : Kˣ) D.rep = D'.rep

Tactic:
simp [← hD]