-- Mathlib/LinearAlgebra/Dimension/Localization.lean
/-- A domain that is not (left) Ore is of infinite rank.
See [cohn_1995] Proposition 1.3.6 -/
lemma aleph0_le_rank_of_isEmpty_oreSet (hS : IsEmpty (OreLocalization.OreSet R⁰)) :
    ℵ₀ ≤ Module.rank R R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s = g 0 * r
⊢ g 0 ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : IsEmpty (OreLocalization.OreSet R⁰)
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ¬∀ (r : R) (s : ↥R⁰), ∃ r' s', ↑s' * r = r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : Fin n → R
hg : ∑ i : Fin n, g i • (r * ↑s ^ ↑i) = 0
i : Fin n
⊢ ∑ i ∈ Finset.range n, (fun i => if h : i < n then g ⟨i, h⟩ else 0) i • (r * ↑s ^ (i + 0)) = 0

Tactic:
simp [← Fin.sum_univ_eq_sum_range, ← hg]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ¬∀ (r : R) (s : ↥R⁰), ∃ r' s', ↑s' * r = r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
push_neg at hS

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ∃ r s, ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : Fin n → R
hg : ∑ i : Fin n, g i • (r * ↑s ^ ↑i) = 0
i : Fin n
⊢ g i = 0

Tactic:
simpa only [dif_pos i.prop] using this (fun i ↦ if h : i < n then g ⟨i, h⟩ else 0) 0
  (by simp [← Fin.sum_univ_eq_sum_range, ← hg]) i i.prop

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
refine Cardinal.aleph0_le.mpr fun n ↦ ?_

Result:
case intro.intro
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ ↑n ≤ Module.rank R R

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s = g 0 * r
⊢ g i = 0

Tactic:
exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
⊢ g i = 0

Tactic:
have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s = g 0 * r
⊢ g i = 0

Proof state:
case intro.intro.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
g : ℕ → R
x : ℕ
hg : ∑ i ∈ Finset.range 0, g i • (r * ↑s ^ (i + x)) = 0
i : ℕ
hin : i < 0
⊢ g i = 0

Tactic:
exact (hin.not_le (zero_le i)).elim

Result:
no goals

Proof state:
case intro.intro.succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg : ∑ i ∈ Finset.range (n + 1), g i • (r * ↑s ^ (i + x)) = 0
i : ℕ
hin : i < n + 1
⊢ g i = 0

Tactic:
rw [Finset.sum_range_succ'] at hg

Result:
case intro.intro.succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * ↑s ^ (k + 1 + x)) + g 0 • (r * ↑s ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
⊢ g i = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : ∃ r s, ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
obtain ⟨r, s, h⟩ := hS

Result:
case intro.intro
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
⊢ ℵ₀ ≤ Module.rank R R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : LinearIndependent R fun i => r * ↑s ^ ↑i
⊢ ↑n ≤ Module.rank R R

Tactic:
simpa using this.cardinal_lift_le_rank

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
⊢ LinearIndependent R fun i => r * ↑s ^ ↑i

Tactic:
refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : Fin n → R
hg : ∑ i : Fin n, g i • (r * ↑s ^ ↑i) = 0
i : Fin n
⊢ g i = 0

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x + g 0 * r * ↑s ^ x = 0
⊢ g i = 0

Tactic:
rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
⊢ g i = 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ ↑n ≤ Module.rank R R

Tactic:
suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
  simpa using this.cardinal_lift_le_rank

Result:
case intro.intro
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ LinearIndependent R fun i => r * ↑s ^ ↑i