awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
inr : ⨆ (ι : { s : Set N // LinearIndepOn S id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank R N
⊢ Module.rank S N ≤ Module.rank R N

Tactic:
rw [Module.rank]

Premises used: Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
inr : ∀ (i : { s : Set N // LinearIndepOn S id s }), #(↑(↑i : Set N) : Type uN) ≤ Module.rank R N
⊢ ⨆ (ι : { s : Set N // LinearIndepOn S id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank R N

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
inr : ⨆ (ι : { s : Set N // LinearIndepOn R id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank S N
⊢ Module.rank R N ≤ Module.rank S N

Tactic:
rw [Module.rank]

Premises used: Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
inr : ∀ (i : { s : Set N // LinearIndepOn R id s }), #(↑(↑i : Set N) : Type uN) ≤ Module.rank S N
⊢ ⨆ (ι : { s : Set N // LinearIndepOn R id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank S N

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set N
hs : LinearIndepOn S id s
⊢ FaithfulSMul R S

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R S).mpr inj
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set N
hs : LinearIndepOn S id s
this : FaithfulSMul R S
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn S id s) s hs) : Set N) : Type uN) ≤ Module.rank R N

Tactic:
(hs.restrict_scalars' R).cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, LinearIndependent.restrict_scalars'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set N
hs : LinearIndepOn S id s
this : FaithfulSMul R S
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn S id s) s hs) : Set N) : Type uN) ≤ Module.rank R N

Tactic:
exact (hs.restrict_scalars' R).cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, LinearIndependent.restrict_scalars'
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set N
hs : LinearIndepOn R id s
⊢ Nontrivial S

Tactic:
have := inj.nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set N
hs : LinearIndepOn R id s
this : Nontrivial S
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn R id s) s hs) : Set N) : Type uN) ≤ Module.rank S N

Tactic:
(hs.localization S p).cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, LinearIndependent.localization
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
S : Type uS
N : Type uN
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
hp : p ≤ R⁰
h : Nontrivial R
inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set N
hs : LinearIndepOn R id s
this : Nontrivial S
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn R id s) s hs) : Set N) : Type uN) ≤ Module.rank S N

Tactic:
exact (hs.localization S p).cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank, LinearIndependent.localization
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
obtain :
  ∀ (w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M)
    (hw : LinearIndependent R w), ∃ (s : Set M), #(↑s : Type uM) = Module.rank R M ∧ LinearIndepOn R id s
⊢ ∃ (s : Set M), #(↑s : Type uM) = Module.rank R M ∧ LinearIndepOn R id s

Tactic:
obtain ⟨w, hw⟩ :=
    IsLocalizedModule.linearIndependent_lift R⁰ (LocalizedModule.mkLinearMap R⁰ M) <|
      Module.Free.chooseBasis (FractionRing R) (LocalizedModule R⁰ M)
        |>.linearIndependent.restrict_scalars' _

Premises used: LocalizedModule, FractionRing, nonZeroDivisors, LinearIndependent.restrict_scalars', IsLocalizedModule.linearIndependent_lift, Module.Basis.linearIndependent, LocalizedModule.mkLinearMap, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M
hw : LinearIndependent R w
⊢ ∃ (s : Set M), #(↑s : Type uM) = Module.rank R M ∧ LinearIndepOn R id s

Tactic:
⟨Set.range w, ?_, (linearIndepOn_id_range_iff hw.injective).mpr hw⟩

Premises used: Iff.mpr, linearIndepOn_id_range_iff, LinearIndependent.injective, And.intro, Exists.intro, Set.range
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M
hw : LinearIndependent R w
refine : #(↑(Set.range w) : Type uM) = Module.rank R M
⊢ ∃ (s : Set M), #(↑s : Type uM) = Module.rank R M ∧ LinearIndepOn R id s

Tactic:
refine ⟨Set.range w, ?_, (linearIndepOn_id_range_iff hw.injective).mpr hw⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M
hw : LinearIndependent R w
a : lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)
⊢ #(↑(Set.range w) : Type uM) = Module.rank R M

Tactic:
apply Cardinal.lift_injective.{max uR uM}
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M
hw : LinearIndependent R w
a :
  lift.{uM, max uM uR} #(Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M)) =
    lift.{max uR uM, uM} (Module.rank R M)
a₁ :
  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)
