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'
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_3 + 1} (α := M') ((f : (a : M) → M') ((↑n : R) • x) : M') ((f : (a : M) → M') ((↑m : R) • y) : M')
⊢ HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')

Tactic:
rw [map_smul, map_smul] at h

Premises used: 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'
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 :
  HSMul.hSMul (β := M') (↑n : R) ((f : (a : M) → M') x : M') =
    HSMul.hSMul (β := M') (↑m : R) ((f : (a : M) → M') y : M')
rwa : (n * m) • a = (n * m) • b
rwa₁ : n • m • a = (n * m) • b
rwa₂ : n • m • a = (m * n) • b
rwa₃ : n • m • a = m • n • b
rwa₄ : HSMul.hSMul (β := M') n ((f : (a : M) → M') x : M') = m • n • b
rwa₅ rwa₆ rwa₇ rwa₈ :
  HSMul.hSMul (β := M') n ((f : (a : M) → M') x : M') = HSMul.hSMul (β := M') m ((f : (a : M) → M') y : M')
⊢ a = b

Tactic:
rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]

Premises used: HMul.hMul, IsLocalizedModule.smul_inj, mul_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'
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
suffices :
  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)
⊢ a = b

Tactic:
suffices h : g (f (n.val • x)) = g (f (m.val • y)) by
    apply H at h
    rw [map_smul, map_smul] at h
    rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]
-- 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
⊢ 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)

Tactic:
simp [← hxm, ← hym, hab, ← S.smul_def, ← mul_smul, mul_comm, ← mul_smul]

Premises used: Submonoid.smul_def, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
⊢ Function.Injective.{u_7 + 1, u_8 + 1} (α := M') (β := N) (⇑g : (a : M') → N)

Tactic:
IsLocalizedModule.injective_of_map_eq S f (fun hxy ↦ ?_)

Premises used: IsLocalizedModule.injective_of_map_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
refine :
  ∀ {x y : M}
    (hxy :
      Eq.{u_8 + 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_7 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')
⊢ Function.Injective.{u_7 + 1, u_8 + 1} (α := M') (β := N) (⇑g : (a : M') → N)

Tactic:
refine IsLocalizedModule.injective_of_map_eq S f (fun hxy ↦ ?_)

Premises used: IsLocalizedModule.injective_of_map_eq
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
x y : M
hxy :
  Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
    ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N)
rw : Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') (x - y) : M') (0 : M')
⊢ Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') x : M') ((f : (a : M) → M') y : M')

Tactic:
rw [← sub_eq_zero, ← map_sub]

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
x y : M
hxy :
  Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') x : M') : N)
    ((g : (a : M') → N) ((f : (a : M) → M') y : M') : N)
a : Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') (x - y) : M') : N) (0 : N)
⊢ Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') (x - y) : M') (0 : M')

Tactic:
apply H
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
N : Type u_8
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : AddCommGroup N
inst_7 : Module R N
g : M' →ₗ[R] N
H :
  ∀ (m : M),
    Eq.{u_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') m : M') : N) (0 : N) →
      Eq.{u_7 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
x y : M
hxy :
  Eq.{u_8 + 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_8 + 1} (α := N) ((g : (a : M') → N) ((f : (a : M) → M') (x - y) : M') : N) (0 : N)

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- 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_1 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid N'
inst_15 : Module R N
inst_16 : Module R N'
g : N →ₗ[R] N'
inst_17 : IsLocalizedModule S g
h₁ h₂ : M →ₗ[R] N
h : lift S f (g ∘ₗ (h₁ + h₂)) ⋯ ∘ₗ f = (lift S f (g ∘ₗ h₁) ⋯ + lift S f (g ∘ₗ h₂) ⋯) ∘ₗ f
⊢ lift S f (g ∘ₗ (h₁ + h₂)) ⋯ = lift S f (g ∘ₗ h₁) ⋯ + lift S f (g ∘ₗ h₂) ⋯

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Premises used: IsLocalizedModule.ext, IsLocalizedModule.map_units
-- 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_1 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid N'
inst_15 : Module R N
inst_16 : Module R N'
g : N →ₗ[R] N'
inst_17 : IsLocalizedModule S g
h₁ h₂ : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (h₁ + h₂)) ⋯ ∘ₗ f = (lift S f (g ∘ₗ h₁) ⋯ + lift S f (g ∘ₗ h₂) ⋯) ∘ₗ f

Tactic:
simp only [lift_comp, LinearMap.add_comp, LinearMap.comp_add]

Premises used: IsLocalizedModule.lift_comp, LinearMap.add_comp, LinearMap.comp_add
-- 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_1 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid N'
inst_15 : Module R N
inst_16 : Module R N'
g : N →ₗ[R] N'
inst_17 : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
h₁ :
  lift S f (g ∘ₗ (r • h)) ⋯ ∘ₗ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift S f (g ∘ₗ h) ⋯) ∘ₗ f
⊢ lift S f (g ∘ₗ (r • h)) ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift S f (g ∘ₗ h) ⋯)

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Premises used: IsLocalizedModule.ext, IsLocalizedModule.map_units
-- 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_1 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
N : Type u_6
N' : Type u_7
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid N'
inst_15 : Module R N
inst_16 : Module R N'
g : N →ₗ[R] N'
inst_17 : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ ∘ₗ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift S f (g ∘ₗ h) ⋯) ∘ₗ f

