-- 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:
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
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
wlog h : Finite V

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 : ¬Finite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

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
⊢ 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
⊢ Nat.card V - 1 = Nat.card (ℙ 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]

Result:
no goals

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)
this : Fintype k
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

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

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
hV : Fintype.card { v // v ≠ 0 } = Fintype.card V - 1
⊢ Fintype.card { v // v ≠ 0 } = Fintype.card (ℙ k V) * Fintype.card kˣ

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
this : Infinite (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
simp

Result:
no goals

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 : ¬Finite V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
simp only [not_finite_iff_infinite] at h

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
⊢ 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
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
⊢ Infinite (ℙ k V)

Tactic:
rwa [this]

Result:
no goals

Proof state:
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)

Tactic:
wlog h : Finite k

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

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
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)