-- Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
lemma finite_iff_of_finite [Finite k] : Finite (ℙ k V) ↔ Finite V

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
⊢ Finite (ℙ 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

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
x : { v // v ≠ 0 } ⊕ Unit
⊢ (fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val (fun x => 0) x) = x

Tactic:
aesop

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Finite V

Tactic:
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⟩

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
eq : { v // v ≠ 0 } ⊕ Unit ≃ V :=
  { toFun := Sum.elim Subtype.val fun x => 0, invFun := fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Finite V

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
⊢ Finite V

Tactic:
have : Finite { v : V // v ≠ 0 } := Finite.of_equiv _ e.symm

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Finite V

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Function.RightInverse (fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val fun x => 0)

Tactic:
intro x

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
x : V
⊢ Sum.elim Subtype.val (fun x => 0) ((fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) x) = x

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
⊢ Finite (ℙ k V) ↔ Finite V

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

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
⊢ Finite V

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
⊢ Finite V

Tactic:
let e := nonZeroEquivProjectivizationProdUnits k V

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
⊢ Finite V

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
x : V
⊢ Sum.elim Subtype.val (fun x => 0) ((fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) x) = x

Tactic:
aesop

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
eq : { v // v ≠ 0 } ⊕ Unit ≃ V :=
  { toFun := Sum.elim Subtype.val fun x => 0, invFun := fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ Finite V

Tactic:
exact Finite.of_equiv _ eq

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
⊢ Function.LeftInverse (fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val fun x => 0)

Tactic:
intro x

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Finite (ℙ k V)
e : { v // v ≠ 0 } ≃ ℙ k V × kˣ := nonZeroEquivProjectivizationProdUnits k V
this : Finite { v // v ≠ 0 }
x : { v // v ≠ 0 } ⊕ Unit
⊢ (fun v => if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩) (Sum.elim Subtype.val (fun x => 0) x) = x