awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Free
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'
⊢ FinitePresentation R (I →₀ R)

Tactic:
have : Module.FinitePresentation R (I →₀ R) := Module.finitePresentation_of_projective _ _
-- Module: Mathlib.RingTheory.Localization.Free
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)
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ₛ)) ⋯ ∘ₗ
          (↑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 ⋯)),
    ∃ (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')
⊢ ∃ (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')

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)

Premises used: LinearEquiv.restrictScalars, Algebra.linearMap, Module.Basis.repr, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, Finsupp.mapRange.linearMap
-- Module: Mathlib.RingTheory.Localization.Free
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')

Tactic:
⟨r, hr, .ofRepr (e ≪≫ₗ ?_), ?_⟩

Premises used: Module.Basis.ofRepr, Exists.intro, LinearEquiv.trans
-- Module: Mathlib.RingTheory.Localization.Free
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))))
⊢ LocalizedModule.Away r (I →₀ R) ≃ₗ[Localization (Submonoid.powers r)]
    Finsupp.{u_6, u_4} I (Localization (Submonoid.powers r))

Tactic:
exact
    { __ := e',
      toLinearMap := e'.extendScalarsOfIsLocalization (.powers r) (Localization (.powers r)) }
-- Module: Mathlib.RingTheory.Localization.Free
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))))
i : I
⊢ Eq (α := LocalizedModule (Submonoid.powers r) (I →₀ R))
    ((e'.symm : (a : I →₀ Localization (Submonoid.powers r)) → LocalizedModule (Submonoid.powers r) (I →₀ R))
        ((Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (Submonoid.powers r))) :
            (a : I →₀ R) → I →₀ Localization (Submonoid.powers r))
          (Finsupp.single i 1)) :
      LocalizedModule (Submonoid.powers r) (I →₀ R))
    ((LocalizedModule.mkLinearMap (Submonoid.powers r) (I →₀ R) :
          (a : I →₀ R) → LocalizedModule (Submonoid.powers r) (I →₀ R))
        (Finsupp.single i 1) :
      LocalizedModule (Submonoid.powers r) (I →₀ R))

Tactic:
have : e'.symm _ = _ := LinearMap.congr_fun (IsLocalizedModule.iso_symm_comp (.powers r)
      (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (.powers r)))))
      (Finsupp.single i 1)
-- Module: Mathlib.RingTheory.Localization.Free
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ₛ)
refine_2 :
  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ₛ)
⊢ 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')

Tactic:
apply b.repr.injective

Premises used: Module.Basis.repr, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Localization.Free
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ₛ)
refine_2 :
  Eq (α := I →₀ Rₛ)
    (((↑(IsUnit.unit (a := (algebraMap R (End R (I →₀ Rₛ)) : (a : R) → End R (I →₀ Rₛ)) (↑1 : R)) ⋯)⁻¹ :
            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ₛ)
⊢ 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ₛ)

Tactic:
rw [← he, Basis.repr_self, this, LocalizedModule.lift_mk]

Premises used: LocalizedModule.lift_mk, Module.Basis.repr_self
-- Module: Mathlib.RingTheory.Localization.Free
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ₛ)
    (((↑(IsUnit.unit (a := (algebraMap R (End R (I →₀ Rₛ)) : (a : R) → End R (I →₀ Rₛ)) (↑1 : R)) ⋯)⁻¹ :
            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:
simp
-- Module: Mathlib.RingTheory.Localization.Free
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'
⊢ Module.Finite Rₛ M'

Tactic:
have : Module.Finite Rₛ M' := Module.Finite.of_isLocalizedModule S (Rₚ := Rₛ) f
-- Module: Mathlib.RingTheory.Localization.Free
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'
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 ⋯ : (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'
⊢ ∃ 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

Premises used: Module.FinitePresentation.exists_basis_localizedModule_powers
-- Module: Mathlib.RingTheory.Localization.Free
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')
⊢ 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
-- Module: Mathlib.RingTheory.Localization.Free
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'

Tactic:
⟨r, hr, .of_basis b', ?_⟩

Premises used: Module.Free.of_basis, And.intro, Exists.intro