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
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')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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 : R) • 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')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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')
rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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 : R) • 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₃ : HSMul.hSMul (β := M') (↑b : R)
    ((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).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 : R) • a)
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')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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')
rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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 : R) • a) :
      M')
rw₃ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.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 : R) • 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₄ : HSMul.hSMul (β := M') (↑b : R)
    ((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).1 : M') =
  HSMul.hSMul (β := M') (↑sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
    ((f : (a : M) → M') 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')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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')
rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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 : R) • a) :
      M')
rw₃ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.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 : R) • a)
rw₄ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 : M') =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') 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₅ : (↑b : R) • sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
  HSMul.hSMul (β := M') (↑sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
    ((f : (a : M) → M') 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')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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')
rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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 : R) • a) :
      M')
rw₃ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.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 : R) • a)
rw₄ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 : M') =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') a : M')
rw₅ :
  (↑b : R) • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') 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₆ : b • sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
  HSMul.hSMul (β := M') (↑sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
    ((f : (a : M) → M') 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')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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')
rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((↑b : R) • ⋯.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 : R) • a) :
      M')
rw₃ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.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 : R) • a)
rw₄ :
  HSMul.hSMul (β := M') (↑b : R)
      ((f : (a : M) → M') ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1 : M') =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') a : M')
rw₅ :
  (↑b : R) • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') a : M')
rw₆ :
  b • ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
    HSMul.hSMul (β := M') (↑⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 : R)
      ((f : (a : M) → M') 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₇ : b • sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 • m =
  HSMul.hSMul (β := M') sorry.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2
    ((f : (a : M) → M') 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
⊢ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f = LocalizedModule.mkLinearMap S M
have h : ∀ (m : M),
  Eq (α := LocalizedModule S M)
    (((↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
Tactic: ext m
-- 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 : M' →ₗ[R] LocalizedModule S M) ∘ₗ f : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
have h : HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := M') 1 ((f : (a : M) → M') m : M') = (f : (a : M) → M') m
Tactic: rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe, iso_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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
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'')
⊢ (LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M)) ∘ₗ f = g
have rw : LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f = g
Tactic: rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]
-- 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''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
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'')
rw : LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f = g
⊢ (LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M)) ∘ₗ f = g
have rw₁ : LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g
Tactic: rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]
-- 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''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
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'')
rw : LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f = g
rw₁ : LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g
⊢ (LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M)) ∘ₗ f = g
have rw₂ : g = g
Tactic: rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]
-- 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''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
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 : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) = l
have rw : (l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M')) ∘ₗ LocalizedModule.mkLinearMap S M = g
Tactic: rw [LocalizedModule.lift_unique S g h (l.comp (iso S f).toLinearMap), LinearMap.comp_assoc,
    LinearEquiv.comp_coe, LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap,
    LinearMap.comp_id]
-- 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''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
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 : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M')) ∘ₗ LocalizedModule.mkLinearMap S M = g
have rw : l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f
Tactic: rw [LinearMap.comp_assoc, ← hl]
-- 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''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
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 : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f
have h₁ : ∀ (x : M),
  Eq.{u_4 + 1} (α := M'')
    ((l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M'') x : M'')
    ((l ∘ₗ f : (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_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
map_unit :
  ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ j = k
have hl : k ∘ₗ f = k ∘ₗ f
Tactic: rw [← lift_unique S f (k.comp f) map_unit j h, lift_unique]
-- 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
m : M'
inj : Function.Injective.{u_1 + 1, u_3 + 1} (β := M') fun (r : R) ↦ r • m
s : ↥S
r r' : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ (↑s : R) * x) r) ((fun (x : R) ↦ (↑s : R) * x) r')
⊢ r = r'
have this : Eq.{u_3 + 1} (α := M') ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r))
  ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r'))
Tactic: have := congr_arg (· • m) eq
-- 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
m : M'
inj : Function.Injective.{u_1 + 1, u_3 + 1} (β := M') fun (r : R) ↦ r • m
s : ↥S
r r' : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ (↑s : R) * x) r) ((fun (x : R) ↦ (↑s : R) * x) r')
this :
  Eq.{u_3 + 1} (α := M') ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r))
    ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r'))
⊢ r = r'
have this₁ : r • m = r' • m
Tactic: simp_rw [mul_smul, ← Submonoid.smul_def, smul_inj f] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
r : R
m : M
s : ↥S
⊢ mk' f (r • m) s = r • mk' f m s
have delta : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (r • m) s) =
  HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
Tactic: delta mk'
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
r : R
m : M
s : ↥S
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (r • m) s) =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
have rw : (fromLocalizedModule S f : (a : LocalizedModule S M) → M')
    (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk m s)) =
  HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
Tactic: rw [← LocalizedModule.smul'_mk, map_smul]