awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_surj : Function.Surjective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : N
s : ↥S
⊢ ∃ (a : M'),
    (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a = Function.uncurry (mk' g) (x, s)
have obtain : ∀ (x : M),
  ∃ (a : M'),
    (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a =
      Function.uncurry (β := ↥S) (mk' g) ((h : (a : M) → N) x, s)
Tactic: obtain ⟨x, rfl⟩ := h_surj x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ Eq (α := LocalizedModule S M ≃ₗ[R] LocalizedModule S M) (iso S (mkLinearMap S M))
    (LinearEquiv.refl R (LocalizedModule S M))
have obtain : ∀ (e : LocalizedModule S M →ₗ[R] LocalizedModule S M),
  e ∘ₗ f = f →
    ∀
      (univ :
        ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M),
          (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f) y → y = e),
      Eq (α := LocalizedModule S M ≃ₗ[R] LocalizedModule S M) (iso S (mkLinearMap S M))
        (LinearEquiv.refl R (LocalizedModule S M))
Tactic: obtain ⟨e, _, univ⟩ := is_universal S f f (map_units f)
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left : e ∘ₗ f = f
univ :
  ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M),
    (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f) y → y = e
⊢ Eq (α := LocalizedModule S M ≃ₗ[R] LocalizedModule S M) (iso S (mkLinearMap S M))
    (LinearEquiv.refl R (LocalizedModule S M))
have rw : e = (↑(LinearEquiv.refl R (LocalizedModule S M)) : LocalizedModule S M →ₗ[R] LocalizedModule S M)
Tactic: rw [← toLinearMap_inj, univ (iso S f) ((eq_toLinearMap_symm_comp f f).1 (iso_symm_comp S f).symm)]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_7
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ Eq (α := LocalizedModule S M₁)
    ((((map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
          (a : LocalizedModule S M₀) → LocalizedModule S M₁)
        (LocalizedModule.mk m s) :
      LocalizedModule S M₁)
    (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s : LocalizedModule S M₁)
have this : Eq (α := LocalizedModule S M₁)
  (((↑(IsUnit.unit sorry)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
      ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
    LocalizedModule S M₁)
  ((iso S (mkLinearMap S M₁) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
      (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s) :
    LocalizedModule S M₁)
Tactic: have := (iso_apply_mk S (mkLinearMap S M₁) (g m) s).symm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_7
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this :
  Eq (α := LocalizedModule S M₁)
    (((↑(IsUnit.unit ⋯)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
      LocalizedModule S M₁)
    ((iso S (mkLinearMap S M₁) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₁)
⊢ Eq (α := LocalizedModule S M₁)
    ((((map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
          (a : LocalizedModule S M₀) → LocalizedModule S M₁)
        (LocalizedModule.mk m s) :
      LocalizedModule S M₁)
    (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s : LocalizedModule S M₁)
have this₁ : Eq (α := LocalizedModule S M₁)
  (((↑(IsUnit.unit sorry)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
      ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
    LocalizedModule S M₁)
  (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s : LocalizedModule S M₁)
Tactic: rw [iso_localizedModule_eq_refl, refl_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
⊢ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') =
    (↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
      (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
          (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
        g
have h : ∀ (x : LocalizedModule S M₀),
  Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        x :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        x :
      M₁')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
⊢ Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        x :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        x :
      M₁')
have h : ∀ (m : M₀) (s : ↥S),
  Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')
Tactic: induction x using induction_on with | _ m s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')
have h : Eq.{u_8 + 1} (α := M₁')
  ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
      (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
            (a : LocalizedModule S M₀) → M₁')
          (LocalizedModule.mk m s) :
        M₁') :
    M₁')
  ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
      (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
              (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
            (a : LocalizedModule S M₀) → M₁')
          (LocalizedModule.mk m s) :
        M₁') :
    M₁')
Tactic: refine ((Module.End.isUnit_iff _).1 (map_units f₁ s)).1 ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ Eq.{u_8 + 1} (α := M₁')
    ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
        (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
              (a : LocalizedModule S M₀) → M₁')
            (LocalizedModule.mk m s) :
          M₁') :
      M₁')
    ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
        (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
                (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                    (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                  g :
              (a : LocalizedModule S M₀) → M₁')
            (LocalizedModule.mk m s) :
          M₁') :
      M₁')
have h : Eq.{u_8 + 1} (α := M₁')
  (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
        (a : LocalizedModule S M₀) → M₁')
      (LocalizedModule.mk m 1) :
    M₁')
  (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
          (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
              (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
            g :
        (a : LocalizedModule S M₀) → M₁')
      (LocalizedModule.mk m 1) :
    M₁')
Tactic: rw [Module.algebraMap_end_apply, Module.algebraMap_end_apply,
    ← CompatibleSMul.map_smul, ← CompatibleSMul.map_smul, smul'_mk, ← mk_smul _ s.2, mk_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : AddCommMonoid M₂'
inst_13 : Module R M₂
inst_14 : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst_15 : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
⊢ Eq (α := M₀' →ₗ[R] M₂') ((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂')
    ((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
      M₀' →ₗ[R] M₂')
have h₁ : ∀ (x : M₀'),
  Eq.{u_10 + 1} (α := M₂')
    ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂') x : M₂')
    (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
          (a : M₀') → M₂')
        x :
      M₂')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst_1 : AddCommMonoid M₀
inst_2 : AddCommMonoid M₀'
inst_3 : Module R M₀
inst_4 : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst_5 : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : AddCommMonoid M₂'
inst_13 : Module R M₂
inst_14 : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst_15 : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀'
⊢ Eq.{u_10 + 1} (α := M₂')
    ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂') x : M₂')
    (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
          (a : M₀') → M₂')
        x :
      M₂')
have h₁ : ∀ (x : M₀) (s : ↥S),
  Eq.{u_10 + 1} (α := M₂')
    ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂')
        (Function.uncurry (mk' f₀) (x, s)) :
      M₂')
    (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
          (a : M₀') → M₂')
        (Function.uncurry (mk' f₀) (x, s)) :
      M₂')
Tactic: obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f₀ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') → ∃ (m : ↥M), m • x = 0
x : S
h : ∃ (m : ↥M), m • x = 0
m : R
hm : m ∈ M
e : Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm • x = 0
⊢ HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') ((f : (a : S) → S') x : S') =
    HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') (0 : S')
have rw : HSMul.hSMul (β := S') m ((f : (a : S) → S') x : S') =
  HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') (0 : S')
Tactic: rw [← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') → ∃ (m : ↥M), m • x = 0
⊢ IsLocalizedModule M f.toLinearMap
have h₄ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
Tactic: replace h₃ := fun x =>
    Iff.intro (h₃ x) fun ⟨⟨m, hm⟩, e⟩ =>
      (h₁ m hm).mul_left_cancel <| by
        rw [← Algebra.smul_def]
        simpa [Submonoid.smul_def] using f.congr_arg e
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
⊢ IsLocalizedModule M f.toLinearMap
have map_units : ∀ (x : ↥M), IsUnit.{u_8} (M := End R S') ((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
map_units :
  ∀ (x : ↥M), IsUnit.{u_8} (M := End R S') ((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S')
⊢ IsLocalizedModule M f.toLinearMap
have surj : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f.toLinearMap : (a : S) → S') x.1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
map_units :
  ∀ (x : ↥M), IsUnit.{u_8} (M := End R S') ((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S')
surj : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f.toLinearMap : (a : S) → S') x.1
⊢ IsLocalizedModule M f.toLinearMap
have exists_of_eq : ∀ {x₁ x₂ : S},
  Eq.{u_8 + 1} (α := S') ((f.toLinearMap : (a : S) → S') x₁ : S') ((f.toLinearMap : (a : S) → S') x₂ : S') →
    ∃ (c : ↥M), c • x₁ = c • x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
⊢ IsUnit.{u_8} (M := End R S') ((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S')
have map_units : Function.Bijective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
  (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
Tactic: rw [Module.End.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
⊢ Function.Bijective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
have map_units : Function.Injective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
  (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
map_units :
  Function.Injective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
⊢ Function.Bijective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
have map_units₁ : Function.Surjective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
  (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a b : S'
e : x • a = x • b
⊢ a = b
have e₁ : HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') a =
  HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') b
Tactic: simp_rw [Submonoid.smul_def, Algebra.smul_def] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a : S'
⊢ ∃ (a_1 : S'), (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') a_1 = a
have map_units : (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑sorry.unit⁻¹ : S') * a) = a
Tactic: refine ⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