awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
M' : Submodule R M
a :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{max uM uR, uM} (Module.rank R ↥M') =
    lift.{max uR uM, uM} (Module.rank R M)
a₁ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{max uR uM, uM} (Module.rank R M)
⊢ lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)
have a₂ : lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
  lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
Tactic: simp_rw [lift_add, ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalized R⁰) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
    ← IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
    ← lift_add, rank_quotient_add_rank_of_divisionRing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
M' : Submodule R M
a :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{max uM uR, uM} (Module.rank R ↥M') =
    lift.{max uR uM, uM} (Module.rank R M)
a₁ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{max uR uM, uM} (Module.rank R M)
a₂ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
⊢ lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)
have a₃ : lift.{uM, max uM uR}
      (Module.rank R
        (HasQuotient.Quotient (LocalizedModule.{uR, uM} (R := R) R⁰ M) (B :=
          Submodule (Localization (M := R) R⁰) (LocalizedModule.{uR, uM} (R := R) R⁰ M)) (Submodule.localized R⁰ M'))) +
    lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
  lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
Tactic: simp_rw [lift_add, ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalized R⁰) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
    ← IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
    ← lift_add, rank_quotient_add_rank_of_divisionRing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
M' : Submodule R M
a :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{max uM uR, uM} (Module.rank R ↥M') =
    lift.{max uR uM, uM} (Module.rank R M)
a₁ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{max uR uM, uM} (Module.rank R M)
a₂ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
a₃ :
  lift.{uM, max uM uR}
        (Module.rank R
          (HasQuotient.Quotient (LocalizedModule.{uR, uM} (R := R) R⁰ M) (B :=
            Submodule (Localization (M := R) R⁰) (LocalizedModule.{uR, uM} (R := R) R⁰ M))
            (Submodule.localized R⁰ M'))) +
      lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
⊢ lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)
have a₄ : lift.{uM, max uM uR}
      (Module.rank (FractionRing R)
        (HasQuotient.Quotient (LocalizedModule.{uR, uM} (R := R) R⁰ M) (B :=
          Submodule (Localization (M := R) R⁰) (LocalizedModule.{uR, uM} (R := R) R⁰ M)) (Submodule.localized R⁰ M'))) +
    lift.{uM, max uM uR} (Module.rank (FractionRing R) ↥(Submodule.localized R⁰ M')) =
  lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M))
Tactic: simp_rw [lift_add, ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalized R⁰) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
    ← IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
    ← lift_add, rank_quotient_add_rank_of_divisionRing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
M' : Submodule R M
a :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{max uM uR, uM} (Module.rank R ↥M') =
    lift.{max uR uM, uM} (Module.rank R M)
a₁ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{max uR uM, uM} (Module.rank R M)
a₂ :
  lift.{max uM uR, uM} (Module.rank R (M ⧸ M')) + lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
a₃ :
  lift.{uM, max uM uR}
        (Module.rank R
          (HasQuotient.Quotient (LocalizedModule.{uR, uM} (R := R) R⁰ M) (B :=
            Submodule (Localization (M := R) R⁰) (LocalizedModule.{uR, uM} (R := R) R⁰ M))
            (Submodule.localized R⁰ M'))) +
      lift.{uM, max uM uR} (Module.rank R ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M))
a₄ :
  lift.{uM, max uM uR}
        (Module.rank (FractionRing R)
          (HasQuotient.Quotient (LocalizedModule.{uR, uM} (R := R) R⁰ M) (B :=
            Submodule (Localization (M := R) R⁰) (LocalizedModule.{uR, uM} (R := R) R⁰ M))
            (Submodule.localized R⁰ M'))) +
      lift.{uM, max uM uR} (Module.rank (FractionRing R) ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M))
⊢ lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)
have a₅ : lift.{uM, max uM uR}
    (Module.rank (FractionRing R)
        (HasQuotient.Quotient (LocalizedModule.{uR, uM} (R := R) R⁰ M) (B :=
          Submodule (Localization (M := R) R⁰) (LocalizedModule.{uR, uM} (R := R) R⁰ M)) (Submodule.localized R⁰ M')) +
      Module.rank (FractionRing R) ↥(Submodule.localized R⁰ M')) =
  lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M))
Tactic: simp_rw [lift_add, ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalized R⁰) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
    ← IsLocalizedModule.lift_rank_eq R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
    ← IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
    ← lift_add, rank_quotient_add_rank_of_divisionRing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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 uP
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have rw : Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
  Cardinal.lift.{max uP (max uN uS) uT, uM} (Module.rank R M)
Tactic: rw [← lift_inj.{_, max uS uT uN}, lift_lift, lift_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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 uP
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
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uP (max uN uS) uT, uM} (Module.rank R M)
have rw : Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
  (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))
Tactic: rw [← lift_lift.{uN, max uS uT uP}, ← IsLocalizedModule.lift_rank_eq p f hp,
    ← IsLocalization.rank_eq S p hp, lift_lift, ← lift_lift.{max uS uT, max uM uP},
    ← rank_baseChange (R := ST), ← lift_id'.{max uS uT, max uS uT uN} (Module.rank ..),
    lift_lift, ← lift_lift.{max uS uT uP, uM}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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 uP
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
ST : Type (max uS uT) := S ⊗[R] T
⊢ Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
    Cardinal.lift.{max uP (max uN uS) uT, uM} (Module.rank R M)
have conv_rhs : Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
  Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
    (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))
Tactic: conv_rhs => rw [← lift_lift.{uN, max uS uT uP}, ← IsLocalizedModule.lift_rank_eq p f hp,
    ← IsLocalization.rank_eq S p hp, lift_lift, ← lift_lift.{max uS uT, max uM uP},
    ← rank_baseChange (R := ST), ← lift_id'.{max uS uT, max uS uT uN} (Module.rank ..),
    lift_lift, ← lift_lift.{max uS uT uP, uM}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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
inst_15 : StrongRankCondition (S ⊗[R] T)
P : Type uP
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
ST : Type (max uS uT) := S ⊗[R] T
x : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uM (max uN uS) uT, uP} (Module.rank T P) =
    Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
      (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))
have rw : Cardinal.lift.{max uS uT uN, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P)) =
  Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N))
Tactic: rw [← lift_lift.{max uS uT, max uM uN}, ← lift_umax.{uP},
    ← IsLocalizedModule.lift_rank_eq pT (mk T ST P 1) hpT,
    ← IsLocalization.rank_eq ST pT hpT, lift_id'.{uP, max uS uT},
    ← lift_id'.{max uS uT, max uS uT uP} (Module.rank ..), lift_lift,
    ← lift_lift.{max uS uT uN, uM}, lift_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have inj : Function.Injective.{uR + 1, uT + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
Tactic: have inj := FaithfulSMul.algebraMap_injective R T
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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)
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have this : NoZeroDivisors R
Tactic: have := inj.noZeroDivisors _ (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have inl : Subsingleton R → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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)
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have inr : Nontrivial R → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have this₁ : Subsingleton T
Tactic: have := (algebraMap R T).codomain_trivial
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have this₁ : IsDomain T
Tactic: have := (isDomain_iff_noZeroDivisors_and_nontrivial T).mpr
    ⟨‹_›, (FaithfulSMul.algebraMap_injective R T).nontrivial⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have inj₁ : 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
Cleared hypotheses: inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
have this₁ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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 hS₁ : ¬∀ (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
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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)
⊢ ℵ₀ ≤ Module.rank R R
have hS₁ : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
Tactic: push Not at hS
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 : ∃ (r : R) (s : ↥(R⁰ : Submonoid R)), ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
⊢ ℵ₀ ≤ Module.rank R R
have obtain : ∀ (r : R) (s : ↥(R⁰ : Submonoid R)) (h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)),
  ℵ₀ ≤ Module.rank R R
Tactic: obtain ⟨r, s, h⟩ := hS
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
r : R
s : ↥(R⁰ : Submonoid R)
h : ∀ (r' : R) (s' : ↥(R⁰ : Submonoid R)), (↑s' : R) * r ≠ r' * (↑s : R)
⊢ ℵ₀ ≤ Module.rank R R
have refine : ∀ (n : ℕ), (↑n : Cardinal.{u_1}) ≤ Module.rank R R
Tactic: refine Cardinal.aleph0_le.mpr fun n ↦ ?_
-- 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 : ℕ
⊢ (↑n : Cardinal.{u_1}) ≤ Module.rank R R
have suffices : LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
Tactic: suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank
-- 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 : ℕ
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 : ℕ)
have 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
Tactic: refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
-- 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 : ℕ
⊢ LinearIndependent R (M := R) fun (i : Fin n) ↦ r * (↑s : R) ^ (↑i : ℕ)
have 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
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
-- 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 : 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
have 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
Tactic: rw [Finset.sum_range_succ'] at hg
Cleared hypotheses: 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 : ℕ
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
⊢ g i = 0
have pos : ∀ (hg0 : g 0 = 0), g i = 0
Tactic: by_cases hg0 : g 0 = 0