[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
⊢ Fintype (ChooseBasisIndex R M)
[PROOFSTEP]
refine @Fintype.ofFinite _ ?_
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Subsingleton R
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
have := Module.subsingleton R M
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
rw [ChooseBasisIndex]
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ _root_.Finite ↑(Exists.choose (_ : ∃ S, Nonempty (Basis (↑S) R M)))
[PROOFSTEP]
infer_instance
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Nontrivial R
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
obtain ⟨s, hs⟩ := id ‹Module.Finite R M›
[GOAL]
case inr.mk.intro
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
exact basis_finite_of_finite_spans (↑s) s.finite_toSet hs (chooseBasis _ _)
[GOAL]
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
⊢ Finite R M
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Finite R M
[PROOFSTEP]
classical
refine' ⟨⟨Finset.univ.image b, _⟩⟩
simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
[GOAL]
case intro
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Finite R M
[PROOFSTEP]
refine' ⟨⟨Finset.univ.image b, _⟩⟩
[GOAL]
case intro
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Submodule.span R ↑(Finset.image (↑b) Finset.univ) = ⊤
[PROOFSTEP]
simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
ι₁ : Type u_1
ι₂ : Type u_2
inst✝¹ : _root_.Finite ι₁
inst✝ : _root_.Finite ι₂
⊢ Finite R (Matrix ι₁ ι₂ R)
[PROOFSTEP]
cases nonempty_fintype ι₁
[GOAL]
case intro
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
ι₁ : Type u_1
ι₂ : Type u_2
inst✝¹ : _root_.Finite ι₁
inst✝ : _root_.Finite ι₂
val✝ : Fintype ι₁
⊢ Finite R (Matrix ι₁ ι₂ R)
[PROOFSTEP]
cases nonempty_fintype ι₂
[GOAL]
case intro.intro
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
ι₁ : Type u_1
ι₂ : Type u_2
inst✝¹ : _root_.Finite ι₁
inst✝ : _root_.Finite ι₂
val✝¹ : Fintype ι₁
val✝ : Fintype ι₂
⊢ Finite R (Matrix ι₁ ι₂ R)
[PROOFSTEP]
exact Module.Finite.of_basis (Pi.basis fun _ => Pi.basisFun R _)
