awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
t : R
ht : (↑s₀ : R) * (↑s₁ : R) * (↑s₂ : R) ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
  (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N) :=
  (LocalizedModule.map (Submonoid.powers t) :
      (a : M →ₗ[R] N) →
        LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
          LocalizedModule (Submonoid.powers t) N)
    l
hu :
  IsUnit (M := Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x) t ⋯) : R) :
      Rₛ)
hu₀ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₀ : R) : Rₛ)
⊢ Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
    (⇑((LocalizedModule.map (Submonoid.powers t) :
              (a : M →ₗ[R] N) →
                LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                  LocalizedModule (Submonoid.powers t) N)
            l :
          LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
            (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
      (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)
have hu₁ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₁ : R) : Rₛ)
Tactic: have hu₁ : IsUnit (algebraMap R Rₛ s₁) := isUnit_of_dvd_unit
      (map_dvd (algebraMap R Rₛ) (dvd_trans ⟨s₀ * s₂, by ring⟩ ht)) hu
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
t : R
ht : (↑s₀ : R) * (↑s₁ : R) * (↑s₂ : R) ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
  (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N) :=
  (LocalizedModule.map (Submonoid.powers t) :
      (a : M →ₗ[R] N) →
        LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
          LocalizedModule (Submonoid.powers t) N)
    l
hu :
  IsUnit (M := Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x) t ⋯) : R) :
      Rₛ)
