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
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))
rw₁ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    fromLocalizedModule' S f (LocalizedModule.mk (r • 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') =
  ((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') (r • a) : M')
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))
rw₁ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    fromLocalizedModule' S f (LocalizedModule.mk (r • a) b)
rw₂ :
  HSMul.hSMul (β := M') r (((↑⋯.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') (r • a) : M')
⊢ 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') =
  ((↑sorry.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') r ((f : (a : M) → M') a : M'))
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))
rw₁ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    fromLocalizedModule' S f (LocalizedModule.mk (r • a) b)
rw₂ :
  HSMul.hSMul (β := M') r (((↑⋯.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') (r • a) : M')
rw₃ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') r ((f : (a : M) → M') a : M'))
⊢ 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') =
  HSMul.hSMul (β := M') r (((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
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
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
r : R
x : LocalizedModule S M
⊢ fromLocalizedModule' S f (r • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (fromLocalizedModule' S f x)
have rw : fromLocalizedModule' S f (r • x) =
  fromLocalizedModule' S f (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
Tactic: rw [fromLocalizedModule'_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 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
r : R
x : LocalizedModule S M
rw :
  fromLocalizedModule' S f (r • x) =
    fromLocalizedModule' S f (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
⊢ fromLocalizedModule' S f (r • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (fromLocalizedModule' S f x)
have rw₁ : fromLocalizedModule' S f (r • x) = fromLocalizedModule' S f (r • x)
Tactic: rw [fromLocalizedModule'_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
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
eq1 :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') x : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') y : M')
⊢ x = y
have h : ∀ (a : M) (b : ↥S)
  (eq1 :
    Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a b) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') y : M')),
  LocalizedModule.mk a b = y
Tactic: induction x with | _ a b
Cleared hypotheses: x, 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
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
y : LocalizedModule S M
a : M
b : ↥S
eq1 :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a b) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') y : M')
⊢ LocalizedModule.mk a b = y
have h : ∀ (a' : M) (b' : ↥S)
  (eq1 :
    Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a b) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a' b') : M')),
  Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
Tactic: induction y with | _ a' b'
Cleared hypotheses: y, eq1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  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')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have eq1₁ : HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
  HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
Tactic: rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff'] at eq1
Cleared hypotheses: 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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h : ∃ (u : ↥S), u • b' • a = u • b • a'
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h₂ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') (b • a') : M')
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
h₂ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') (b • a') : M')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') ((↑b : R) • a') : M')
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
h₂ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') (b • a') : M')
h₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') ((↑b : R) • a') : M')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h₄ : HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') = (f : (a : M) → M') ((↑b : R) • a')
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
h₂ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') (b • a') : M')
h₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') ((↑b : R) • a') : M')
h₄ : HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') = (f : (a : M) → M') ((↑b : R) • a')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h₅ : HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') =
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M')
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
h₂ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') (b • a') : M')
h₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') ((↑b : R) • a') : M')
h₄ : HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') = (f : (a : M) → M') ((↑b : R) • a')
h₅ :
  HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') =
    HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
have h₆ : HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') =
  HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
Tactic: rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.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
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 : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = (f : (a : M) → M') (m, s).1
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) = x
have rw : ((↑sorry.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M') = x
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
      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 : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = (f : (a : M) → M') (m, s).1
rw : ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M') = x
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) = x
have rw₁ : (f : (a : M) → M') m = (↑s : R) • x
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
      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 : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = (f : (a : M) → M') (m, s).1
rw : ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M') = x
rw₁ : (f : (a : M) → M') m = (↑s : R) • x
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) = x
have rw₂ : (m, s).2 • x = (↑s : R) • x
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
      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 : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = (f : (a : M) → M') (m, s).1
rw : ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M') = x
rw₁ : (f : (a : M) → M') m = (↑s : R) • x
rw₂ : (m, s).2 • x = (↑s : R) • x
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) = x
have rw₃ : (↑(m, s).2 : R) • x = (↑s : R) • x
Tactic: rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
      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
m : M'
⊢ Eq (α := LocalizedModule S M) (((iso S f).symm : (a : M') → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
        ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 :
      LocalizedModule S M)
have apply_fun : Eq.{u_3 + 1} (α := M')
  ((iso S f : (a : LocalizedModule S M) → M')
      (((iso S f).symm : (a : M') → LocalizedModule S M) m : LocalizedModule S M) :
    M')
  ((iso S f : (a : LocalizedModule S M) → M')
      (LocalizedModule.mk sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
        sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2) :
    M')
Tactic: apply_fun iso S f using LinearEquiv.injective (iso S f)
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
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')
    ((iso S f : (a : LocalizedModule S M) → M')
        (((iso S f).symm : (a : M') → LocalizedModule S M) m : LocalizedModule S M) :
      M')
    ((iso S f : (a : LocalizedModule S M) → M')
        (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
          ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2) :
      M')
have rw : m =
  (iso S f : (a : LocalizedModule S M) → M')
    (LocalizedModule.mk sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
      sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2)
Tactic: rw [LinearEquiv.apply_symm_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
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'
a : M
b : ↥S
eq1 : b • m = (f : (a : M) → M') a
⊢ ∃ (u : ↥S),
    u • b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 =
      u • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a
have rw : Eq.{u_3 + 1} (α := M')
  ((f : (a : M) → M') (b • sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1) : M')
  ((f : (a : M) → M') (sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a) : M')
Tactic: rw [← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul,
        f.map_smul, ← (surj _ _ _).choose_spec, ← Submonoid.smul_def, ← Submonoid.smul_def,
        ← mul_smul, mul_comm, mul_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
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'
a : M
b : ↥S
eq1 : b • m = (f : (a : M) → M') a
rw :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M') (b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1) : M')
    ((f : (a : M) → M') (⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a) : M')
⊢ ∃ (u : ↥S),
    u • b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 =
      u • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a
have rw₁ : Eq.{u_3 + 1} (α := M')
  ((f : (a : M) → M') ((↑b : R) • sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1) :
    M')
  ((f : (a : M) → M') (sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • a) : M')
Tactic: rw [← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul,
        f.map_smul, ← (surj _ _ _).choose_spec, ← Submonoid.smul_def, ← Submonoid.smul_def,
        ← mul_smul, mul_comm, mul_smul, eq1]