awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw : Eq (α := LocalizedModule S M)
  ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
      (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
    LocalizedModule S M)
  (mk m t : LocalizedModule S M)
Tactic: rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₁ : (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry =
  mk m t
Tactic: rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    mk m t
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₂ : Eq (α := LocalizedModule S M) (liftOn (mk ((↑s : R) • m) t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry) (mk m t)
Tactic: rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    mk m t
rw₂ :
  Eq (α := LocalizedModule S M) (liftOn (mk ((↑s : R) • m) t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
    (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • m, t).1 (((↑s : R) • m, t).2 * s)) (mk m t)
Tactic: rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    mk m t
rw₂ :
  Eq (α := LocalizedModule S M) (liftOn (mk ((↑s : R) • m) t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
    (mk m t)
rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • m, t).1 (((↑s : R) • m, t).2 * s)) (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₄ : Eq (α := LocalizedModule S M) (mk (s • m, t).1 ((s • m, t).2 * s)) (mk m t)
Tactic: rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  (HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk m t)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    mk m t
rw₂ :
  Eq (α := LocalizedModule S M) (liftOn (mk ((↑s : R) • m) t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
    (mk m t)
rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • m, t).1 (((↑s : R) • m, t).2 * s)) (mk m t)
rw₄ : Eq (α := LocalizedModule S M) (mk (s • m, t).1 ((s • m, t).2 * s)) (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M)
        ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
              End R (LocalizedModule S M)) :
            (a : LocalizedModule S M) → LocalizedModule S M)
          (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₅ : Eq (α := LocalizedModule S M) (mk m (s • m, t).2) (mk m t)
Tactic: rw [Module.algebraMap_end_apply, divBy_apply, smul'_mk, liftOn_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw : Eq (α := LocalizedModule S M)
  ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
          End R (LocalizedModule S M)) :
        (a : LocalizedModule S M) → LocalizedModule S M)
      (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry) :
    LocalizedModule S M)
  (mk m t : LocalizedModule S M)
Tactic: rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₁ : HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry) =
  mk m t
Tactic: rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) =
    mk m t
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₂ : HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk (m, t).1 ((m, t).2 * s)) = mk m t
Tactic: rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) =
    mk m t
rw₂ : HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk (m, t).1 ((m, t).2 * s)) = mk m t
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • (m, t).1) ((m, t).2 * s)) (mk m t)
Tactic: rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) =
    mk m t
