awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
hp : p ≤ R⁰
inst_11 : Free S N
inst_12 : StrongRankCondition S
T : Type uT
inst_13 : CommRing T
inst_14 : Algebra R T
hpT : LE.le (α := Submonoid T) (Algebra.algebraMapSubmonoid T p) T⁰
inst_15 : StrongRankCondition (S ⊗[R] T)
P : Type uM
inst_16 : AddCommGroup P
inst_17 : Module R P
inst_18 : Module T P
inst_19 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Module.rank T P = Module.rank R M

Tactic:
simpa using lift_rank_eq_of_le_nonZeroDivisors S f hp hpT bc

Premises used: IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
have inj := FaithfulSMul.algebraMap_injective R T
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ NoZeroDivisors R

Tactic:
have := inj.noZeroDivisors _ (map_zero _) (map_mul _)
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
this : NoZeroDivisors R
inl : Subsingleton R → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
inr : Nontrivial R → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
this : NoZeroDivisors R
h : Subsingleton R
⊢ Subsingleton T

Tactic:
have := (algebraMap R T).codomain_trivial
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
this_1 : NoZeroDivisors R
h : Subsingleton R
this : Subsingleton T
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
simp only [rank_subsingleton, lift_one]

Premises used: Cardinal.lift_one, rank_subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
this : NoZeroDivisors R
h : Nontrivial R
⊢ IsDomain T

Tactic:
have := (isDomain_iff_noZeroDivisors_and_nontrivial T).mpr
    ⟨‹_›, (FaithfulSMul.algebraMap_injective R T).nontrivial⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
this_1 : NoZeroDivisors R
h : Nontrivial R
this : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
⊢ Function.Injective.{uR + 1, uT + 1} (α := R) (β := FT) (⇑(algebraMap R FT) : (a : R) → FT)

Tactic:
replace inj : Function.Injective (algebraMap R FT) := (IsFractionRing.injective T _).comp inj
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g_1 : M →ₗ[R] P
bc : IsBaseChange T g_1
this_1 : NoZeroDivisors R
h : Nontrivial R
this : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := FT) (⇑(algebraMap R FT) : (a : R) → FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P : (a : FT) → P →ₗ[T] FT ⊗[T] P) 1
⊢ IsLocalizedModule (R := R) (M := FT) (M' := FR ⊗[R] FT) R⁰
    ((TensorProduct.mk R FR FT : (a : FR) → FT →ₗ[R] FR ⊗[R] FT) 1)

Tactic:
have : IsLocalizedModule R⁰ (TensorProduct.mk R FR FT 1) := inferInstance
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uP
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ finrank T P = finrank R M

Tactic:
simpa using congr_arg toNat bc.lift_rank_eq

Premises used: Cardinal.toNat, congr_arg, IsBaseChange.lift_rank_eq, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
T : Type uT
inst_3 : CommRing T
inst_4 : NoZeroDivisors T
inst_5 : Algebra R T
inst_6 : FaithfulSMul R T
P : Type uM
inst_7 : AddCommGroup P
inst_8 : Module R P
inst_9 : Module T P
inst_10 : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Module.rank T P = Module.rank R M

Tactic:
simpa using bc.lift_rank_eq

Premises used: IsBaseChange.lift_rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : IsEmpty.{u_1 + 1} (OreLocalization.OreSet (R⁰ : Submonoid R))
⊢ ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)

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

Premises used: OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors, not_nonempty_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : ¬∀ (r : R) (s : ↥(R⁰ : Submonoid R)), ∃ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r = r' * (↑s : R)
⊢ ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)

Tactic:
push Not at hS

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsDomain R
hS : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
obtain :
  ∀ (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

Tactic:
obtain ⟨r, s, h⟩ := hS
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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)
⊢ ℵ₀ ≤ Module.rank R R

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

