-- Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
/-- Fraction free cardinality formula for the points of `ℙ k V` if `k` and `V` are finite
(for silly reasons the formula also holds when `k` and `V` are infinite).
See `Projectivization.card'` and `Projectivization.card''` for other spellings of the formula. -/
lemma card : Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Proof state:
case inr
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst : Module k V] (k : Type u_1)
    (V : Type u_2) [inst : DivisionRing k] [inst_2 : AddCommGroup V] [inst_3 : Module k V],
    Nontrivial V → Finite k → Finite V → Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
h : Infinite V
this : ¬Finite (ℙ k V) ↔ ¬Finite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
simp only [not_finite_iff_infinite] at this

Result:
case inr
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst : Module k V] (k : Type u_1)
    (V : Type u_2) [inst : DivisionRing k] [inst_2 : AddCommGroup V] [inst_3 : Module k V],
    Nontrivial V → Finite k → Finite V → Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
h : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Proof state:
case inr
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst : Module k V] (k : Type u_1)
    (V : Type u_2) [inst : DivisionRing k] [inst_2 : AddCommGroup V] [inst_3 : Module k V],
    Nontrivial V → Finite k → Finite V → Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
h : Infinite V
this : Infinite (ℙ k V) ↔ Infinite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
have : Infinite (ℙ k V) := by rwa [this]

Result:
case inr
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
this✝¹ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst : Module k V] (k : Type u_1)
    (V : Type u_2) [inst : DivisionRing k] [inst_2 : AddCommGroup V] [inst_3 : Module k V],
    Nontrivial V → Finite k → Finite V → Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
h : Infinite V
this✝ : Infinite (ℙ k V) ↔ Infinite V
this : Infinite (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Proof state:
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
nontriviality V

Result:
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Proof state:
k✝¹ : Type u_1
V✝¹ : Type u_2
inst✝⁸ : DivisionRing k✝¹
inst✝⁷ : AddCommGroup V✝¹
inst✝⁶ : Module k✝¹ V✝¹
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this : Fintype V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)

Result:
k✝¹ : Type u_1
V✝¹ : Type u_2
inst✝⁸ : DivisionRing k✝¹
inst✝⁷ : AddCommGroup V✝¹
inst✝⁶ : Module k✝¹ V✝¹
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝ : Fintype V
this : Fintype (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Proof state:
k✝¹ : Type u_1
V✝¹ : Type u_2
inst✝⁸ : DivisionRing k✝¹
inst✝⁷ : AddCommGroup V✝¹
inst✝⁶ : Module k✝¹ V✝¹
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝ : Fintype V
this : Fintype (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
haveI : Fintype k := Fintype.ofFinite k

Result:
k✝¹ : Type u_1
V✝¹ : Type u_2
inst✝⁸ : DivisionRing k✝¹
inst✝⁷ : AddCommGroup V✝¹
inst✝⁶ : Module k✝¹ V✝¹
k✝ : Type u_1
V✝ : Type u_2
inst✝⁵ : DivisionRing k✝
inst✝⁴ : AddCommGroup V✝
inst✝³ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝¹ : Fintype V
this✝ : Fintype (ℙ k V)
this : Fintype k
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)