awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < n), g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * (↑s : R) ^ (k + 1 + x)) + g 0 • (r * (↑s : R) ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
pos : ∀ (hg0 : g 0 = 0), g i = 0
⊢ g i = 0
have neg : ∀ (hg0 : ¬g 0 = 0), g i = 0
Tactic: by_cases hg0 : g 0 = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < n), g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * (↑s : R) ^ (k + 1 + x)) + g 0 • (r * (↑s : R) ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
hg0 : g 0 = 0
⊢ g i = 0
have hg₁ : Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * (↑s : R) ^ (x_1 + (1 + x)))) 0
Tactic: simp only [hg0, zero_smul, add_zero, add_assoc] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < n), g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : g 0 = 0
hg : Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * (↑s : R) ^ (x_1 + (1 + x)))) 0
⊢ g i = 0
have pos : ∀ (hin : 0 < n + 1), g 0 = 0
Tactic: cases i
Cleared hypotheses: i, hin
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < n), g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : g 0 = 0
hg : Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * (↑s : R) ^ (x_1 + (1 + x)))) 0
pos : ∀ (hin : 0 < n + 1), g 0 = 0
⊢ g i = 0
have pos₁ : ∀ (n_1 : ℕ) (hin : n_1 + 1 < n + 1), g (n_1 + 1) = 0
Tactic: cases i
Cleared hypotheses: i, hin
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < n), g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * (↑s : R) ^ (k + 1 + x)) + g 0 • (r * (↑s : R) ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
⊢ g i = 0
have hg₁ : (∑ i ∈ Finset.range n, g (i + 1) * r * (↑s : R) ^ i) * (↑s : R) * (↑s : R) ^ x + g 0 * r * (↑s : R) ^ x = 0
Tactic: simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : 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 : R) ^ i) * (↑s : R) * (↑s : R) ^ x + g 0 * r * (↑s : R) ^ x = 0
⊢ g i = 0
have hg₁ : (-∑ i ∈ Finset.range n, g (i + 1) * r * (↑s : R) ^ i) * (↑s : R) * (↑s : R) ^ x = g 0 * r * (↑s : R) ^ x
Tactic: rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
IH :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : 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 : R) ^ i) * (↑s : R) * (↑s : R) ^ x = g 0 * r * (↑s : R) ^ x
⊢ g i = 0
have this : (-∑ i ∈ Finset.range n, g (i + 1) * r * (↑s : R) ^ i) * (↑s : R) = g 0 * r
Tactic: have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
g : ℕ → R
x : ℕ
hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0
i : ℕ
hin : i < n
⊢ g i = 0
have zero : ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range 0, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
  (hin : i < 0), g i = 0
Tactic: induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: n, g, x, hg, i, hin
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
n : ℕ
g : ℕ → R
x : ℕ
hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0
i : ℕ
hin : i < n
zero :
  ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range 0, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
    (hin : i < 0), g i = 0
⊢ g i = 0
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0) (i : ℕ)
      (hin : i < n), g i = 0)
  (g : ℕ → R) (x : ℕ) (hg : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range (n + 1), g i • (r * (↑s : R) ^ (i + x))) 0)
  (i : ℕ) (hin : i < n + 1), g i = 0
Tactic: induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: n, g, x, hg, i, hin
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
⊢ ℵ₀ ≤ Module.rank R R
have rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
⊢ ℵ₀ ≤ Module.rank R R
have rw₁ : ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
  ℵ₀ ≤ Module.rank R R
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
rw₁ rw₂ rw₃ :
  ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
⊢ ℵ₀ ≤ Module.rank R R
have rw₄ : ∀ (hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
  ℵ₀ ≤ Module.rank R R
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
rw₁ rw₂ rw₃ :
  ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₄ :
  ∀ (hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
⊢ ℵ₀ ≤ Module.rank R R
have rw₅ : ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
  ℵ₀ ≤ Module.rank R R
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
rw₁ rw₂ rw₃ :
  ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₄ :
  ∀ (hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₅ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
⊢ ℵ₀ ≤ Module.rank R R
have rw₆ : ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)) (n : ℕ),
  (↑n : Cardinal.{u_1}) ≤ Module.rank R R
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
rw₁ rw₂ rw₃ :
  ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₄ :
  ∀ (hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₅ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₆ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R))
    (n : ℕ), (↑n : Cardinal.{u_1}) ≤ Module.rank R R
⊢ ℵ₀ ≤ Module.rank R R
have rw₇ : ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)) (n : ℕ),
  LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
rw : ∀ (hS : ¬Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), ℵ₀ ≤ Module.rank R R
rw₁ rw₂ rw₃ :
  ∀ (hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₄ :
  ∀ (hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₅ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
    ℵ₀ ≤ Module.rank R R
rw₆ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R))
    (n : ℕ), (↑n : Cardinal.{u_1}) ≤ Module.rank R R
rw₇ :
  ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R))
    (n : ℕ), LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
⊢ ℵ₀ ≤ Module.rank R R
have rw₈ : ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)) (n : ℕ)
  (g : ℕ → R) (x : ℕ), Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range n, g i • (r * (↑s : R) ^ (i + x))) 0 → ∀ i < n, g i = 0
Tactic: classical
  rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
  push Not at hS
  obtain ⟨r, s, h⟩ := hS
  refine Cardinal.aleph0_le.mpr fun n ↦ ?_
  suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
  suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 →
      ∀ i < n, g i = 0 by
    refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
    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
  intro g x hg i hin
  induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
⊢ Nonempty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
have by_contra! : ∀ (h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
⊢ False
have this : ℵ₀ ≤ Module.rank R R
Tactic: have := aleph0_le_rank_of_isEmpty_oreSet h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
h : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
this : ℵ₀ ≤ Module.rank R R
⊢ False
have this₁ : ℵ₀ ≤ 1
Tactic: rw [rank_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.OrzechProperty (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : OrzechProperty R
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_3
inst_4 : Fintype ι
b : ι → M
spans : LE.le (α := Submodule R M) ⊤ (span R (Set.range b))
card_le : Fintype.card ι ≤ finrank R M
⊢ LinearIndependent R b
have spans₁ : Function.Surjective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R b) : (a : ι →₀ R) → M)
Tactic: rw [← Finsupp.range_linearCombination, top_le_iff, LinearMap.range_eq_top] at spans
Cleared hypotheses: spans, card_le