awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K_1 : Type u_5
inst_5 : IsDomain A
k : Type u_6
K : Type u_7
inst_6 : Field k
inst_7 : Field K
inst_8 : Algebra A k
inst_9 : Algebra A K
inst_10 : Algebra k K
inst_11 : FaithfulSMul A k
inst_12 : FaithfulSMul A K
inst_13 : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x : A × ↥(A⁰ : Submonoid A)
a₁ : A
a₂ : ↥(A⁰ : Submonoid A)
simp_rw simp_rw₁ :
  (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk a₁ a₂) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk a₁ a₂) (b • c)
simp_rw₂ :
  (HSMul.hSMul (β := FractionRing A) (↑a₂ : A) (Localization.mk a₁ a₂) • b) • c =
    HSMul.hSMul (β := FractionRing A) (↑a₂ : A) (Localization.mk a₁ a₂) • b • c
simp_rw₃ :
  HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) • a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) • a₁) a₂) (b • c)
simp_rw₄ :
  HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) * a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) * a₁) a₂) (b • c)
simp_rw₅ :
  HSMul.hSMul (α := FractionRing A) (IsLocalization.mk' (Localization (M := A) A⁰) ((↑a₂ : A) * a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (IsLocalization.mk' (Localization (M := A) A⁰) ((↑a₂ : A) * a₁) a₂) (b • c)
⊢ (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)
have simp_rw₆ : HSMul.hSMul (α := FractionRing A)
      ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) a₁ : Localization (M := A) A⁰) b •
    c =
  HSMul.hSMul (α := FractionRing A)
    ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) a₁ : Localization (M := A) A⁰) (b • c)
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K_1 : Type u_5
inst_5 : IsDomain A
k : Type u_6
K : Type u_7
inst_6 : Field k
inst_7 : Field K
inst_8 : Algebra A k
inst_9 : Algebra A K
inst_10 : Algebra k K
inst_11 : FaithfulSMul A k
inst_12 : FaithfulSMul A K
inst_13 : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x : A × ↥(A⁰ : Submonoid A)
a₁ : A
a₂ : ↥(A⁰ : Submonoid A)
simp_rw simp_rw₁ :
  (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk a₁ a₂) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk a₁ a₂) (b • c)
simp_rw₂ :
  (HSMul.hSMul (β := FractionRing A) (↑a₂ : A) (Localization.mk a₁ a₂) • b) • c =
    HSMul.hSMul (β := FractionRing A) (↑a₂ : A) (Localization.mk a₁ a₂) • b • c
simp_rw₃ :
  HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) • a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) • a₁) a₂) (b • c)
simp_rw₄ :
  HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) * a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) * a₁) a₂) (b • c)
simp_rw₅ :
  HSMul.hSMul (α := FractionRing A) (IsLocalization.mk' (Localization (M := A) A⁰) ((↑a₂ : A) * a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (IsLocalization.mk' (Localization (M := A) A⁰) ((↑a₂ : A) * a₁) a₂) (b • c)
simp_rw₆ :
  HSMul.hSMul (α := FractionRing A)
        ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) a₁ : Localization (M := A) A⁰) b •
      c =
    HSMul.hSMul (α := FractionRing A)
      ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) a₁ : Localization (M := A) A⁰) (b • c)
