awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : LinearMap.{u, u, v', v} (RingHom.id K) (↥f.range) V
hg : f.rangeRestrict ∘ₗ g = id
fg :
  LeftInverse.{v' + 1, v + 1} (α := ↥f.range) (β := V) (⇑f.rangeRestrict : (a : V) → ↥f.range) (⇑g : (a : ↥f.range) → V)
s : Set V
hsc : lift.{v', v} #(↑s : Type v) = lift.{v, v'} c
si : LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
this : LinearIndepOn.{v, u, v'} K (M := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
⊢ c = #(↑((⇑f.rangeRestrict : (a : V) → ↥f.range) '' s) : Type v')
have h : InjOn.{v, v'} (β := ↥f.range) (⇑f.rangeRestrict : (a : V) → ↥f.range) s
Tactic: rw [← Cardinal.lift_inj, ← hsc, Cardinal.mk_image_eq_of_injOn_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (↑n : Cardinal.{v'}) ≤ f.rank ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
have simp : (∃ (s : Set V),
    (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) ↔
  ∃ (s : Finset V),
    s.card = n ∧
      LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
Tactic: simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
    Cardinal.mk_set_eq_nat_iff_finset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
have mp : (∃ (s : Set V),
    (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) →
  ∃ (s : Finset V),
    s.card = n ∧
      LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.LinearMap (goal)
Goal:
K : Type u
V : Type v
V' : Type v'
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V'
inst_4 : Module K V'
n : ℕ
f : V →ₗ[K] V'
mp :
  (∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) →
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
⊢ (∃ (s : Set V),
      (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s) ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)
have mpr : (∃ (s : Finset V),
    s.card = n ∧
      LinearIndependent.{v, u, v'} K (M := V') fun (x : (↑(↑s : Set V) : Type v)) ↦ (f : (a : V) → V') (↑x : V)) →
  ∃ (s : Set V),
    (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn.{v, u, v'} K (M := V') (⇑f : (a : V) → V') s
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
have inl : Subsingleton R → Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, 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
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
inl : Subsingleton R → Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
have inr : Nontrivial R → Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, 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
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
have inr : Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
inr : Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) = Cardinal.lift.{uN, uM} (Module.rank R M)
have inr₁ : Cardinal.lift.{uN, uM} (Module.rank R M) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
⊢ Cardinal.lift.{uM, uN} (Module.rank R N) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)
have inr : ⨆ (i : { s : Set N // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #(↑(↑i : Set N) : Type uN) ≤
  Cardinal.lift.{uN, uM} (Module.rank R M)
Tactic: rw [Module.rank_def, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
⊢ Cardinal.lift.{uN, uM} (Module.rank R M) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
have inr : ⨆ (i : { s : Set M // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #(↑(↑i : Set M) : Type uM) ≤
  Cardinal.lift.{uM, uN} (Module.rank R N)
Tactic: rw [Module.rank_def, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
⊢ ⨆ (i : { s : Set N // LinearIndepOn R id s }), Cardinal.lift.{uM, uN} #(↑(↑i : Set N) : Type uN) ≤
    Cardinal.lift.{uN, uM} (Module.rank R M)
have inr : ∀ (i : { s : Set N // LinearIndepOn R id s }),
  Cardinal.lift.{uM, uN} #(↑(↑i : Set N) : Type uN) ≤ Cardinal.lift.{uN, uM} (Module.rank R M)
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
hp : p ≤ R⁰
h : Nontrivial R
⊢ ⨆ (i : { s : Set M // LinearIndepOn R id s }), Cardinal.lift.{uN, uM} #(↑(↑i : Set M) : Type uM) ≤
    Cardinal.lift.{uM, uN} (Module.rank R N)
have inr : ∀ (i : { s : Set M // LinearIndepOn R id s }),
  Cardinal.lift.{uN, uM} #(↑(↑i : Set M) : Type uM) ≤ Cardinal.lift.{uM, uN} (Module.rank R N)
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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⁰
⊢ Module.rank S N = Module.rank R N
have inl : Subsingleton R → Module.rank S N = Module.rank R N
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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⁰
inl : Subsingleton R → Module.rank S N = Module.rank R N
⊢ Module.rank S N = Module.rank R N
have inr : Nontrivial R → Module.rank S N = Module.rank R N
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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 : Subsingleton R
⊢ Module.rank S N = Module.rank R N
have this : Subsingleton S
Tactic: have := (algebraMap R S).codomain_trivial
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ Module.rank S N = Module.rank R N
have inj : Function.Injective.{uR + 1, uS + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Tactic: have inj := IsLocalization.injective S hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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)
⊢ Module.rank S N = Module.rank R N
have inr : Module.rank S N ≤ Module.rank R N
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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 : Module.rank S N ≤ Module.rank R N
⊢ Module.rank S N = Module.rank R N
have inr₁ : Module.rank R N ≤ Module.rank S N
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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)
⊢ Module.rank S N ≤ Module.rank R N
have inr : ⨆ (ι : { s : Set N // LinearIndepOn S id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank R N
Tactic: rw [Module.rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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 // LinearIndepOn S id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank R N
have inr : ∀ (i : { s : Set N // LinearIndepOn S id s }), #(↑(↑i : Set N) : Type uN) ≤ Module.rank R N
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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)
⊢ Module.rank R N ≤ Module.rank S N
have inr : ⨆ (ι : { s : Set N // LinearIndepOn R id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank S N
Tactic: rw [Module.rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (goal)
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 // LinearIndepOn R id s }), #(↑(↑ι : Set N) : Type uN) ≤ Module.rank S N
have inr : ∀ (i : { s : Set N // LinearIndepOn R id s }), #(↑(↑i : Set N) : Type uN) ≤ Module.rank S N
Tactic: apply ciSup_le'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn S id s) s hs) : Set N) : Type uN) ≤ Module.rank R N
have this : FaithfulSMul R S
Tactic: have := (faithfulSMul_iff_algebraMap_injective R S).mpr inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Localization (hypothesis)
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
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set N) ↦ LinearIndepOn R id s) s hs) : Set N) : Type uN) ≤ Module.rank S N
have this : Nontrivial S
Tactic: have := inj.nontrivial
-- 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
⊢ ∃ (s : Set M), #(↑s : Type uM) = Module.rank R M ∧ LinearIndepOn R id s
have 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
Tactic: obtain ⟨w, hw⟩ :=
    IsLocalizedModule.linearIndependent_lift R⁰ (LocalizedModule.mkLinearMap R⁰ M) <|
      Module.Free.chooseBasis (FractionRing R) (LocalizedModule R⁰ M)
        |>.linearIndependent.restrict_scalars' _
-- 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
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
have refine : #(↑(Set.range w) : Type uM) = Module.rank R M
Tactic: refine ⟨Set.range w, ?_, (linearIndepOn_id_range_iff hw.injective).mpr hw⟩
-- 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
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M
hw : LinearIndependent R w
⊢ #(↑(Set.range w) : Type uM) = Module.rank R M
have a : lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)
Tactic: apply Cardinal.lift_injective.{max uR uM}
-- 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
w : Free.ChooseBasisIndex (FractionRing R) (LocalizedModule.{uR, uM} (R := R) R⁰ M) → M
hw : LinearIndependent R w
⊢ lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)
have 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)
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]
-- 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
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)
⊢ lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)
have 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)
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]
-- 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
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)
⊢ lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)
have 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)
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]
-- 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
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)
⊢ lift.{max uR uM, uM} #(↑(Set.range w) : Type uM) = lift.{max uR uM, uM} (Module.rank R M)
have a₃ : lift.{max uM uR, uM} (Module.rank R M) = 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]
-- 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
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M
have a : lift.{max uR uM, uM} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max uR uM, uM} (Module.rank R M)
Tactic: apply lift_injective.{max uR uM}
-- 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
⊢ 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.{max uM uR, uM} (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]
-- 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)
⊢ 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.{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]