Tactic:
simp only [lift_comp, LinearMap.smul_comp, LinearMap.comp_smul, RingHom.id_apply]

Premises used: LinearMap.smul_comp, RingHom.id_apply, IsLocalizedModule.lift_comp, LinearMap.comp_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
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
⊢ (map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h ∘ₗ f = g ∘ₗ h

Tactic:
lift_comp S f (g ∘ₗ h) (IsLocalizedModule.map_units g)

Premises used: IsLocalizedModule.lift, IsLocalizedModule.lift_comp, LinearMap.comp, IsLocalizedModule.map_units
-- 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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
⊢ Eq.{u_7 + 1} (α := N')
    ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') ((f : (a : M) → M') x : M') : N')
    ((g : (a : N) → N') ((h : (a : M) → N) x : N) : N')

Tactic:
lift_apply S f (g ∘ₗ h) (IsLocalizedModule.map_units g) x

Premises used: LinearMap.comp, IsLocalizedModule.lift_apply, IsLocalizedModule.map_units
-- 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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
simp :
  (LocalizedModule.lift S (g ∘ₗ h) ⋯ : (a : LocalizedModule S M) → N')
      (((iso S f).symm : (a : M') → LocalizedModule S M) (mk' f x s) : LocalizedModule S M) =
    mk' g ((h : (a : M) → N) x) s
⊢ (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') (mk' f x s) =
    mk' g ((h : (a : M) → N) x) s

Tactic:
simp only [map, lift, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_apply]

Premises used: LinearMap.coe_mk, IsLocalizedModule.lift, LinearMap.coe_comp, IsLocalizedModule.map, Function.comp_apply, AddHom.coe_mk, LinearEquiv.coe_coe
-- 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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
rw : ((↑⋯.unit⁻¹ : End R N') : (a : N') → N') ((g ∘ₗ h : (a : M) → N') x : N') = mk' g ((h : (a : M) → N) x) s
⊢ (LocalizedModule.lift S (g ∘ₗ h) ⋯ : (a : LocalizedModule S M) → N')
      (((iso S f).symm : (a : M') → LocalizedModule S M) (mk' f x s) : LocalizedModule S M) =
    mk' g ((h : (a : M) → N) x) s

Tactic:
rw [iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s), LocalizedModule.lift_mk]

Premises used: IsLocalizedModule.iso_symm_apply', IsLocalizedModule.mk'_cancel', LocalizedModule.lift_mk, IsLocalizedModule.mk'
-- 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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ ((↑⋯.unit⁻¹ : End R N') : (a : N') → N') ((g ∘ₗ h : (a : M) → N') x : N') = mk' g ((h : (a : M) → N) x) s

Tactic:
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
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
h :
  ∀ (x : M'),
    Eq (α := M') ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M') x : M')
      ((LinearMap.id : (a : M') → M') x : M')
⊢ Eq.{u_3 + 1} (α := M' →ₗ[R] M') ((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M')
    (LinearMap.id : M' →ₗ[R] M')

Tactic:
ext x
-- 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'
h :
  ∀ (x : M) (s : ↥S),
    Eq (α := M')
      ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M')
          (Function.uncurry (mk' f) (x, s)) :
        M')
      ((LinearMap.id : (a : M') → M') (Function.uncurry (mk' f) (x, s)) : M')
⊢ Eq (α := M') ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M') x : M')
    ((LinearMap.id : (a : M') → M') x : M')

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.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
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
s : ↥S
⊢ Eq (α := M')
    ((((map S f f : (a : M →ₗ[R] M) → M' →ₗ[R] M') LinearMap.id : M' →ₗ[R] M') : (a : M') → M')
        (Function.uncurry (mk' f) (x, s)) :
      M')
    ((LinearMap.id : (a : M') → M') (Function.uncurry (mk' f) (x, s)) : M')

Tactic:
simp
-- 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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x y : M'
obtain :
  ∀ (x : M) (s : ↥S),
    Eq.{u_7 + 1} (α := N')
        ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
            (Function.uncurry (mk' f) (x, s)) :
          N')
        ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') y : N') →
      Function.uncurry (mk' f) (x, s) = y
⊢ Eq.{u_7 + 1} (α := N') ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') x : N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') y : N') →
    x = y

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.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
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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
y : M'
x : M
s : ↥S
obtain :
  ∀ (y : M) (t : ↥S),
    Eq.{u_7 + 1} (α := N')
        ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
            (Function.uncurry (mk' f) (x, s)) :
          N')
        ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
            (Function.uncurry (mk' f) (y, t)) :
          N') →
      Function.uncurry (mk' f) (x, s) = Function.uncurry (mk' f) (y, t)
⊢ Eq.{u_7 + 1} (α := N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (x, s)) :
        N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') y : N') →
    Function.uncurry (mk' f) (x, s) = y

Tactic:
obtain ⟨⟨y, t⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y

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
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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : M
s : ↥S
y : M
t : ↥S
simp :
  ∀ x_1 ∈ S,
    x_1 • HSMul.hSMul (β := N) s ((h : (a : M) → N) y : N) = x_1 • HSMul.hSMul (β := N) t ((h : (a : M) → N) x : N) →
      ∃ a ∈ S, a • s • y = a • t • x
⊢ Eq.{u_7 + 1} (α := N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (x, s)) :
        N')
      ((((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N')
          (Function.uncurry (mk' f) (y, t)) :
        N') →
    Function.uncurry (mk' f) (x, s) = Function.uncurry (mk' f) (y, t)

Tactic:
simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_mk'_iff, Subtype.exists,
    Submonoid.mk_smul, exists_prop, forall_exists_index, and_imp]

Premises used: and_imp, IsLocalizedModule.mk'_eq_mk'_iff, Subtype.exists, forall_exists_index, Submonoid.mk_smul, exists_prop, IsLocalizedModule.map_mk', Function.uncurry_apply_pair
-- 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
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : M
s : ↥S
y : M
t : ↥S
c : R
hc : c ∈ S
e : c • HSMul.hSMul (β := N) s ((h : (a : M) → N) y : N) = c • HSMul.hSMul (β := N) t ((h : (a : M) → N) x : N)
⊢ Eq.{u_6 + 1} (α := N) ((h : (a : M) → N) (c • s • y) : N) ((h : (a : M) → N) (c • t • x) : N)

Tactic:
simpa