awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
left :
  Function.Injective.{u_4 + 1, u_4 + 1} (α := ↥(localized₀ p f M')) (β := ↥(localized₀ p f M'))
    (⇑((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
          Module.End R ↥(localized₀ p f M')) :
      (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
right :
  Function.Surjective.{u_4 + 1, u_4 + 1} (α := ↥(localized₀ p f M')) (β := ↥(localized₀ p f M'))
    (⇑((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
          Module.End R ↥(localized₀ p f M')) :
      (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
⊢ Function.Bijective.{u_4 + 1, u_4 + 1} (α := ↥(localized₀ p f M')) (β := ↥(localized₀ p f M'))
    (⇑((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
          Module.End R ↥(localized₀ p f M')) :
      (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := ↥(localized₀ p f M')) (β := ↥(localized₀ p f M'))
    (⇑((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
          Module.End R ↥(localized₀ p f M')) :
      (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))

Tactic:
fun _ _ e ↦ Subtype.ext
        (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))

Premises used: congr_arg, IsLocalizedModule.smul_injective, Function.Injective, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := ↥(localized₀ p f M')) (β := ↥(localized₀ p f M'))
    (⇑((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
          Module.End R ↥(localized₀ p f M')) :
      (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))

Tactic:
exact fun _ _ e ↦ Subtype.ext
        (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))

Premises used: IsLocalizedModule.smul_injective, Subtype.ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
m : M
hm : m ∈ M'
s : ↥p
⊢ ∃ (a : ↥(localized₀ p f M')),
    Eq (α := ↥(localized₀ p f M'))
      ((((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
              Module.End R ↥(localized₀ p f M')) :
            (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
          a :
        ↥(localized₀ p f M'))
      (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯ : ↥(localized₀ p f M'))

Tactic:
⟨⟨IsLocalizedModule.mk' f m (s * x), ⟨_, hm, _, rfl⟩⟩, Subtype.ext ?_⟩

Premises used: HMul.hMul, Subtype.mk, And.intro, Exists.intro, rfl, IsLocalizedModule.mk', Subtype.ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
m : M
hm : m ∈ M'
s : ↥p
right :
  (↑((((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
              Module.End R ↥(localized₀ p f M')) :
            (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
⊢ ∃ (a : ↥(localized₀ p f M')),
    Eq (α := ↥(localized₀ p f M'))
      ((((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
              Module.End R ↥(localized₀ p f M')) :
            (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
          a :
        ↥(localized₀ p f M'))
      (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯ : ↥(localized₀ p f M'))

Tactic:
refine ⟨⟨IsLocalizedModule.mk' f m (s * x), ⟨_, hm, _, rfl⟩⟩, Subtype.ext ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
m : M
hm : m ∈ M'
s : ↥p
right :
  (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (↑x : R)
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₁ :
  (↑x : R) • (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₂ :
  IsLocalizedModule.mk' f ((↑x : R) • m) (s * x) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₃ :
  IsLocalizedModule.mk' f (x • m) (s * x) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₄ right₅ :
  IsLocalizedModule.mk' f m s =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
⊢ (↑((((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
              Module.End R ↥(localized₀ p f M')) :
            (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)

Tactic:
rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]

Premises used: Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right, Module.algebraMap_end_apply, SetLike.val_smul_of_tower, IsLocalizedModule.mk'_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
a :
  (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).2
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f x s) ⋯)) :
      N) =
    (↑(((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
            (a : ↥M') → ↥(localized₀ p f M'))
          (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).1) :
      N)
⊢ HSMul.hSMul (β := ↥(localized₀ p f M')) (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).2
      (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f x s) ⋯) =
    ((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
        (a : ↥M') → ↥(localized₀ p f M'))
      (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).1

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
⊢ (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).2
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f x s) ⋯)) :
      N) =
    (↑(((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
            (a : ↥M') → ↥(localized₀ p f M'))
          (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).1) :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
⊢ ∃ (x_1 : Prod.{u_3, u_1} ↥M' ↥p),
    HSMul.hSMul (β := ↥(localized₀ p f M')) x_1.2
        (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f x s) ⋯) =
      ((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
          (a : ↥M') → ↥(localized₀ p f M'))
        x_1.1

Tactic:
exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x₁ x₂ : ↥M'
e :
  Eq.{u_4 + 1} (α := ↥(localized₀ p f M'))
    (((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
          (a : ↥M') → ↥(localized₀ p f M'))
        x₁ :
      ↥(localized₀ p f M'))
    (((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
          (a : ↥M') → ↥(localized₀ p f M'))
        x₂ :
      ↥(localized₀ p f M'))
⊢ ∃ (c : ↥p), c • x₁ = c • x₂

Tactic:
simpa [Subtype.ext_iff] using
      IsLocalizedModule.exists_of_eq (S := p) (f := f) (congr_arg Subtype.val e)

Premises used: Subtype.ext_iff, congr_arg, IsLocalizedModule.exists_of_eq, Subtype.val
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ IsLocalizedModule (M' := ↥(localized' S p f M')) p (toLocalized' S p f M')

Tactic:
inferInstanceAs (IsLocalizedModule p (M'.toLocalized₀ p f))

Premises used: _private.0.Submodule.isLocalizedModule._proof_1
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f a r ∈ localized₀ p f Q

Tactic:
⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, And.intro, Exists.intro, HSMul.hSMul, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
refine : IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r
⊢ IsLocalizedModule.mk' f a r ∈ localized₀ p f Q

Tactic:
refine ⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
⊢ LE.le (α := Submodule S N) (localized' S p f P) (localized' S p f Q)

Tactic:
localized₀_le_localized₀_of_smul_le p f x h

Premises used: Set.Mem, Submodule.localized₀_le_localized₀_of_smul_le
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' (S := p) f x 1 = (f : (a : M) → N) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
x : M
⊢ Eq.{u_8 + 1} (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (((toLocalizedQuotient' S p f M' :
            LinearMap.{u_5, u_5, u_7, u_8} (RingHom.id R) (M ⧸ M')
              (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : M ⧸ M') → N ⧸ localized' S p f M')
        (Quotient.mk x) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (Quotient.mk ((f : (a : M) → N) x) : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Submodule.restrictScalars, setOf, Submodule.localized', rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
rw : (↑x : R) • IsLocalization.mk' S 1 x • m = m
rw₁ : ((↑x : R) • IsLocalization.mk' S 1 x) • m = m
rw₂ : IsLocalization.mk' S (↑x : R) x • m = m
rw₃ : HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 m = m
rw₄ rw₅ : m = m
⊢ (((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : R) → Module.End R (N ⧸ localized' S p f M'))
            (↑x : R) :
          Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
      (IsLocalization.mk' S 1 x • m) =
    m

Tactic:
rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]

Premises used: smul_assoc, IsLocalization.mk'_self', one_smul, IsLocalization.smul_mk'_one, Module.algebraMap_end_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
refine :
  ∀ (m n : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    (e :
      Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
        ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                    (a : R) → Module.End R (N ⧸ localized' S p f M'))
                  (↑x : R) :
                Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
            m :
          HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
        ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                    (a : R) → Module.End R (N ⧸ localized' S p f M'))
                  (↑x : R) :
                Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
            n :
          HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))),
    m = n
⊢ IsUnit.{u_8} (M := Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')))
    ((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : R) → Module.End R (N ⧸ localized' S p f M'))
        (↑x : R) :
      Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')))

Tactic:
refine (Module.End.isUnit_iff _).mpr ⟨fun m n e ↦ ?_, fun m ↦ ⟨(IsLocalization.mk' S 1 x) • m,
      by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩

Premises used: Iff.mpr, Module.End.isUnit_iff, IsLocalization.mk', And.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e :
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                (a : R) → Module.End R (N ⧸ localized' S p f M'))
              (↑x : R) :
            Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                (a : R) → Module.End R (N ⧸ localized' S p f M'))
              (↑x : R) :
            Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
⊢ Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • (m - n))

Tactic:
simp only [Module.algebraMap_end_apply, ← mk_smul, Submodule.Quotient.eq, ← smul_sub] at e

Premises used: Submodule.Quotient.eq, Submodule.Quotient.mk_smul, smul_sub, Module.algebraMap_end_apply