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
r : R
m : M
s : ↥S
rw :
  (fromLocalizedModule S f : (a : LocalizedModule S M) → M')
      (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk m s)) =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (r • m) s) =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
have rw₁ : HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M') =
  HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
Tactic: rw [← LocalizedModule.smul'_mk, map_smul]
-- 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
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)
have delta : HAdd.hAdd (α := M') (β := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') =
  (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))
Tactic: delta mk'
-- 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
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ HAdd.hAdd (α := M') (β := M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') =
    (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))
have rw : Eq.{u_3 + 1} (α := M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M')
      (HAdd.hAdd (α := LocalizedModule S M) (LocalizedModule.mk m₁ s₁) (LocalizedModule.mk m₂ s₂)) :
    M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
Tactic: rw [← map_add, LocalizedModule.mk_add_mk]
-- 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
m₁ m₂ : M
s₁ s₂ : ↥S
rw :
  Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M')
        (HAdd.hAdd (α := LocalizedModule S M) (LocalizedModule.mk m₁ s₁) (LocalizedModule.mk m₂ s₂)) :
      M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
⊢ HAdd.hAdd (α := M') (β := M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') =
    (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))
have rw₁ : Eq.{u_3 + 1} (α := M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
Tactic: rw [← map_add, LocalizedModule.mk_add_mk]
-- 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
s : ↥S
⊢ mk' f 0 s = 0
have rw : mk' f (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 0 0) s = 0
Tactic: rw [← zero_smul R (0 : M), mk'_smul, zero_smul]
-- 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
s : ↥S
rw : mk' f (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 0 0) s = 0
⊢ mk' f 0 s = 0
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (mk' f 0 s) = 0
Tactic: rw [← zero_smul R (0 : M), mk'_smul, zero_smul]
-- 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
s : ↥S
rw : mk' f (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 0 0) s = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (mk' f 0 s) = 0
⊢ mk' f 0 s = 0
have rw₂ : Eq.{u_3 + 1} (α := M') 0 0
Tactic: rw [← zero_smul R (0 : M), mk'_smul, zero_smul]
-- 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
m : M
⊢ mk' (S := S) f m 1 = (f : (a : M) → M') m
have delta : Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
  ((f : (a : M) → M') m : M')
Tactic: delta mk'
-- 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
m : M
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
have rw : Eq (α := M')
  (((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) sorry)⁻¹ : End R M') : (a : M') → M')
      ((f : (a : M) → M') m : M') :
    M')
  ((f : (a : M) → M') m : M')
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
    one_smul]
-- 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
m : M
rw :
  Eq (α := M')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
        ((f : (a : M) → M') m : M') :
      M')
    ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
have rw₁ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') (↑1 : R) ((f : (a : M) → M') m : M')
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
    one_smul]
-- 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
m : M
rw :
  Eq (α := M')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
        ((f : (a : M) → M') m : M') :
      M')
    ((f : (a : M) → M') m : M')
rw₁ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') (↑1 : R) ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
have rw₂ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') 1 ((f : (a : M) → M') m : M')
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
    one_smul]
-- 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
m : M
rw :
  Eq (α := M')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
        ((f : (a : M) → M') m : M') :
      M')
    ((f : (a : M) → M') m : M')
rw₁ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') (↑1 : R) ((f : (a : M) → M') m : M')
rw₂ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') 1 ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
have rw₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') ((f : (a : M) → M') m : M')
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
    one_smul]
-- 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
m : M
s : ↥S
⊢ mk' f (s • m) s = (f : (a : M) → M') m
have delta : Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
  ((f : (a : M) → M') m : M')
Tactic: delta mk'
-- 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
m : M
s : ↥S
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw : Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
  ((f : (a : M) → M') m : M')
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw₂ : ((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) sorry)⁻¹ : End R M') : (a : M') → M')
    ((f : (a : M) → M') m : M') =
  mk' (S := S) f m 1
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
rw₂ :
  ((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
      ((f : (a : M) → M') m : M') =
    mk' (S := S) f m 1
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw₃ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑1 : R) (mk' (S := S) f m 1)
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
rw₂ :
  ((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
      ((f : (a : M) → M') m : M') =
    mk' (S := S) f m 1
rw₃ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑1 : R) (mk' (S := S) f m 1)
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw₄ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (mk' (S := S) f m 1)
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
rw₂ :
  ((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
      ((f : (a : M) → M') m : M') =
    mk' (S := S) f m 1
rw₃ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑1 : R) (mk' (S := S) f m 1)
rw₄ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (mk' (S := S) f m 1)
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw₅ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') 1 ((f : (a : M) → M') m : M')
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
rw₂ :
  ((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
      ((f : (a : M) → M') m : M') =
    mk' (S := S) f m 1
rw₃ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑1 : R) (mk' (S := S) f m 1)
rw₄ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (mk' (S := S) f m 1)
rw₅ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') 1 ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
have rw₆ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') ((f : (a : M) → M') m : M')
Tactic: rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]
-- 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
m : M
s : ↥S
⊢ s • mk' f m s = (f : (a : M) → M') m
have rw : (↑s : R) • mk' f m s = (f : (a : M) → M') m
Tactic: rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, 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_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
m : M
s : ↥S
rw : (↑s : R) • mk' f m s = (f : (a : M) → M') m
⊢ s • mk' f m s = (f : (a : M) → M') m
have rw₁ : mk' f ((↑s : R) • m) s = (f : (a : M) → M') m
Tactic: rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, 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_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
m : M
s : ↥S
rw : (↑s : R) • mk' f m s = (f : (a : M) → M') m
rw₁ : mk' f ((↑s : R) • m) s = (f : (a : M) → M') m
⊢ s • mk' f m s = (f : (a : M) → M') m
have rw₂ : mk' f (s • m) s = (f : (a : M) → M') m
Tactic: rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, 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_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
m : M
s : ↥S
rw : (↑s : R) • mk' f m s = (f : (a : M) → M') m
rw₁ : mk' f ((↑s : R) • m) s = (f : (a : M) → M') m
rw₂ : mk' f (s • m) s = (f : (a : M) → M') m
⊢ s • mk' f m s = (f : (a : M) → M') m
have rw₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') ((f : (a : M) → M') m : M')
Tactic: rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, 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_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
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂
have delta : Eq.{u_3 + 1} (α := M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) : M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
Tactic: delta mk'
-- 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
m : M
s₁ s₂ : ↥S
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
have rw : Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
Tactic: rw [LocalizedModule.mk_cancel_common_left]
-- 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
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁
have delta : Eq.{u_3 + 1} (α := M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) : M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
Tactic: delta mk'
-- 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
m : M
s₁ s₂ : ↥S
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
have rw : Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
  ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
Tactic: rw [LocalizedModule.mk_cancel_common_right]
-- 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
m₁ m₂ : M
s : ↥S
⊢ mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s
have rw : mk' f (m₁ + m₂) s = mk' f (s • m₁ + s • m₂) (s * s)
Tactic: rw [mk'_add_mk', ← smul_add, mk'_cancel_left]