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
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw₁ : (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
  HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_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
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
rw₁ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw₂ : (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
  HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (LocalizedModule.mk m s)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_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
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
rw₁ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
rw₂ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (LocalizedModule.mk m s)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw₃ : Eq (α := LocalizedModule S M)
  ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
  (LocalizedModule.mk ((↑s : R) • m) s : LocalizedModule S M)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_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
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
rw₁ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
rw₂ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (LocalizedModule.mk m s)
rw₃ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk ((↑s : R) • m) s : LocalizedModule S M)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw₄ : Eq (α := LocalizedModule S M)
  ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
  (LocalizedModule.mk (s • m) s : LocalizedModule S M)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_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
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
rw₁ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
rw₂ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (LocalizedModule.mk m s)
rw₃ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk ((↑s : R) • m) s : LocalizedModule S M)
rw₄ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk (s • m) s : LocalizedModule S M)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw₅ : Eq (α := LocalizedModule S M)
  ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
  (LocalizedModule.mk m 1 : LocalizedModule S M)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_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
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
rw₁ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
rw₂ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (LocalizedModule.mk m s)
rw₃ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk ((↑s : R) • m) s : LocalizedModule S M)
rw₄ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk (s • m) s : LocalizedModule S M)
rw₅ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk m 1 : LocalizedModule S M)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)
have rw₆ : Eq (α := LocalizedModule S M) (LocalizedModule.mk m 1) (LocalizedModule.mk m 1)
Tactic: rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_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'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ IsLocalization.mk' A x s • mk' f m t = mk' f (x • m) (s * t)
have a : Eq.{u_3 + 1} (α := M') ((fun (m : M') ↦ (s * t) • m) (IsLocalization.mk' A x s • mk' f m t))
  ((fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t)))
Tactic: apply smul_injective f (s * 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
| (fun (m : M') ↦ (s * t) • m) (IsLocalization.mk' A x s • mk' f m t)
have simp : s • IsLocalization.mk' A x s • t • mk' f m t
Tactic: simp only [smul_assoc, mul_smul, smul_comm 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ Eq.{u_3 + 1} (α := M') ((fun (m : M') ↦ (s * t) • m) (IsLocalization.mk' A x s • mk' f m t))
    ((fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t)))
have a : s • IsLocalization.mk' A x s • t • mk' f m t = (fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t))
Tactic: conv_lhs => simp only [smul_assoc, mul_smul, smul_comm 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ s • IsLocalization.mk' A x s • t • mk' f m t = (fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t))
have a : (↑s : R) • HSMul.hSMul (β := M') (IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
  HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
Tactic: simp only [mk'_cancel', map_smul, Submonoid.smul_def 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'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ (↑s : R) • HSMul.hSMul (β := M') (IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
    HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
have a : HSMul.hSMul (β := M') ((↑s : R) • IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
  HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
Tactic: rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_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'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
a :
  HSMul.hSMul (β := M') ((↑s : R) • IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
    HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
⊢ (↑s : R) • HSMul.hSMul (β := M') (IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
    HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
have a₁ : HSMul.hSMul.{u_5, u_3, u_3} (α := A) (β := M') ((algebraMap R A : (a : R) → A) x : A) ((f : (a : M) → M') m : M') =
  HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
Tactic: rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_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'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
a :
  HSMul.hSMul (β := M') ((↑s : R) • IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
    HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
a₁ :
  HSMul.hSMul.{u_5, u_3, u_3} (α := A) (β := M') ((algebraMap R A : (a : R) → A) x : A) ((f : (a : M) → M') m : M') =
    HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
⊢ (↑s : R) • HSMul.hSMul (β := M') (IsLocalization.mk' A x s) ((f : (a : M) → M') m : M') =
    HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
have a₂ : HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M')
Tactic: rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x : M'
⊢ ∃ (a : Prod.{u_2, u_1} M ↥S), Function.uncurry (mk' f) a = x
have obtain : ∀ (m : M) (s : ↥S) (e : s • x = (f : (a : M) → M') m), ∃ (a : Prod.{u_2, u_1} M ↥S), Function.uncurry (mk' f) a = x
Tactic: obtain ⟨⟨m, s⟩, e : s • x = f m⟩ := IsLocalizedModule.surj S f x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_7 : IsLocalizedModule S₁ f₁
inst_8 : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ (liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (mk' f₁ m s) = mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯)
have a : Eq.{u_6 + 1} (α := M₂)
  ((((algebraMap R (End R M₂) : (a : R) → End R M₂) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) sorry) : R) :
          End R M₂) :
        (a : M₂) → M₂)
      ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (mk' f₁ m s) : M₂) :
    M₂)
  ((((algebraMap R (End R M₂) : (a : R) → End R M₂) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) sorry) : R) :
          End R M₂) :
        (a : M₂) → M₂)
      (mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) sorry)) :
    M₂)
Tactic: apply ((Module.End.isUnit_iff _).mp (map_units f₂ ⟨s, h s.2⟩)).1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_7 : IsLocalizedModule S₁ f₁
inst_8 : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ Eq.{u_6 + 1} (α := M₂)
    ((((algebraMap R (End R M₂) : (a : R) → End R M₂) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯) : R) :
            End R M₂) :
          (a : M₂) → M₂)
        ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (mk' f₁ m s) : M₂) :
      M₂)
    ((((algebraMap R (End R M₂) : (a : R) → End R M₂) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯) : R) :
            End R M₂) :
          (a : M₂) → M₂)
        (mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯)) :
      M₂)
