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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
⊢ HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M''))
have symm : ((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'')
    ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
  HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
Tactic: symm
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
have rw : (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
have rw₁ : HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m', s').2 : R) • m) : M'') =
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₁ :
  HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m', s').2 : R) • m) : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
have rw₂ : (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₁ :
  HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m', s').2 : R) • m) : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₂ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
have rw₃ : (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
  HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m, s).2 : R) • m') : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₁ :
  HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m', s').2 : R) • m) : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₂ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₃ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m, s).2 : R) • m') : M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
have rw₄ : Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) : M'')
  ((g : (a : M) → M'') ((↑c : R) • (↑(m, s).2 : R) • m') : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g_1 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₁ :
  HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m', s').2 : R) • m) : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₂ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₃ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m, s).2 : R) • m') : M'')
rw₄ :
  Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) : M'')
    ((g : (a : M) → M'') ((↑c : R) • (↑(m, s).2 : R) • m') : M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
have rw₅ : Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') ((↑c : R) • (↑s : R) • m') : M'')
  ((g : (a : M) → M'') ((↑c : R) • (↑(m, s).2 : R) • m') : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ lift' S g h (HAdd.hAdd (α := LocalizedModule S M) (mk a b) (mk a' b')) = lift' S g h (mk a b) + lift' S g h (mk a' b')
have rw : ((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑(b * b') : R)) sorry)⁻¹ : End R M'') :
      (a : M'') → M'')
    ((g : (a : M) → M'') (b' • a + b • a') : M'') =
  HAdd.hAdd (α := M'') (β := M'') (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'')
    (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a' : M'') : M'')
Tactic: rw [mk_add_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑(b * b') : R)) ⋯)⁻¹ : End R M'') :
        (a : M'') → M'')
      ((g : (a : M) → M'') (b' • a + b • a') : M'') =
    HAdd.hAdd (α := M'') (β := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a' : M'') : M'')
have rw : HAdd.hAdd (α := M'') (β := M'') ((g : (a : M) → M'') (b' • a) : M'') ((g : (a : M) → M'') (b • a') : M'') =
  HAdd.hAdd (α := M'') (β := M'')
    (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
    (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
      M'')
Tactic: rw [map_add, Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul,
        ← map_smul, ← 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ HAdd.hAdd (α := M'') (β := M'') ((g : (a : M) → M'') (b' • a) : M'') ((g : (a : M) → M'') (b • a') : M'') =
    HAdd.hAdd (α := M'') (β := M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
          (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
        M'')
have e_a : Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b' • a) : M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
Tactic: congr 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_2
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b' • a) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
⊢ HAdd.hAdd (α := M'') (β := M'') ((g : (a : M) → M'') (b' • a) : M'') ((g : (a : M) → M'') (b • a') : M'') =
    HAdd.hAdd (α := M'') (β := M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
          (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
        M'')
have e_a₁ : Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b • a') : M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
    M'')
Tactic: congr 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_2
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b' • a) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
have e_a : Eq (α := M'') (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
  ((g : (a : M) → M'') (b' • a) : M'')
Tactic: symm
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b • a') : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
      M'')
have e_a : Eq (α := M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
    M'')
  ((g : (a : M) → M'') (b • a') : M'')
Tactic: symm
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
    ((g : (a : M) → M'') (b' • a) : M'')
have e_a : (g : (a : M) → M'') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M'') (↑b : R) ((g : (a : M) → M'') (b' • a) : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff]
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (g : (a : M) → M'') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M'') (↑b : R) ((g : (a : M) → M'') (b' • a) : M'')
have e_a : HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a : M'') =
  (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
Tactic: simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
have e_a : (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'') =
  (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
Tactic: rw [mul_smul, Submonoid.smul_def]
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
⊢ HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
have e_a₁ : (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'') =
  (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'')
Tactic: rw [mul_smul, Submonoid.smul_def]
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
      M'')
    ((g : (a : M) → M'') (b • a') : M'')
have e_a : Eq (α := M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'')
      (HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a' : M'')) :
    M'')
  ((g : (a : M) → M'') (b • a') : M'')
Tactic: dsimp
-- 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a' : M'')) :
      M'')
    ((g : (a : M) → M'') (b • a') : M'')
have e_a : HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') ((↑b : R) • a') : M'') =
  HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') (b • a') : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, mul_comm, mul_smul, ← map_smul]