Premises used: Iff.mpr, Cardinal.aleph0_le
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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)
refine : ∀ (n : ℕ), (↑n : Cardinal.{u_1}) ≤ Module.rank R R
⊢ ℵ₀ ≤ Module.rank R R

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

Premises used: Iff.mpr, Cardinal.aleph0_le
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
this : LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
⊢ (↑n : Cardinal.{u_1}) ≤ Module.rank R R

Tactic:
simpa using this.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
suffices : LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
⊢ (↑n : Cardinal.{u_1}) ≤ Module.rank R R

Tactic:
suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
this :
  ∀ (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
⊢ LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)

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

Premises used: Iff.mpr, Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
this :
  ∀ (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
refine :
  ∀ (g : Fin n → R) (hg : Eq.{u_1 + 1} (α := R) (∑ i : Fin n, g i • (r * (↑s : R) ^ (↑i : ℕ))) 0) (i : Fin n), g i = 0
⊢ LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)

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

Premises used: Iff.mpr, Fintype.linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
this :
  ∀ (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
g : Fin n → R
hg : Eq.{u_1 + 1} (α := R) (∑ i : Fin n, g i • (r * (↑s : R) ^ (↑i : ℕ))) 0
i : Fin n
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i ∈ Finset.range n,
      HSMul.hSMul (α := R) ((fun (i : ℕ) ↦ (if h : i < n then g ⟨i, h⟩ else 0 : R)) i) (r * (↑s : R) ^ (i + 0)))
    0

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

Premises used: Fin.sum_univ_eq_sum_range
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
this :
  ∀ (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
g : Fin n → R
hg : Eq.{u_1 + 1} (α := R) (∑ i : Fin n, g i • (r * (↑s : R) ^ (↑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

Premises used: Fin.prop, dif_pos, Fin.mk, Fin.val, dite, LT.lt, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
suffices :
  ∀ (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
⊢ LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)

Tactic:
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
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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)
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:
contradiction
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range (n + 1), g i • (r * (↑s : R) ^ (i + x))) 0
i : ℕ
hin : i < n + 1
succ :
  ∀ (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), g i = 0
⊢ g i = 0

Tactic:
rw [Finset.sum_range_succ'] at hg

Premises used: Finset.sum_range_succ'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
neg : ∀ (hg0 : ¬g 0 = 0), g i = 0
⊢ g i = 0

Tactic:
by_cases hg0 : g 0 = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
⊢ 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

Premises used: add_assoc, zero_smul, add_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
pos₁ : ∀ (n_1 : ℕ) (hin : n_1 + 1 < n + 1), g (n_1 + 1) = 0
⊢ g i = 0

Tactic:
cases i
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
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
hin : 0 < n + 1
⊢ g 0 = 0

Tactic:
hg0
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
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
n_1 : ℕ
hin : n_1 + 1 < n + 1
⊢ g (n_1 + 1) = 0

Tactic:
IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)

Premises used: Nat.succ_lt_succ_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 : ℕ
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
hin : 0 < n + 1
⊢ g 0 = 0

Tactic:
exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
⊢ (∑ 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

Premises used: pow_succ, mul_assoc, pow_add, zero_add, smul_eq_mul, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
⊢ (-∑ 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

Premises used: neg_eq_iff_add_eq_zero, neg_mul
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
⊢ (-∑ 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
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * (↑s : R) ^ i) * (↑s : R) = g 0 * r
⊢ g 0 ≠ 0

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * (↑s : R) ^ i) * (↑s : R) = g 0 * r
⊢ g i = 0

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

Premises used: Iff.mpr, False.elim, Subtype.mk, mem_nonZeroDivisors_iff_ne_zero, OfNat.ofNat, Eq.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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
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
⊢ 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

Premises used: neg_eq_iff_add_eq_zero, pow_succ, add_assoc, mul_assoc, pow_add, zero_add, zero_smul, neg_mul, smul_eq_mul, add_zero, OfNat.ofNat, Finset.sum_range_succ', Finset.sum_mul