rw₂ : HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk (m, t).1 ((m, t).2 * s)) = mk m t
rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • (m, t).1) ((m, t).2 * s)) (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₄ : Eq (α := LocalizedModule S M) (mk (s • (m, t).1) ((m, t).2 * s)) (mk m t)
Tactic: rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
rw :
  Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (liftOn (mk m t) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯) =
    mk m t
rw₂ : HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (mk (m, t).1 ((m, t).2 * s)) = mk m t
rw₃ : Eq (α := LocalizedModule S M) (mk ((↑s : R) • (m, t).1) ((m, t).2 * s)) (mk m t)
rw₄ : Eq (α := LocalizedModule S M) (mk (s • (m, t).1) ((m, t).2 * s)) (mk m t)
⊢ Eq (α := LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        ((divBy s : (a : LocalizedModule S M) → LocalizedModule S M) (mk m t)) :
      LocalizedModule S M)
    (mk m t : LocalizedModule S M)
have rw₅ : Eq (α := LocalizedModule S M) (mk (m, t).1 (m, t).2) (mk m t)
Tactic: rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]
-- 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
x₁ x₂ : M
h_1 : ∃ (c : ↥S), c • x₁ = c • x₂
c : ↥S
h : c • x₁ = c • x₂
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')
have h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (c • x₁) : M') ((f : (a : M) → M') (c • x₂) : M')
Tactic: apply_fun f at h
Cleared hypotheses: h
-- 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
x₁ x₂ : M
h_1 : ∃ (c : ↥S), c • x₁ = c • x₂
c : ↥S
h : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (c • x₁) : M') ((f : (a : M) → M') (c • x₂) : M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M')
have h₁ : Eq.{u_3 + 1} (α := M')
  ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M') ((f : (a : M) → M') x₁ : M') :
    M')
  ((((algebraMap R (End R M') : (a : R) → End R M') (↑c : R) : End R M') : (a : M') → M') ((f : (a : M) → M') x₂ : M') :
    M')
Tactic: simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h
Cleared hypotheses: 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
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
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔ ∀ (c : ↥S), IsSMulRegular M c
have simp_rw : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔
  ∀ (c : ↥S), Function.Injective (β := M) fun (x : M) ↦ c • x
Tactic: simp_rw [IsSMulRegular, Function.Injective, eq_iff_exists S, exists_imp, forall_comm (α := S)]
-- 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
simp_rw :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔
    ∀ (c : ↥S), Function.Injective (β := M) fun (x : M) ↦ c • x
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔ ∀ (c : ↥S), IsSMulRegular M c
have simp_rw₁ : (∀ ⦃a₁ a₂ : M⦄, Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') a₁ : M') ((f : (a : M) → M') a₂ : M') → a₁ = a₂) ↔
  ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
Tactic: simp_rw [IsSMulRegular, Function.Injective, eq_iff_exists S, exists_imp, forall_comm (α := S)]
-- 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
simp_rw :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔
    ∀ (c : ↥S), Function.Injective (β := M) fun (x : M) ↦ c • x
simp_rw₁ :
  (∀ ⦃a₁ a₂ : M⦄, Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') a₁ : M') ((f : (a : M) → M') a₂ : M') → a₁ = a₂) ↔
    ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔ ∀ (c : ↥S), IsSMulRegular M c
have simp_rw₂ : (∀ ⦃a₁ a₂ : M⦄, (∃ (c : ↥S), c • a₁ = c • a₂) → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
Tactic: simp_rw [IsSMulRegular, Function.Injective, eq_iff_exists S, exists_imp, forall_comm (α := S)]
-- 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
simp_rw :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔
    ∀ (c : ↥S), Function.Injective (β := M) fun (x : M) ↦ c • x
simp_rw₁ :
  (∀ ⦃a₁ a₂ : M⦄, Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') a₁ : M') ((f : (a : M) → M') a₂ : M') → a₁ = a₂) ↔
    ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
simp_rw₂ : (∀ ⦃a₁ a₂ : M⦄, (∃ (c : ↥S), c • a₁ = c • a₂) → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M') ↔ ∀ (c : ↥S), IsSMulRegular M c
have simp_rw₃ : (∀ ⦃a₁ a₂ : M⦄ (x : ↥S), x • a₁ = x • a₂ → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
Tactic: simp_rw [IsSMulRegular, Function.Injective, eq_iff_exists S, exists_imp, forall_comm (α := S)]
-- 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''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ (algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) =
    (↑e : M' →ₗ[R] M'') ∘ₗ (algebraMap R (End R M') : (a : R) → End R M') (↑s : R) ∘ₗ (↑e.symm : M'' →ₗ[R] M')
have h : ∀ (x : M''),
  Eq (α := M'') ((((algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) : End R M'') : (a : M'') → M'') x : M'')
    (((↑e : M' →ₗ[R] M'') ∘ₗ (algebraMap R (End R M') : (a : R) → End R M') (↑s : R) ∘ₗ (↑e.symm : M'' →ₗ[R] M') :
          (a : M'') → M'')
        x :
      M'')
Tactic: ext
-- 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''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R) : End R M'')
have rw : Function.Bijective.{u_3 + 1, u_3 + 1} (α := M') (β := M')
  (⇑((algebraMap R (End R M') : (a : R) → End R M') (↑s : R) : End R M') : (a : M') → M')
Tactic: rw [show algebraMap R (Module.End R M'') s = e ∘ₗ (algebraMap R (Module.End R M') s) ∘ₗ e.symm
      by ext; simp, Module.End.isUnit_iff, LinearMap.coe_comp, LinearMap.coe_comp,
      LinearEquiv.coe_coe, LinearEquiv.coe_coe, EquivLike.comp_bijective, EquivLike.bijective_comp]
-- 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''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
⊢ ∃ (x_1 : Prod.{u_2, u_1} M ↥S), x_1.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x_1.1
have obtain : ∀ (p : Prod.{u_2, u_1} M ↥S)
  (h : HSMul.hSMul (β := M') p.2 ((e.symm : (a : M'') → M') x : M') = (f : (a : M) → M') p.1),
  ∃ (x_1 : Prod.{u_2, u_1} M ↥S), x_1.2 • x = ((↑e : M' →ₗ[R] M'') ∘ₗ f : (a : M) → M'') x_1.1
Tactic: obtain ⟨p, h⟩ := hf.surj (e.symm x)