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
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
this : a ≠ 0
⊢ ∃ (a : Kˣ), a • D.rep = D'.rep

Tactic:
refine ⟨(Ne.isUnit this).unit, by 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
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
suffices : a ≠ 0
⊢ ∃ (a : Kˣ), a • D.rep = D'.rep

Tactic:
suffices a ≠ 0 by refine ⟨(Ne.isUnit this).unit, by 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
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
ha : a = 0
⊢ D'.rep = 0

Tactic:
simp [← hD, 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
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
⊢ a ≠ 0

Tactic:
exact fun ha ↦ D'.rep_nonzero (by simp [← hD, ha])

Premises used: 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
pos : ∀ (h : D = D'), LinearIndepOn (ι := V) K id {D.rep, D'.rep}
neg : ∀ (h : ¬D = D'), LinearIndepOn (ι := V) K id {D.rep, D'.rep}
⊢ LinearIndepOn (ι := V) K id {D.rep, D'.rep}

Tactic:
by_cases h : D = D'
-- 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'
⊢ LinearIndepOn (ι := V) K id {D.rep, D'.rep}

Tactic:
simpa [h] using D'.rep_nonzero

Premises used: 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 : ¬D = D'
neg : ∀ (h : LinearIndepOn K id (Set.range ![D'.rep, D.rep])), LinearIndepOn (ι := V) K id {D.rep, D'.rep}
neg₁ : ∀ (h : LinearIndependent K ![D'.rep, D.rep]), Function.Injective ![D'.rep, D.rep]
⊢ LinearIndepOn (ι := V) K id {D.rep, D'.rep}

Tactic:
rw [← ne_eq, ← linearIndependent_pair_iff_ne, LinearIndependent.pair_symm_iff,
    ← linearIndepOn_id_range_iff] at h

Premises used: linearIndepOn_id_range_iff, ne_eq, LinearIndependent.pair_symm_iff, Projectivization.linearIndependent_pair_iff_ne
-- 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 : LinearIndepOn K id (Set.range ![D'.rep, D.rep])
⊢ LinearIndepOn (ι := V) K id {D.rep, D'.rep}

Tactic:
simpa using 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 : LinearIndependent K ![D'.rep, D.rep]
⊢ Function.Injective ![D'.rep, D.rep]

Tactic:
simpa [injective_pair_iff_ne, injective_pair_iff_ne, ne_eq] using h.injective

Premises used: injective_pair_iff_ne, LinearIndependent.injective, ne_eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
b : { v : V // v ≠ 0 }
rw : Eq.{u_1 + 1} (α := Subgroup kˣ) (MulAction.stabilizer kˣ (↑b : V)) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := Subgroup kˣ) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup kˣ) (MulAction.stabilizer kˣ b) ⊥

Tactic:
rw [(Units.nonZeroSubMul k V).stabilizer_of_subMul,
      Module.stabilizer_units_eq_bot_of_ne_zero k b.property]

Premises used: SubMulAction.stabilizer_of_subMul, Module.stabilizer_units_eq_bot_of_ne_zero, Subtype.property
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Subsingleton V
⊢ IsEmpty.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }

Tactic:
have : IsEmpty { v : V // v ≠ 0 } := ⟨fun v ↦ v.2 (Subsingleton.elim v.1 0)⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Subsingleton V
this : IsEmpty.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }
⊢ IsEmpty.{u_2 + 1} (ℙ k V)

Tactic:
simpa using (nonZeroEquivProjectivizationProdUnits k V).symm.isEmpty

Premises used: Equiv.isEmpty, Projectivization.nonZeroEquivProjectivizationProdUnits, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite V
⊢ Finite.{u_2 + 1} (ℙ k V)

Tactic:
have : Finite (ℙ k V × kˣ) := Finite.of_equiv _ (nonZeroEquivProjectivizationProdUnits k V)
  Finite.prod_left kˣ

Premises used: Finite.of_equiv, Units, Subtype, Ne, Projectivization.nonZeroEquivProjectivizationProdUnits, OfNat.ofNat, Finite.prod_left
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
⊢ Finite.{u_2 + 1} (ℙ k V) ↔ Finite V

Tactic:
⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
refine : ∀ (h : Finite.{u_2 + 1} (ℙ k V)), Finite V
⊢ Finite.{u_2 + 1} (ℙ k V) ↔ Finite V

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
h : Finite.{u_2 + 1} (ℙ k V)
e : { v : V // v ≠ 0 } ≃ Prod.{u_2, u_1} (ℙ k V) kˣ := nonZeroEquivProjectivizationProdUnits k V
⊢ Finite.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }

Tactic:
have : Finite { v : V // v ≠ 0 } := Finite.of_equiv _ e.symm
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
h : Finite.{u_2 + 1} (ℙ k V)
e : { v : V // v ≠ 0 } ≃ Prod.{u_2, u_1} (ℙ k V) kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }
x : { v : V // v ≠ 0 } ⊕ Unit
⊢ (fun (v : V) ↦
        (if h : v = 0 then Sum.inr () else Sum.inl (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v h) :
          { v : V // v ≠ 0 } ⊕ Unit))
      (Sum.elim (Subtype.val (p := fun (v : V) ↦ v ≠ 0)) (fun (x : Unit) ↦ 0) x) =
    x

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
h : Finite.{u_2 + 1} (ℙ k V)
e : { v : V // v ≠ 0 } ≃ Prod.{u_2, u_1} (ℙ k V) kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }
x : V
⊢ Sum.elim (α := { v : V // v ≠ 0 }) (Subtype.val (p := fun (v : V) ↦ v ≠ 0)) (fun (x : Unit) ↦ 0)
      ((fun (v : V) ↦
          (if h : v = 0 then Sum.inr () else Sum.inl (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v h) :
            { v : V // v ≠ 0 } ⊕ Unit))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
h : Finite.{u_2 + 1} (ℙ k V)
e : { v : V // v ≠ 0 } ≃ Prod.{u_2, u_1} (ℙ k V) kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }
eq : { v : V // v ≠ 0 } ⊕ Unit ≃ V :=
  { toFun := Sum.elim (Subtype.val (p := fun (v : V) ↦ v ≠ 0)) fun (x : Unit) ↦ 0,
    invFun := fun (v : V) ↦ if h : v = 0 then Sum.inr () else Sum.inl (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v h),
    left_inv := ⋯, right_inv := ⋯ }
⊢ Finite V

Tactic:
Finite.of_equiv _ eq

Premises used: Finite.of_equiv
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
h : Finite.{u_2 + 1} (ℙ k V)
e : { v : V // v ≠ 0 } ≃ Prod.{u_2, u_1} (ℙ k V) kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }
eq : { v : V // v ≠ 0 } ⊕ Unit ≃ V :=
  { toFun := Sum.elim (Subtype.val (p := fun (v : V) ↦ v ≠ 0)) fun (x : Unit) ↦ 0,
    invFun := fun (v : V) ↦ if h : v = 0 then Sum.inr () else Sum.inl (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) v h),
    left_inv := ⋯, right_inv := ⋯ }
⊢ Finite V

Tactic:
exact Finite.of_equiv _ eq

Premises used: Finite.of_equiv
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
refine : ∀ (h : Finite.{u_2 + 1} (ℙ k V)), Finite V
refine₁ : ∀ (h : Finite.{u_2 + 1} (ℙ k V)), Finite V
refine₂ refine₃ : ∀ (h : Finite.{u_2 + 1} (ℙ k V)) (this : Finite.{max 1 (u_2 + 1)} { v : V // v ≠ 0 }), Finite V
⊢ Finite.{u_2 + 1} (ℙ k V) ↔ Finite V

Tactic:
classical
  refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  let e := nonZeroEquivProjectivizationProdUnits k V
  have : Finite { v : V // v ≠ 0 } := Finite.of_equiv _ e.symm
  let eq : { v : V // v ≠ 0 } ⊕ Unit ≃ V :=
    ⟨(Sum.elim Subtype.val (fun _ ↦ 0)), fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩,
      by intro x; aesop, by intro x; aesop⟩
  exact Finite.of_equiv _ eq
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
⊢ Nontrivial V

Tactic:
nontriviality V
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h : Infinite k
⊢ Infinite V

Tactic:
have : Infinite V := Module.Free.infinite k V
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h : Infinite k
this : Infinite V
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Infinite V
⊢ ¬Finite.{u_2 + 1} (ℙ k V) ↔ ¬Finite V

Tactic:
have := not_iff_not.mpr (finite_iff_of_finite k V)
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Infinite V
this : ¬Finite.{u_2 + 1} (ℙ k V) ↔ ¬Finite V
⊢ Infinite.{u_2 + 1} (ℙ k V) ↔ Infinite V

Tactic:
push Not at this

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Infinite V
this : Infinite.{u_2 + 1} (ℙ k V) ↔ Infinite V
rwa rwa₁ rwa₂ rwa₃ : Infinite V
⊢ Infinite.{u_2 + 1} (ℙ k V)

Tactic:
rwa [this]
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Infinite V
this : Infinite.{u_2 + 1} (ℙ k V) ↔ Infinite V
⊢ Infinite.{u_2 + 1} (ℙ k V)

Tactic:
have : Infinite (ℙ k V) := by rwa [this]
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Infinite V
this_1 : Infinite.{u_2 + 1} (ℙ k V) ↔ Infinite V
this : Infinite.{u_2 + 1} (ℙ k V)
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
inl : ∀ (this : Fintype V), Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
haveI : Fintype V := Fintype.ofFinite V
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
this : Fintype V
inl : ∀ (this : Fintype (ℙ k V)), Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
this_1 : Fintype V
this : Fintype (ℙ k V)
inl : ∀ (this : Fintype k), Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
haveI : Fintype k := Fintype.ofFinite k
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
this_1 : Fintype V
this_2 : Fintype (ℙ k V)
this : Fintype k
⊢ Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card V - 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
this_1 : Fintype V
this_2 : Fintype (ℙ k V)
this : Fintype k
⊢ Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card V - 1

Tactic:
have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
this_1 : Fintype V
this_2 : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card V - 1
inl : Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card.{u_2} (ℙ k V) * Fintype.card.{u_1} kˣ
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]

Premises used: Fintype.card_units, Fintype.card_eq_nat_card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
this_1 : Fintype V
this_2 : Fintype (ℙ k V)
this : Fintype k
hV : Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card V - 1
inl : Fintype.card (Prod.{u_2, u_1} (ℙ k V) kˣ) = Fintype.card.{u_2} (ℙ k V) * Fintype.card.{u_1} kˣ
inl₁ inl₂ : Fintype.card.{u_2} (ℙ k V) * Fintype.card.{u_1} kˣ = Fintype.card.{u_2} (ℙ k V) * Fintype.card.{u_1} kˣ
⊢ Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card.{u_2} (ℙ k V) * Fintype.card.{u_1} kˣ

Tactic:
rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

Premises used: Fintype.card_congr, Fintype.card_prod, Projectivization.nonZeroEquivProjectivizationProdUnits
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h_2 : Finite k
h : Finite V
inl inl₁ inl₂ : ∀ (this : Fintype V), Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
inl₃ : ∀ (this : Fintype V) (this : Fintype (ℙ k V)), Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
inl₄ :
  ∀ (this : Fintype V) (this : Fintype (ℙ k V)) (this : Fintype k),
    Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
inl₅ :
  ∀ (this : Fintype V) (this_1 : Fintype (ℙ k V)) (this_2 : Fintype k)
    (hV : Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card V - 1),
    Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)
inl₆ :
  ∀ (this : Fintype V) (this_1 : Fintype (ℙ k V)) (this_2 : Fintype k)
    (hV : Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card V - 1),
    Fintype.card.{u_2} { v : V // v ≠ 0 } = Fintype.card.{u_2} (ℙ k V) * Fintype.card.{u_1} kˣ
⊢ Nat.card V - 1 = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1)

Tactic:
classical
  haveI : Fintype V := Fintype.ofFinite V
  haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  haveI : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

Premises used: Fintype.card_prod, Fintype.card_eq_nat_card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h_1 : Nontrivial V
h : Finite k
⊢ Finite V ∨ Infinite V

Tactic:
cases finite_or_infinite V with
  | inr h =>
    have := not_iff_not.mpr (finite_iff_of_finite k V)
    push Not at this
    have : Infinite (ℙ k V) := by rwa [this]
    simp
  | inl h =>
  classical
  haveI : Fintype V := Fintype.ofFinite V
  haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  haveI : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

Premises used: finite_or_infinite, Fintype.card_prod, Not, Fintype.card_eq_nat_card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
h : Nontrivial V
⊢ Finite k ∨ Infinite k

Tactic:
cases finite_or_infinite k with
  | inr h =>
    have : Infinite V := Module.Free.infinite k V
    simp
  | inl h =>
  cases finite_or_infinite V with
  | inr h =>
    have := not_iff_not.mpr (finite_iff_of_finite k V)
    push Not at this
    have : Infinite (ℙ k V) := by rwa [this]
    simp
  | inl h =>
  classical
  haveI : Fintype V := Fintype.ofFinite V
  haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  haveI : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

Premises used: finite_or_infinite, Fintype.card_prod, Not, Fintype.card_eq_nat_card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite V
rw : Nat.card V = Nat.card V - 1 + 1
⊢ Nat.card V = Nat.card.{u_2} (ℙ k V) * (Nat.card k - 1) + 1

Tactic:
rw [← card k V]

Premises used: Projectivization.card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite V
⊢ Nat.card V > 0

Tactic:
have : Nat.card V > 0 := Nat.card_pos
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite V
this : Nat.card V > 0
⊢ Nat.card V = Nat.card V - 1 + 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
⊢ 1 < Nat.card k

Tactic:
have : 1 < Nat.card k := Finite.one_lt_card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
this : 1 < Nat.card k
H : 0 < Nat.card k - 1
⊢ Nat.card.{u_2} (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
rw [card k, Nat.mul_div_cancel]

Premises used: Nat.mul_div_cancel, Projectivization.card
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
this : 1 < Nat.card k
⊢ 0 < Nat.card k - 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
inr :
  ∀
    (this :
      ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k]
        {n : ℕ} (h : Module.finrank k V = n) (hf : Finite V),
        Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i)
    (hf : ¬Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
wlog :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
⊢ Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
wlog hf : Finite V

Premises used: Finite
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
contrapose! : ∀ (hf : Finite.{u_2 + 1} (ℙ k V)), Finite V
⊢ Infinite.{u_2 + 1} (ℙ k V)

Tactic:
contrapose! hf
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Finite.{u_2 + 1} (ℙ k V)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hf : Finite V), Finite V
⊢ Finite V

Tactic:
rwa [finite_iff_of_finite] at hf

Premises used: Projectivization.finite_iff_of_finite
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
⊢ Infinite.{u_2 + 1} (ℙ k V)

Tactic:
have : Infinite (ℙ k V) := by
      contrapose! hf
      rwa [finite_iff_of_finite] at hf
-- Module: Mathlib.LinearAlgebra.Projectivization.Cardinality
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Finite k
n : ℕ
h : Module.finrank k V = n
this_1 :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_4 : AddCommGroup V] [inst_5 : Module k V] [Finite k] {n : ℕ}
    (h : Module.finrank k V = n) (hf : Finite V), Nat.card.{u_2} (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : ¬Finite V
this : Infinite.{u_2 + 1} (ℙ k V)
rw : Module.finrank k V = 0
⊢ n = 0

Tactic:
rw [← h]