hu₀ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₀ : R) : Rₛ)
hu₁ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₁ : R) : Rₛ)
⊢ Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
    (⇑((LocalizedModule.map (Submonoid.powers t) :
              (a : M →ₗ[R] N) →
                LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                  LocalizedModule (Submonoid.powers t) N)
            l :
          LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
            (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
      (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)
have hu₂ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₂ : R) : Rₛ)
Tactic: have hu₂ : IsUnit (algebraMap R Rₛ s₂) := isUnit_of_dvd_unit
      (map_dvd (algebraMap R Rₛ) (dvd_trans ⟨s₀ * s₁, by ring⟩ ht)) hu
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_5
M : Type u_6
N : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R M
inst_6 : FinitePresentation R N
f : M →ₗ[R] N
p : Ideal R
inst_7 : p.IsPrime
Mₚ : Type u_3
Nₚ : Type u_4
inst_8 : AddCommGroup Mₚ
inst_9 : AddCommGroup Nₚ
inst_10 : Module R Mₚ
inst_11 : Module R Nₚ
fM : M →ₗ[R] Mₚ
fN : N →ₗ[R] Nₚ
inst_12 : IsLocalizedModule p.primeCompl fM
inst_13 : IsLocalizedModule p.primeCompl fN
hf :
  Function.Bijective.{u_3 + 1, u_4 + 1} (α := Mₚ) (β := Nₚ)
    (⇑((IsLocalizedModule.map p.primeCompl fM fN : (a : M →ₗ[R] N) → Mₚ →ₗ[R] Nₚ) f : Mₚ →ₗ[R] Nₚ) : (a : Mₚ) → Nₚ)
⊢ ∃ g ∉ p,
    Function.Bijective (α := LocalizedModule (Submonoid.powers g) M) (β := LocalizedModule (Submonoid.powers g) N)
      (⇑((LocalizedModule.map (Submonoid.powers g) :
                (a : M →ₗ[R] N) →
                  LocalizedModule (Submonoid.powers g) M →ₗ[Localization (Submonoid.powers g)]
                    LocalizedModule (Submonoid.powers g) N)
              f :
            LinearMap (R := Localization (Submonoid.powers g)) (RingHom.id (Localization (Submonoid.powers g)))
              (LocalizedModule (Submonoid.powers g) M) (LocalizedModule (Submonoid.powers g) N)) :
        (a : LocalizedModule (Submonoid.powers g) M) → LocalizedModule (Submonoid.powers g) N)
have obtain : ∀ (g : R) (hg : g ∈ p.primeCompl)
  (h :
    ∀ (t : R),
      g ∣ t →
        Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
          (⇑((LocalizedModule.map (Submonoid.powers t) :
                    (a : M →ₗ[R] N) →
                      LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                        LocalizedModule (Submonoid.powers t) N)
                  f :
                LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                  (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
            (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)),
  ∃ g ∉ p,
    Function.Bijective (α := LocalizedModule (Submonoid.powers g) M) (β := LocalizedModule (Submonoid.powers g) N)
      (⇑((LocalizedModule.map (Submonoid.powers g) :
                (a : M →ₗ[R] N) →
                  LocalizedModule (Submonoid.powers g) M →ₗ[Localization (Submonoid.powers g)]
                    LocalizedModule (Submonoid.powers g) N)
              f :
            LinearMap (R := Localization (Submonoid.powers g)) (RingHom.id (Localization (Submonoid.powers g)))
              (LocalizedModule (Submonoid.powers g) M) (LocalizedModule (Submonoid.powers g) N)) :
        (a : LocalizedModule (Submonoid.powers g) M) → LocalizedModule (Submonoid.powers g) N)
Tactic: obtain ⟨g, hg, h⟩ := exists_bijective_map_powers p.primeCompl fM fN f hf
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
⊢ ∃ (r : R) (hr : r ∈ S) (l' : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N),
    LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ
        (↑R :
            {S : Type u_3} →
              {M : Type (max u_3 u_4)} →
                {M₂ : Type (max u_3 u_5)} →
                  [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₂)
          (↑l' : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N) =
      (↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
have obtain : ∀ (l' : M →ₗ[R] N) (s : ↥S) (H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f),
  ∃ (r : R) (hr : r ∈ S) (l' : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N),
    LocalizedModule.lift (Submonoid.powers r) g sorry ∘ₗ
        (↑R :
            {S : Type u_3} →
              {M : Type (max u_3 u_4)} →
                {M₂ : Type (max u_3 u_5)} →
                  [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₂)
          (↑l' : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N) =
      (↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers r) f sorry
Tactic: obtain ⟨l', s, H⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (l ∘ₗ f)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
⊢ (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')
have h : (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f =
  (HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f
Tactic: apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
⊢ (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f =
    (HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f
have apply : ∀ (x : M),
  Eq.{u_2 + 1} (α := N') (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f : (a : M) → N') x : N')
    (((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f : (a : M) → N') x : N')
Tactic: apply LinearMap.ext fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
x : M
⊢ Eq.{u_2 + 1} (α := N') (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' ∘ₗ f : (a : M) → N') x : N')
    (((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) ∘ₗ f : (a : M) → N') x : N')
have simp : Eq.{u_2 + 1} (α := N') ((g : (a : N) → N') ((l' : (a : M) → N) x : N) : N')
  ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
      (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
    N')
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
x : M
⊢ Eq.{u_2 + 1} (α := N') ((g : (a : N) → N') ((l' : (a : M) → N) x : N) : N')
    ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
        (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
      N')
have rw : Eq.{u_2 + 1} (α := N') ((s • (↑l : M' →ₗ[R] N') ∘ₗ f : (a : M) → N') x : N')
  ((HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id : (a : N') → N')
      (((↑l : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N') :
    N')
Tactic: rw [← LinearMap.comp_apply, H]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' : M' →ₗ[R] N') : (a : M') → N')
have this : (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')
Tactic: have : IsLocalizedModule.map S f g l' = (s • LinearMap.id) ∘ₗ l := by
      apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
      apply LinearMap.ext fun x ↦ ?_
      simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]
      rw [← LinearMap.comp_apply, H]
      simp
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
this :
  (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' = HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' : M' →ₗ[R] N') : (a : M') → N')
have rw : Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
  (⇑(HSMul.hSMul (β := N' →ₗ[R] N') s LinearMap.id ∘ₗ (↑l : M' →ₗ[R] N')) : (a : M') → N')
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
⊢ ∃ (r : R) (hr : r ∈ S) (l' : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N),
    LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ
        (↑R :
            {S : Type u_3} →
              {M : Type (max u_3 u_4)} →
                {M₂ : Type (max u_3 u_5)} →
                  [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₂)
          (↑l' : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N) =
      (↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
have this : Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
  (⇑((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' : M' →ₗ[R] N') : (a : M') → N')
Tactic: have : Function.Bijective (IsLocalizedModule.map S f g l') := by
    have : IsLocalizedModule.map S f g l' = (s • LinearMap.id) ∘ₗ l := by
      apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
      apply LinearMap.ext fun x ↦ ?_
      simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]
      rw [← LinearMap.comp_apply, H]
      simp
    rw [this]
    exact ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).comp l.bijective
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
this :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' : M' →ₗ[R] N') : (a : M') → N')
r : R
hr : r ∈ S
hr' :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] N) →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) N)
                l' :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)
rs : Submonoid R := Submonoid.powers (r * (↑s : R))
Rᵣₛ : Type u_3 := Localization (M := R) rs
⊢ ∃ (r : R) (hr : r ∈ S) (l' : LocalizedModule.Away r M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N),
    LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ
        (↑R :
            {S : Type u_3} →
              {M : Type (max u_3 u_4)} →
                {M₂ : Type (max u_3 u_5)} →
                  [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₂)
          (↑l' : LocalizedModule.Away r M →ₗ[Localization (Submonoid.powers r)] LocalizedModule.Away r N) =
      (↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
have hsu : IsUnit (M := Rᵣₛ) ((algebraMap R Rᵣₛ : (a : R) → Rᵣₛ) (↑s : R) : Rᵣₛ)
Tactic: have hsu : IsUnit (algebraMap R Rᵣₛ s) := isUnit_of_dvd_unit
      (hu := IsLocalization.map_units (M := rs) Rᵣₛ ⟨_, Submonoid.mem_powers _⟩)
      (map_dvd (algebraMap R Rᵣₛ) ⟨r, mul_comm _ _⟩)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
⊢ IsLocalizedModule S (IsLocalizedModule.map S f g)
have map_units : ∀ (x : ↥S),
  IsUnit (M := End R (M' →ₗ[R] N'))
    ((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑x : R) : End R (M' →ₗ[R] N'))
Tactic: constructor