have a : (liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) ((f₁ : (a : M) → M₁) m : M₁) =
  s • mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) sorry)
Tactic: simp only [Module.algebraMap_end_apply, ← map_smul, ← Submonoid.smul_def, mk'_cancel']
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_7 : IsLocalizedModule S₁ f₁
inst_8 : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ (liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) ((f₁ : (a : M) → M₁) m : M₁) =
    s • mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯)
have a : (f₂ : (a : M) → M₂) m = s • mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) sorry)
Tactic: rw [liftOfLE, lift_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
M₁ : Type u_6
M₂ : Type u_7
inst_13 : AddCommMonoid M₁
inst_14 : AddCommMonoid M₂
inst_15 : Module R M₁
inst_16 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_17 : IsLocalizedModule S₁ f₁
inst_18 : IsLocalizedModule S₂ f₂
y : M₂
⊢ ∃ (x : Prod.{u_6, u_1} M₁ ↥S₂), x.2 • y = (liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) x.1
have obtain : ∀ (y' : M) (s : ↥S₂) (e : (y', s).2 • y = (f₂ : (a : M) → M₂) (y', s).1),
  ∃ (x : Prod.{u_6, u_1} M₁ ↥S₂), x.2 • y = (liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) x.1
Tactic: obtain ⟨⟨y', s⟩, e⟩ := IsLocalizedModule.surj S₂ f₂ y
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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
M₁ : Type u_6
M₂ : Type u_7
inst_13 : AddCommMonoid M₁
inst_14 : AddCommMonoid M₂
inst_15 : Module R M₁
inst_16 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_17 : IsLocalizedModule S₁ f₁
inst_18 : IsLocalizedModule S₂ f₂
x₁ x₂ : M₁
e :
  Eq.{u_7 + 1} (α := M₂) ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) x₁ : M₂)
    ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) x₂ : M₂)
