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_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'')
r : R
m : LocalizedModule S M
a : M
b : ↥S
⊢ r • lift' S g h (mk a b) = lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
have rw : HSMul.hSMul (β := M'') r (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
  lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
Tactic: rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.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'')
r : R
m : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
⊢ r • lift' S g h (mk a b) = lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
have rw₁ : HSMul.hSMul (β := M'') r (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
  lift' S g h (mk (r • a) b)
Tactic: rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.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'')
r : R
m : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
rw₁ :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (mk (r • a) b)
⊢ r • lift' S g h (mk a b) = lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
have rw₂ : HSMul.hSMul (β := M'') r (((↑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'') (r • a) : M'')
Tactic: rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.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'')
r : R
m : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
rw₁ :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (mk (r • a) b)
rw₂ :
  HSMul.hSMul (β := M'') r (((↑⋯.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'') (r • a) : M'')
⊢ r • lift' S g h (mk a b) = lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
have rw₃ : Eq (α := M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') (HSMul.hSMul (β := M'') r ((g : (a : M) → M'') a : M'')) : M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
Tactic: rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.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'')
r : R
m : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
rw₁ :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (mk (r • a) b)
rw₂ :
  HSMul.hSMul (β := M'') r (((↑⋯.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'') (r • a) : M'')
rw₃ :
  Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') (HSMul.hSMul (β := M'') r ((g : (a : M) → M'') a : M'')) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
⊢ r • lift' S g h (mk a b) = lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
have rw₄ : Eq (α := M'') (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
  (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
Tactic: rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.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
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'')
r : R
x : LocalizedModule S M
⊢ lift' S g h (r • x) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift' S g h x)
have rw : lift' S g h (r • x) = lift' S g h (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
Tactic: rw [LocalizedModule.lift'_smul, RingHom.id_apply]
-- 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'')
r : R
x : LocalizedModule S M
rw : lift' S g h (r • x) = lift' S g h (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
⊢ lift' S g h (r • x) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift' S g h x)
have rw₁ : lift' S g h (r • x) = lift' S g h (r • x)
Tactic: rw [LocalizedModule.lift'_smul, RingHom.id_apply]
-- 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'')
⊢ lift S g h ∘ₗ mkLinearMap S M = g
have h₁ : ∀ (x : M),
  Eq.{u_4 + 1} (α := M'') ((lift S g h ∘ₗ mkLinearMap S M : (a : M) → M'') x : 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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
⊢ lift S g h = l
have h₁ : ∀ (x : LocalizedModule S M),
  Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') x : M'')
    ((l : (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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
x : LocalizedModule S M
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') x : M'')
    ((l : (a : LocalizedModule S M) → M'') x : M'')
have h₁ : ∀ (m : M) (s : ↥S),
  Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') (mk m s) : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')
Tactic: induction x 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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') (mk m s) : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')
have h₁ : Eq (α := M'') (((↑sorry.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') m : M'') : M'')
  ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')
Tactic: rw [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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') m : M'') : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')
have h₁ : Eq.{u_4 + 1} (α := M'') ((l : (a : LocalizedModule S M) → M'') (mk m 1) : M'')
  ((l : (a : LocalizedModule S M) → M'') (mk ((↑s : R) • m) s) : M'')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
    Function.comp_apply, LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ Eq.{u_4 + 1} (α := M'') ((l : (a : LocalizedModule S M) → M'') (mk m 1) : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk ((↑s : R) • m) s) : M'')
have h₁ : Eq (α := LocalizedModule S M) (mk m 1) (mk ((↑s : R) • m) s)
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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ Eq (α := LocalizedModule S M) (mk m 1) (mk ((↑s : R) • m) s)
have h₁ : ∃ (u : ↥S), u • s • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m)
Tactic: rw [LocalizedModule.mk_eq]
-- 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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ ∃ (u : ↥S), u • s • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m)
have h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 (s • m) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m))
Tactic: refine ⟨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
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''
p : LocalizedModule S M
m : M
t : ↥S
⊢ ∃ (x : Prod.{u_2, u_1} M ↥S),
    HSMul.hSMul (β := LocalizedModule S M) x.2 (LocalizedModule.mk m t) =
      (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x.1
have refine : HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
Tactic: refine ⟨⟨m, t⟩, ?_⟩
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
have rw : HSMul.hSMul (β := LocalizedModule S M) (↑(m, t).2 : R) (LocalizedModule.mk m t) =
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
Tactic: rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M) (↑(m, t).2 : R) (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
⊢ HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
have rw₁ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t)
  ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1)
Tactic: rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M) (↑(m, t).2 : R) (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
rw₁ :
  Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1)
⊢ HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
have rw₂ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t) (LocalizedModule.mk (m, t).1 1)
Tactic: rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M) (↑(m, t).2 : R) (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
rw₁ :
  Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1)
rw₂ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t) (LocalizedModule.mk (m, t).1 1)
⊢ HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
have rw₃ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((m, t).2 • m) t) (LocalizedModule.mk (m, t).1 1)
Tactic: rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M) (↑(m, t).2 : R) (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
rw₁ :
  Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1)
rw₂ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t) (LocalizedModule.mk (m, t).1 1)
rw₃ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((m, t).2 • m) t) (LocalizedModule.mk (m, t).1 1)
⊢ HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
have rw₄ : Eq (α := LocalizedModule S M) (LocalizedModule.mk m 1) (LocalizedModule.mk (m, t).1 1)
Tactic: rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]
-- 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 : ↥(Algebra.algebraMapSubmonoid A S)
⊢ IsUnit.{u_6} (M := End A N) ((algebraMap A (End A N) : (a : A) → End A N) (↑x : A) : End A N)
have obtain : ∀ (x : R) (hx : x ∈ (↑S : Set R)),
  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) sorry) :
          A) :
      End A N)
Tactic: obtain ⟨_, x, hx, rfl⟩ := x
Cleared hypotheses: 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
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)
⊢ 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 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)
Tactic: have := IsLocalizedModule.map_units (f.restrictScalars R) ⟨x, hx⟩