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

Tactic:
exact nm k'

Result:
no goals

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
⊢ Finite ι

Tactic:
haveI := hw.to_subtype

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
⊢ 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
⊢ Finite ι

Tactic:
classical
haveI := hw.to_subtype
cases nonempty_fintype w
rw [← not_infinite_iff_finite]
intro i
let S : Finset ι := Finset.univ.sup fun x : w => (b.repr x).support
let bS : Set M := b '' S
have h : ∀ x ∈ w, x ∈ span R bS := by
  intro x m
  rw [← b.linearCombination_repr x, span_image_eq_map_linearCombination, Submodule.mem_map]
  use b.repr x
  simp only [and_true, eq_self_iff_true, Finsupp.mem_supported]
  rw [Finset.coe_subset, ← Finset.le_iff_subset]
  exact Finset.le_sup (f := fun x : w ↦ (b.repr ↑x).support) (Finset.mem_univ (⟨x, m⟩ : w))
have k : span R bS = ⊤ := eq_top_iff.2 (le_trans s.ge (span_le.2 h))
obtain ⟨x, nm⟩ := Infinite.exists_not_mem_finset S
have k' : b x ∈ span R bS := by
  rw [k]
  exact mem_top
simp only [self_mem_span_image, Finset.mem_coe, bS] at k'
exact nm k'

Result:
no goals

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:
rw [Finset.coe_subset, ← Finset.le_iff_subset]

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).support ≤ S

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
⊢ Finite ι

Tactic:
rw [← not_infinite_iff_finite]

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
⊢ ¬Infinite ι

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 ∈ supported R R ↑S ∧ (linearCombination R ⇑b) (b.repr x) = (linearCombination R ⇑b) (b.repr x)

Tactic:
simp only [and_true, eq_self_iff_true, Finsupp.mem_supported]

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).support ⊆ ↑S

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
⊢ ¬Infinite ι

Tactic:
intro i

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 ι
⊢ 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
⊢ False

Tactic:
have h : ∀ x ∈ w, x ∈ span R bS := by
  intro x m
  rw [← b.linearCombination_repr x, span_image_eq_map_linearCombination, Submodule.mem_map]
  use b.repr x
  simp only [and_true, eq_self_iff_true, Finsupp.mem_supported]
  rw [Finset.coe_subset, ← Finset.le_iff_subset]
  exact Finset.le_sup (f := fun x : w ↦ (b.repr ↑x).support) (Finset.mem_univ (⟨x, m⟩ : 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
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

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 ∈ w, x ∈ span R bS

Tactic:
intro x m

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
⊢ x ∈ span R bS

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
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
⊢ b x ∈ ⊤

Tactic:
exact mem_top

Result:
no goals