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
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x : R
hx : x ∈ (↑S : Set R)
this :
  IsUnit.{u_6} (M := End R N)
    ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) x hx) : R) : End R N)
⊢ IsUnit.{u_6} (M := End A N)
    ((algebraMap A (End A N) : (a : A) → End A N)
        (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
              ((algebraMap R A : (a : R) → A) x) ⋯) :
          A) :
      End A N)
have simp : ∀
  (this :
    Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
      (⇑((algebraMap R (End R N) : (a : R) → End R N) x : End R N) : (a : N) → N)),
  Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
    (⇑((algebraMap R (End A N) : (a : R) → End A N) x : End A N) : (a : N) → N)
Tactic: simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
y : N
⊢ ∃ (x : Prod.{u_2, u_5} M ↥(Algebra.algebraMapSubmonoid A S)), x.2 • y = (f : (a : M) → N) x.1
have obtain : ∀ (x : M) (t : ↥S)
  (e :
    (x, t).2 • y =
      ((↑R :
              {S : Type u_5} →
                {M : Type u_2} →
                  {M₂ : Type u_6} →
                    [inst : Semiring R] →
                      [inst_12 : Semiring S] →
                        [inst_13 : AddCommMonoid M] →
                          [inst_14 : AddCommMonoid M₂] →
                            [inst_15 : Module R M] →
                              [inst_16 : Module R M₂] →
                                [inst_17 : Module S M] →
                                  [inst_18 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → N)
        (x, t).1),
  ∃ (x : Prod.{u_2, u_5} M ↥(Algebra.algebraMapSubmonoid A S)), x.2 • y = (f : (a : M) → N) x.1
Tactic: obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S (f.restrictScalars R) y
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x₁ x₂ : M
e : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), c • x₁ = c • x₂
have obtain : ∀ (c : ↥S) (hc : c • x₁ = c • x₂), ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), c • x₁ = c • x₂
Tactic: obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f.restrictScalars R) e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x : ↥T
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
have obtain : ∀ (m : R) (mx : m * (↑x : R) ∈ S),
  IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
Tactic: obtain ⟨m, mx⟩ := h' x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x : ↥T
m : R
mx : m * (↑x : R) ∈ S
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
have this : IsUnit.{u_6} (M := End R N)
  ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (m * (↑x : R)) mx) : R) :
    End R N)
Tactic: have := IsLocalizedModule.map_units f ⟨_, mx⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x : ↥T
m : R
mx : m * (↑x : R) ∈ S
this :
  IsUnit.{u_6} (M := End R N)
    ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (m * (↑x : R)) mx) : R) :
      End R N)
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
have this₁ : IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) m : End R N) ∧
  IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
Tactic: rw [map_mul, (Algebra.commute_algebraMap_left _ _).isUnit_mul_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
y : N
⊢ ∃ (x : Prod.{u_2, u_1} M ↥T), x.2 • y = (f : (a : M) → N) x.1
have obtain : ∀ (x : M) (t : ↥S) (e : (x, t).2 • y = (f : (a : M) → N) (x, t).1),
  ∃ (x : Prod.{u_2, u_1} M ↥T), x.2 • y = (f : (a : M) → N) x.1
Tactic: obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S f y
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
e : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N)
⊢ ∃ (c : ↥T), c • x₁ = c • x₂
have obtain : ∀ (c : ↥S) (hc : c • x₁ = c • x₂), ∃ (c : ↥T), c • x₁ = c • x₂
Tactic: obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f) e
-- 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 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ Eq.{u_3 + 1} (α := M')
    ((fun (x : Prod.{u_2, u_1} M ↥S) ↦ (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') x.1 : M') : M'))
      (a, b))
    ((fun (x : Prod.{u_2, u_1} M ↥S) ↦ (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') x.1 : M') : M'))
      (a', b'))
have dsimp : Eq (α := M') (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
  (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : 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_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 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ Eq (α := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')
have rw : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑(a, b).2 : R) • a') : M')
  ((f : (a : M) → M') ((↑(a', b').2 : R) • a) : M')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, ← map_smul,
        Module.End.algebraMap_isUnit_inv_apply_eq_iff', ← 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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ fromLocalizedModule' S f (HAdd.hAdd (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')) =
    fromLocalizedModule' S f (LocalizedModule.mk a b) + fromLocalizedModule' S f (LocalizedModule.mk a' b')
have simp : ((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') (b' • a + b • a') : M') =
  HAdd.hAdd (α := M') (β := M') (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
    (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')
Tactic: simp only [LocalizedModule.mk_add_mk, fromLocalizedModule'_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') (b' • a + b • a') : M') =
    HAdd.hAdd (α := M') (β := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')
have rw : HAdd.hAdd (α := M') (β := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M') =
  HAdd.hAdd (α := M') (β := M')
    (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
    (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) : M')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul, ← map_smul,
        ← map_smul, map_add]
-- 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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ HAdd.hAdd (α := M') (β := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M') =
    HAdd.hAdd (α := M') (β := M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) :
        M')
have e_a : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M')
  (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
⊢ HAdd.hAdd (α := M') (β := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M') =
    HAdd.hAdd (α := M') (β := M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) :
        M')
have e_a₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b • a') : M')
  (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
have e_a : (f : (a : M) → M') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M') (↑b : R) ((f : (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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b • a') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) : M')
have e_a : HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
  HSMul.hSMul (β := M') (↑b' : R) ((f : (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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
have e_a : HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
  HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
Tactic: rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, 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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
⊢ HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
have e_a₁ : HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
  (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
Tactic: rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, 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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
e_a₁ :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
⊢ HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
have e_a₂ : HSMul.hSMul (β := M') ((↑b' : R) * (↑b : R)) ((f : (a : M) → M') a' : M') =
  (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
Tactic: rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, 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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
e_a₁ :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
e_a₂ :
  HSMul.hSMul (β := M') ((↑b' : R) * (↑b : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
⊢ HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
have e_a₃ : (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
  (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
Tactic: rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, 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_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
e_a₁ :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
e_a₂ :
  HSMul.hSMul (β := M') ((↑b' : R) * (↑b : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
e_a₃ :
  (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
⊢ HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
have e_a₄ : (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
  (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M')
Tactic: rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, 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_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
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) =
    fromLocalizedModule' S f (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk a b))
have rw : HSMul.hSMul (β := M') r (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
  fromLocalizedModule' S f (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk a b))
Tactic: rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk,
        f.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_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
x : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    fromLocalizedModule' S f (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk a b))
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) =
    fromLocalizedModule' S f (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk a b))
have rw₁ : HSMul.hSMul (β := M') r (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
  fromLocalizedModule' S f (LocalizedModule.mk (r • a) b)
Tactic: rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk,
        f.map_smul, map_smul]