awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 : s • IsLocalization.mk' A x s • t • mk' f m t = (fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t))
⊢ 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:
conv_lhs => simp only [smul_assoc, mul_smul, smul_comm t]

Premises used: smul_assoc, SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 :
  (↑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')
⊢ s • IsLocalization.mk' A x s • t • mk' f m t = (fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t))

Tactic:
simp only [mk'_cancel', map_smul, Submonoid.smul_def s]

Premises used: IsLocalizedModule.mk'_cancel', Submonoid.smul_def, map_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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')
a₂ a₃ : HSMul.hSMul (β := M') x ((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')

Tactic:
rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]

Premises used: smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M') ↔ ∃ (s' : ↥S), s' • m = 0

Tactic:
(mk'_eq_zero (1 : S)).symm.trans (mk'_eq_zero' f _)

Premises used: IsLocalizedModule.mk'_eq_zero', Iff.trans, OfNat.ofNat, IsLocalizedModule.mk'_eq_zero, Iff.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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'
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
⊢ ∃ (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

Premises used: IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x : M'
m : M
s : ↥S
e : s • x = (f : (a : M) → M') m
⊢ ∃ (a : Prod.{u_2, u_1} M ↥S), Function.uncurry (mk' f) a = x

Tactic:
⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩

Premises used: Iff.mpr, Prod.mk, Exists.intro, Eq.symm, IsLocalizedModule.mk'_eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
x : M'
m : M
s : ↥S
e : s • x = (f : (a : M) → M') m
⊢ ∃ (a : Prod.{u_2, u_1} M ↥S), Function.uncurry (mk' f) a = x

Tactic:
exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂
⊢ liftOfLE S₁ S₂ h f₁ f₂ ∘ₗ f₁ = f₂

Tactic:
lift_comp ..

Premises used: IsLocalizedModule.lift_comp, IsLocalizedModule.liftOfLE
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂
x : M
⊢ Eq.{u_6 + 1} (α := M₂) ((liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) ((f₁ : (a : M) → M₁) x : M₁) : M₂)
    ((f₂ : (a : M) → M₂) x : M₂)

Tactic:
lift_apply ..

Premises used: IsLocalizedModule.lift_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
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) ⋯) : 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₂)
⊢ (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) ⋯)

Tactic:
apply ((Module.End.isUnit_iff _).mp (map_units f₂ ⟨s, h s.2⟩)).1

Premises used: Module.End.isUnit_iff, Subtype.mk, And.left, Iff.mp, IsLocalizedModule.map_units, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
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) ⋯)
⊢ 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₂)

Tactic:
simp only [Module.algebraMap_end_apply, ← map_smul, ← Submonoid.smul_def, mk'_cancel']

Premises used: IsLocalizedModule.mk'_cancel', Submonoid.smul_def, Module.algebraMap_end_apply, map_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
a : (f₂ : (a : M) → M₂) m = s • mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯)
⊢ (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) ⋯)

Tactic:
rw [liftOfLE, lift_apply]

Premises used: IsLocalizedModule.liftOfLE, IsLocalizedModule.lift_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
⊢ (f₂ : (a : M) → M₂) m = s • mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯)

Tactic:
(mk'_cancel' (S := S₂) f₂ m ⟨s.1, h s.2⟩).symm

Premises used: IsLocalizedModule.mk'_cancel', Subtype.mk, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
⊢ (f₂ : (a : M) → M₂) m = s • mk' f₂ m (Subtype.mk (p := fun (x : R) ↦ x ∈ S₂) (↑s : R) ⋯)

Tactic:
exact (mk'_cancel' (S := S₂) f₂ m ⟨s.1, h s.2⟩).symm

Premises used: IsLocalizedModule.mk'_cancel', Subtype.mk, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂
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
⊢ ∃ (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

Premises used: IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂
y' : M
s : ↥S₂
e : (y', s).2 • y = (f₂ : (a : M) → M₂) (y', s).1
⊢ (((f₁ : (a : M) → M₁) y', s) : Prod.{u_6, u_1} M₁ ↥S₂).2 • y =
    (liftOfLE S₁ S₂ h f₁ f₂ : (a : M₁) → M₂) (((f₁ : (a : M) → M₁) y', s).1 : M₁)

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂
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:
exact ⟨⟨f₁ y', s⟩, by simpa⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂)
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₂
⊢ ∃ (c : ↥S₂), c • x₁ = c • x₂

Tactic:
obtain ⟨x₁, s₁, rfl⟩ := mk'_surjective S₁ f₁ x₁

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂)
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₂
⊢ ∃ (c : ↥S₂), c • Function.uncurry (mk' f₁) x₁ = c • x₂

Tactic:
obtain ⟨x₂, s₂, rfl⟩ := mk'_surjective S₁ f₁ x₂

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂)
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
⊢ ∃ (c : ↥S₂), c • Function.uncurry (mk' f₁) x₁ = c • Function.uncurry (mk' f₁) x₂

Tactic:
simp only [Function.uncurry, liftOfLE_mk', mk'_eq_mk'_iff,
      Submonoid.smul_def, ← mk'_smul] at e ⊢

Premises used: IsLocalizedModule.liftOfLE_mk', IsLocalizedModule.mk'_eq_mk'_iff, Submonoid.smul_def, IsLocalizedModule.mk'_smul, Function.uncurry
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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
⊢ ∃ (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
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
c : ↥S₂
e : (↑c : R) • (↑x₁.2 : R) • x₂.1 = (↑c : R) • (↑x₂.2 : R) • x₁.1
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑1 : R) ((↑x₁.2 : R) • (↑c : R) • x₂.1) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑1 : R) ((↑x₂.2 : R) • (↑c : R) • x₁.1)

Tactic:
simpa [← smul_comm c.1]

Premises used: SMulCommClass.smul_comm, Subtype.val
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₁
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:
exact ⟨c, 1, by simpa [← smul_comm c.1]⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
obtain : ∀ (x : M) (m : ↥S) (hxm : m • a = (f : (a : M) → M') x), a = b
⊢ a = b

Tactic:
obtain ⟨⟨x, m⟩, (hxm : m • a = f x)⟩ := IsLocalizedModule.surj S f a

Premises used: IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
obtain : ∀ (y : M) (n : ↥S) (hym : n • b = (f : (a : M) → M') y), a = b
⊢ a = b

Tactic:
obtain ⟨⟨y, n⟩, (hym : n • b = f y)⟩ := IsLocalizedModule.surj S f b

Premises used: IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
x : M
m : ↥S
hxm : m • a = (f : (a : M) → M') x
y : M
n : ↥S
hym : n • b = (f : (a : M) → M') y
h :
  Eq.{u_6 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') ((↑n : R) • x) : M') : N)
    ((g : (a : M') → N) ((f : (a : M) → M') ((↑m : R) • y) : M') : N)
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑n : R) • x) : M') ((f : (a : M) → M') ((↑m : R) • y) : M')

Tactic:
apply H at h