-- 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
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 : Infinite k
this : Infinite 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
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)

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

Tactic:
simp

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

Tactic:
have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp

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

Tactic:
have : Infinite V := Module.Free.infinite k V

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

Tactic:
have := not_iff_not.mpr (finite_iff_of_finite k 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 : Infinite V
this : ¬Finite (ℙ k V) ↔ ¬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:
haveI : Fintype V := Fintype.ofFinite 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
⊢ 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)
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ˣ

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

Result:
no goals