⊢ ∃ (c : ↥S₂), c • x₁ = c • x₂
have obtain : ∀ (x₁ : Prod.{u_2, u_1} M ↥S₁)
  (e :
    Eq.{u_7 + 1} (α := M₂) ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (Function.uncurry (mk' f₁) x₁) : M₂)
      ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) x₂ : M₂)),
  ∃ (c : ↥S₂), c • Function.uncurry (mk' f₁) x₁ = c • x₂
Tactic: obtain ⟨x₁, s₁, rfl⟩ := mk'_surjective S₁ f₁ x₁
Cleared hypotheses: x₁, e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst_13 : AddCommMonoid M₁
inst_14 : AddCommMonoid M₂
inst_15 : Module R M₁
inst_16 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_17 : IsLocalizedModule S₁ f₁
inst_18 : IsLocalizedModule S₂ f₂
x₂ : M₁
x₁ : Prod.{u_2, u_1} M ↥S₁
e :
  Eq.{u_7 + 1} (α := M₂) ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (Function.uncurry (mk' f₁) x₁) : M₂)
    ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) x₂ : M₂)
⊢ ∃ (c : ↥S₂), c • Function.uncurry (mk' f₁) x₁ = c • x₂
have obtain : ∀ (x₂ : Prod.{u_2, u_1} M ↥S₁)
  (e :
    Eq.{u_7 + 1} (α := M₂) ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (Function.uncurry (mk' f₁) x₁) : M₂)
      ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (Function.uncurry (mk' f₁) x₂) : M₂)),
  ∃ (c : ↥S₂), c • Function.uncurry (mk' f₁) x₁ = c • Function.uncurry (mk' f₁) x₂
Tactic: obtain ⟨x₂, s₂, rfl⟩ := mk'_surjective S₁ f₁ x₂
Cleared hypotheses: x₂, e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst_13 : AddCommMonoid M₁
inst_14 : AddCommMonoid M₂
inst_15 : Module R M₁
inst_16 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_17 : IsLocalizedModule S₁ f₁
inst_18 : IsLocalizedModule S₂ f₂
x₁ x₂ : Prod.{u_2, u_1} M ↥S₁
e :
  Eq.{u_7 + 1} (α := M₂) ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (Function.uncurry (mk' f₁) x₁) : M₂)
    ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (Function.uncurry (mk' f₁) x₂) : M₂)
⊢ ∃ (c : ↥S₂), c • Function.uncurry (mk' f₁) x₁ = c • Function.uncurry (mk' f₁) x₂
have simp : ∀ (e : ∃ (s : ↥S₂), (↑s : R) • (↑x₁.2 : R) • x₂.1 = (↑s : R) • (↑x₂.2 : R) • x₁.1),
  ∃ (c : ↥S₂) (s : ↥S₁), (↑s : R) • (↑x₁.2 : R) • (↑c : R) • x₂.1 = (↑s : R) • (↑x₂.2 : R) • (↑c : R) • x₁.1
Tactic: simp only [Function.uncurry, liftOfLE_mk', mk'_eq_mk'_iff,
      Submonoid.smul_def, ← mk'_smul] at e ⊢
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst_13 : AddCommMonoid M₁
inst_14 : AddCommMonoid M₂
inst_15 : Module R M₁
inst_16 : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst_17 : IsLocalizedModule S₁ f₁
inst_18 : IsLocalizedModule S₂ f₂
x₁ x₂ : Prod.{u_2, u_1} M ↥S₁
e : ∃ (s : ↥S₂), (↑s : R) • (↑x₁.2 : R) • x₂.1 = (↑s : R) • (↑x₂.2 : R) • x₁.1
⊢ ∃ (c : ↥S₂) (s : ↥S₁), (↑s : R) • (↑x₁.2 : R) • (↑c : R) • x₂.1 = (↑s : R) • (↑x₂.2 : R) • (↑c : R) • x₁.1
have obtain : ∀ (c : ↥S₂) (e : (↑c : R) • (↑x₁.2 : R) • x₂.1 = (↑c : R) • (↑x₂.2 : R) • x₁.1),
  ∃ (c : ↥S₂) (s : ↥S₁), (↑s : R) • (↑x₁.2 : R) • (↑c : R) • x₂.1 = (↑s : R) • (↑x₂.2 : R) • (↑c : R) • x₁.1
Tactic: obtain ⟨c, e⟩ := e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
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
N : Type u_6
inst_6 : AddCommMonoid N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ {x y : M},
    Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
        ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N) →
      Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
a b : M'
hab : Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) a : N) ((g : (a : M') → N) b : N)
⊢ a = b
have obtain : ∀ (x : M) (m : ↥S) (hxm : m • a = (f : (a : M) → M') x), a = b
Tactic: obtain ⟨⟨x, m⟩, (hxm : m • a = f x)⟩ := IsLocalizedModule.surj S f a