⊢ (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)
have simp_rw₇ : (a₁ • b) • c = a₁ • b • c
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (hypothesis)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : IsLocalization S Rₛ
inst_11 : FinitePresentation R M
I : Type u_6
inst_12 : Finite I
b : Basis I Rₛ M'
⊢ ∃ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
    ∀ (i : I),
      Eq.{u_1 + 1} (α := M')
        ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
            ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
          M')
        ((b : (a : I) → M') i : M')
have this : FinitePresentation R (I →₀ R)
Tactic: have : Module.FinitePresentation R (I →₀ R) := Module.finitePresentation_of_projective _ _
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : IsLocalization S Rₛ
inst_11 : FinitePresentation R M
I : Type u_6
inst_12 : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
⊢ ∃ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
    ∀ (i : I),
      Eq.{u_1 + 1} (α := M')
        ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
            ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
          M')
        ((b : (a : I) → M') i : M')
have obtain : ∀ (r : R) (hr : r ∈ S)
  (e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R))
  (he :
    Eq (α := LocalizedModule (Submonoid.powers r) M →ₗ[R] I →₀ Rₛ)
      (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) sorry ∘ₗ
        (↑R :
            {S : Type u_4} →
              {M : Type (max u_4 u_5)} →
                {M₂ : Type (max u_4 u_6)} →
                  [inst : Semiring R] →
                    [inst_13 : Semiring S] →
                      [inst_14 : AddCommMonoid M] →
                        [inst_15 : AddCommMonoid M₂] →
                          [inst_16 : Module R M] →
                            [inst_17 : Module R M₂] →
                              [inst_18 : Module S M] →
                                [inst_19 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (↑e : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)))
      ((↑(LinearEquiv.restrictScalars R b.repr) : M' →ₗ[R] I →₀ Rₛ) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f sorry)),
  ∃ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
    ∀ (i : I),
      Eq.{u_1 + 1} (α := M')
        ((LocalizedModule.lift (Submonoid.powers r) f sorry : (a : LocalizedModule (Submonoid.powers r) M) → M')
            ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
          M')
        ((b : (a : I) → M') i : M')
Tactic: obtain ⟨r, hr, e, he⟩ := Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule S f
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (b.repr.restrictScalars R)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : IsLocalization S Rₛ
inst_11 : FinitePresentation R M
I : Type u_6
inst_12 : Finite I
b : Basis I Rₛ M'
this : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
he :
  Eq (α := LocalizedModule (Submonoid.powers r) M →ₗ[R] I →₀ Rₛ)
    (LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ ∘ₗ
      (↑R :
          {S : Type u_4} →
            {M : Type (max u_4 u_5)} →
              {M₂ : Type (max u_4 u_6)} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑e : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)))
    ((↑(LinearEquiv.restrictScalars R b.repr) : M' →ₗ[R] I →₀ Rₛ) ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r)) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
⊢ ∃ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
    ∀ (i : I),
      Eq.{u_1 + 1} (α := M')
        ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
            ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
          M')
        ((b : (a : I) → M') i : M')
have refine_1 : LocalizedModule.Away r (I →₀ R) ≃ₗ[Localization (Submonoid.powers r)]
  Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r))
Tactic: refine ⟨r, hr, .ofRepr (e ≪≫ₗ ?_), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : IsLocalization S Rₛ
inst_11 : FinitePresentation R M
I : Type u_6
inst_12 : Finite I
b : Basis I Rₛ M'
this_1 : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r)) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this :
  Eq (α := LocalizedModule (Submonoid.powers r) (I →₀ R))
    ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
        (Finsupp.single i 1) :
      LocalizedModule (Submonoid.powers r) (I →₀ R))
    (LocalizedModule.mk (Finsupp.single i 1) 1 : LocalizedModule (Submonoid.powers r) (I →₀ R))
he :
  Eq (α := I →₀ Rₛ)
    ((LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ :
          (a : LocalizedModule (Submonoid.powers r) (I →₀ R)) → I →₀ Rₛ)
        ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
          (Finsupp.single i 1)) :
      I →₀ Rₛ)
    ((b.repr : (a : M') → I →₀ Rₛ)
        ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((e.symm : (a : LocalizedModule.Away r (I →₀ R)) → LocalizedModule.Away r M)
              ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
                (Finsupp.single i 1)) :
            LocalizedModule.Away r M)) :
      I →₀ Rₛ)
⊢ Eq.{u_1 + 1} (α := M')
    ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
        ((e.symm : (a : LocalizedModule.Away r (I →₀ R)) → LocalizedModule.Away r M)
            ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
              (Finsupp.single i 1)) :
          LocalizedModule.Away r M) :
      M')
    ((b : (a : I) → M') i : M')
have refine_2 : Eq (α := I →₀ Rₛ)
  ((b.repr : (a : M') → I →₀ Rₛ)
      ((LocalizedModule.lift (Submonoid.powers r) f sorry : (a : LocalizedModule (Submonoid.powers r) M) → M')
        ((e.symm : (a : LocalizedModule.Away r (I →₀ R)) → LocalizedModule.Away r M)
            ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
              (Finsupp.single i 1)) :
          LocalizedModule.Away r M)) :
    I →₀ Rₛ)
  ((b.repr : (a : M') → I →₀ Rₛ) ((b : (a : I) → M') i) : I →₀ Rₛ)
Tactic: apply b.repr.injective
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : IsLocalization S Rₛ
inst_11 : FinitePresentation R M
I : Type u_6
inst_12 : Finite I
b : Basis I Rₛ M'
this_1 : FinitePresentation R (I →₀ R)
r : R
hr : r ∈ S
e : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r (I →₀ R)
e' : LocalizedModule (Submonoid.powers r) (I →₀ R) ≃ₗ[R] Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r)) :=
  IsLocalizedModule.iso (Submonoid.powers r)
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))))
i : I
this :
  Eq (α := LocalizedModule (Submonoid.powers r) (I →₀ R))
    ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
        (Finsupp.single i 1) :
      LocalizedModule (Submonoid.powers r) (I →₀ R))
    (LocalizedModule.mk (Finsupp.single i 1) 1 : LocalizedModule (Submonoid.powers r) (I →₀ R))
he :
  Eq (α := I →₀ Rₛ)
    ((LocalizedModule.lift (Submonoid.powers r) (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) ⋯ :
          (a : LocalizedModule (Submonoid.powers r) (I →₀ R)) → I →₀ Rₛ)
        ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
          (Finsupp.single i 1)) :
      I →₀ Rₛ)
    ((b.repr : (a : M') → I →₀ Rₛ)
        ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((e.symm : (a : LocalizedModule.Away r (I →₀ R)) → LocalizedModule.Away r M)
              ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
                (Finsupp.single i 1)) :
            LocalizedModule.Away r M)) :
      I →₀ Rₛ)
⊢ Eq (α := I →₀ Rₛ)
    ((b.repr : (a : M') → I →₀ Rₛ)
        ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((e.symm : (a : LocalizedModule.Away r (I →₀ R)) → LocalizedModule.Away r M)
              ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
                (Finsupp.single i 1)) :
            LocalizedModule.Away r M)) :
      I →₀ Rₛ)
    ((b.repr : (a : M') → I →₀ Rₛ) ((b : (a : I) → M') i) : I →₀ Rₛ)
have refine_2 : Eq (α := I →₀ Rₛ)
  (((↑(IsUnit.unit (a := (algebraMap R (End R (I →₀ Rₛ)) : (a : R) → End R (I →₀ Rₛ)) (↑1 : R)) sorry)⁻¹ :
          End R (I →₀ Rₛ)) :
        (a : I →₀ Rₛ) → I →₀ Rₛ)
      ((Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) : (a : I →₀ R) → I →₀ Rₛ) (Finsupp.single i 1)) :
    I →₀ Rₛ)
  (Finsupp.single i 1 : I →₀ Rₛ)
Tactic: rw [← he, Basis.repr_self, this, LocalizedModule.lift_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (hypothesis)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : Nontrivial Rₛ
inst_11 : IsLocalization S Rₛ
inst_12 : FinitePresentation R M
inst_13 : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
have this : Module.Finite Rₛ M'
Tactic: have : Module.Finite Rₛ M' := Module.Finite.of_isLocalizedModule S (Rₚ := Rₛ) f
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : Nontrivial Rₛ
inst_11 : IsLocalization S Rₛ
inst_12 : FinitePresentation R M
inst_13 : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this : Module.Finite Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
have obtain : ∀ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)),
  (∀ (i : I),
      Eq.{u_1 + 1} (α := M')
        ((LocalizedModule.lift (Submonoid.powers r) f sorry : (a : LocalizedModule (Submonoid.powers r) M) → M')
            ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
          M')
        ((b : (a : I) → M') i : M')) →
    ∃ r ∈ S,
      Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
        finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
Tactic: obtain ⟨r, hr, b', _⟩ := Module.FinitePresentation.exists_basis_localizedModule_powers S f Rₛ b
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (hypothesis)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : Nontrivial Rₛ
inst_11 : IsLocalization S Rₛ
inst_12 : FinitePresentation R M
inst_13 : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
h :
  ∀ (i : I),
    Eq.{u_1 + 1} (α := M')
      ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
        M')
      ((b : (a : I) → M') i : M')
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
have this₁ : Nontrivial.{u_4} (Localization (Submonoid.powers r))
Tactic: have := (show Localization (.powers r) →+* Rₛ from IsLocalization.map (M := .powers r) (T := S) _
    (RingHom.id _) (Submonoid.powers_le.mpr hr)).domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : Nontrivial Rₛ
inst_11 : IsLocalization S Rₛ
inst_12 : FinitePresentation R M
inst_13 : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this_1 : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
h :
  ∀ (i : I),
    Eq.{u_1 + 1} (α := M')
      ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
        M')
      ((b : (a : I) → M') i : M')
this : Nontrivial.{u_4} (Localization (Submonoid.powers r))
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
have refine : finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
Tactic: refine ⟨r, hr, .of_basis b', ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Free (goal)
Goal:
R : Type u_4
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
Rₛ : Type u_3
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
inst_8 : Module Rₛ M'
inst_9 : IsScalarTower R Rₛ M'
inst_10 : Nontrivial Rₛ
inst_11 : IsLocalization S Rₛ
inst_12 : FinitePresentation R M
inst_13 : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this_1 : Module.Finite Rₛ M'
r : R
hr : r ∈ S
b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)
h :
  ∀ (i : I),
    Eq.{u_1 + 1} (α := M')
      ((LocalizedModule.lift (Submonoid.powers r) f ⋯ : (a : LocalizedModule (Submonoid.powers r) M) → M')
          ((b' : (a : I) → LocalizedModule.Away r M) i : LocalizedModule.Away r M) :
        M')
      ((b : (a : I) → M') i : M')
this : Nontrivial.{u_4} (Localization (Submonoid.powers r))
⊢ finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
have rw : finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = Nat.card I
Tactic: rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b']