a₂ :
  lift.{uM, max uM uR} (Module.rank R (LocalizedModule.{uR, uM} (R := R) R⁰ M)) = lift.{max uR uM, uM} (Module.rank R M)
a₃ a₄ : lift.{max uM uR, uM} (Module.rank R M) = lift.{max uR uM, uM} (Module.rank R M)
⊢ lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)

Tactic:
rw [Cardinal.mk_range_eq_of_injective hw.injective, ← Module.Free.rank_eq_card_chooseBasisIndex,
    IsLocalization.rank_eq (FractionRing R) R⁰ le_rfl,
    IsLocalizedModule.lift_rank_eq R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl]

Premises used: le_rfl, Cardinal.mk_range_eq_of_injective, FractionRing, nonZeroDivisors, LinearIndependent.injective, IsLocalizedModule.lift_rank_eq, IsLocalization.rank_eq, LocalizedModule.mkLinearMap, Module.Free.rank_eq_card_chooseBasisIndex
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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 uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M

Tactic:
apply lift_injective.{max uR uM}
-- Module: Mathlib.LinearAlgebra.Dimension.Localization
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))
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))
⊢ lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank 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]

Premises used: le_rfl, FractionRing, nonZeroDivisors, IsLocalizedModule.lift_rank_eq, IsLocalization.rank_eq, Submodule.toLocalizedQuotient, LocalizedModule.mkLinearMap, rank_quotient_add_rank_of_divisionRing, Submodule.toLocalized, Cardinal.lift_add
-- 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 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
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)
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
rw [← lift_inj.{_, max uS uT uN}, lift_lift, lift_lift]

Premises used: Cardinal.lift_lift
-- 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 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
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)))
| Cardinal.lift.{max uP (max uN uS) uT, uM} (Module.rank R M)

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}]

Premises used: Module.rank_baseChange, Cardinal.lift_lift, IsLocalizedModule.lift_rank_eq, IsLocalization.rank_eq
-- 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 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
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)))
⊢ 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:
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}]

Premises used: Module.rank_baseChange, Cardinal.lift_lift, IsLocalizedModule.lift_rank_eq, IsLocalization.rank_eq
-- 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 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
⊢ let pT : Submonoid T := Algebra.algebraMapSubmonoid T p;
  pT ≤ T⁰

Tactic:
set pT := Algebra.algebraMapSubmonoid T p

Premises used: Algebra.algebraMapSubmonoid
-- 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
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⁰
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))
⊢ 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:
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]

Premises used: Cardinal.lift_lift, IsLocalizedModule.lift_rank_eq, Cardinal.lift_inj, IsLocalization.rank_eq, OfNat.ofNat, DFunLike.coe, TensorProduct.mk
-- 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
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 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:
LinearEquiv.lift_rank_eq <| AlgebraTensorModule.congr (.refl ST ST) bc.equiv.symm ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange .. ≪≫ₗ (AlgebraTensorModule.cancelBaseChange ..).symm ≪≫ₗ
    AlgebraTensorModule.congr (.refl ..) ((isLocalizedModule_iff_isBaseChange p S f).mp ‹_›).equiv

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.symm, isLocalizedModule_iff_isBaseChange, LinearEquiv.lift_rank_eq, TensorProduct.AlgebraTensorModule.congr, Iff.mp, LinearEquiv.refl, LinearEquiv.trans, IsBaseChange.equiv
-- 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
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 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:
exact LinearEquiv.lift_rank_eq <| AlgebraTensorModule.congr (.refl ST ST) bc.equiv.symm ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange .. ≪≫ₗ (AlgebraTensorModule.cancelBaseChange ..).symm ≪≫ₗ
    AlgebraTensorModule.congr (.refl ..) ((isLocalizedModule_iff_isBaseChange p S f).mp ‹_›).equiv

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.symm, isLocalizedModule_iff_isBaseChange, LinearEquiv.lift_rank_eq, TensorProduct.AlgebraTensorModule.congr, Iff.mp, LinearEquiv.refl, IsBaseChange.equiv
-- 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 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
⊢ finrank T P = finrank R M

Tactic:
simpa using congr_arg toNat (lift_rank_eq_of_le_nonZeroDivisors S f hp hpT bc)

Premises used: Cardinal.toNat, congr_arg, DFunLike.coe, IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors