-- Mathlib/LinearAlgebra/Basis/Cardinality.lean
/--
Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
-/
lemma basis_finite_of_finite_spans (w : Set M) (hw : w.Finite) (s : span R w = ⊤) {ι : Type w}
    (b : Basis ι R M) : Finite ι

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
x : M
m : x ∈ w
⊢ x ∈ span R bS

Tactic:
rw [← b.linearCombination_repr x, span_image_eq_map_linearCombination, Submodule.mem_map]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
x : M
m : x ∈ w
⊢ ∃ y ∈ supported R R ↑S, (linearCombination R ⇑b) y = (linearCombination R ⇑b) (b.repr x)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
x : M
m : x ∈ w
⊢ ∃ y ∈ supported R R ↑S, (linearCombination R ⇑b) y = (linearCombination R ⇑b) (b.repr x)

Tactic:
use b.repr x

Result:
case h
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
x : M
m : x ∈ w
⊢ b.repr x ∈ supported R R ↑S ∧ (linearCombination R ⇑b) (b.repr x) = (linearCombination R ⇑b) (b.repr x)

Proof state:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
k' : b x ∈ span R bS
⊢ False

Tactic:
simp only [self_mem_span_image, Finset.mem_coe, bS] at k'

Result:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
k' : x ∈ S
⊢ False

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
⊢ False

Tactic:
let S : Finset ι := Finset.univ.sup fun x : w => (b.repr x).support

Result:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
⊢ False

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
⊢ False

Tactic:
let bS : Set M := b '' S

Result:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
⊢ False

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
⊢ False

Tactic:
obtain ⟨x, nm⟩ := Infinite.exists_not_mem_finset S

Result:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
⊢ False

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
⊢ Finite ι

Tactic:
cases nonempty_fintype w

Result:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
⊢ Finite ι

Proof state:
case h
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
x : M
m : x ∈ w
⊢ (b.repr x).support ≤ S

Tactic:
exact Finset.le_sup (f := fun x : w ↦ (b.repr ↑x).support) (Finset.mem_univ (⟨x, m⟩ : w))

Result:
no goals

Proof state:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
⊢ False

Tactic:
have k' : b x ∈ span R bS := by
  rw [k]
  exact mem_top

Result:
case intro.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
k' : b x ∈ span R bS
⊢ False

Proof state:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
⊢ False

Tactic:
have k : span R bS = ⊤ := eq_top_iff.2 (le_trans s.ge (span_le.2 h))

Result:
case intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
⊢ False