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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
obtain :
  ∀ (p : M) (s : ↥S) (h : (p, s).2 • x = (f : (a : M) → M') (p, s).1),
    ∃ (x_1 : Prod.{u_4, u_1} M'' ↥S), x_1.2 • x = (f ∘ₗ (↑e : M'' →ₗ[R] M) : (a : M'') → M') x_1.1
⊢ ∃ (x_1 : Prod.{u_4, u_1} M'' ↥S), x_1.2 • x = (f ∘ₗ (↑e : M'' →ₗ[R] M) : (a : M'') → M') x_1.1

Tactic:
obtain ⟨⟨p, s⟩, h⟩ := hf.surj 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
p : M
s : ↥S
h : (p, s).2 • x = (f : (a : M) → M') (p, s).1
⊢ (((e.symm : (a : M) → M'') p, s) : Prod.{u_4, u_1} M'' ↥S).2 • x =
    (f ∘ₗ (↑e : M'' →ₗ[R] M) : (a : M'') → M') (((e.symm : (a : M) → M'') p, s).1 : M'')

Tactic:
simpa using h
-- 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''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
p : M
s : ↥S
h : (p, s).2 • x = (f : (a : M) → M') (p, s).1
⊢ ∃ (x_1 : Prod.{u_4, u_1} M'' ↥S), x_1.2 • x = (f ∘ₗ (↑e : M'' →ₗ[R] M) : (a : M'') → M') x_1.1

Tactic:
exact ⟨⟨e.symm p, s⟩, by simpa using h⟩
-- 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''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁ x₂ : M''
h :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((e : (a : M'') → M) x₁ : M) : M')
    ((f : (a : M) → M') ((e : (a : M'') → M) x₂ : M) : M')
obtain :
  ∀ (c : ↥S)
    (hc : HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₁ : M) = HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₂ : M)),
    ∃ (c : ↥S), c • x₁ = c • x₂
⊢ ∃ (c : ↥S), c • x₁ = c • x₂

Tactic:
obtain ⟨c, hc⟩ := hf.exists_of_eq h

Premises used: IsLocalizedModule.exists_of_eq
-- 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''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁ x₂ : M''
h :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((e : (a : M'') → M) x₁ : M) : M')
    ((f : (a : M) → M') ((e : (a : M'') → M) x₂ : M) : M')
c : ↥S
hc : HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₁ : M) = HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₂ : M)
⊢ c • x₁ = c • x₂

Tactic:
simpa only [Submonoid.smul_def, map_smul, e.symm_apply_apply]
      using congr(e.symm $hc)

Premises used: LinearEquiv.symm_apply_apply, 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
A : Type u_5
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : Module A M'
inst_7 : IsLocalization S A
inst_8 : Module R M
inst_9 : Module R M'
inst_10 : Module R M''
inst_11 : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁ x₂ : M''
h :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((e : (a : M'') → M) x₁ : M) : M')
    ((f : (a : M) → M') ((e : (a : M'') → M) x₂ : M) : M')
c : ↥S
hc : HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₁ : M) = HSMul.hSMul (β := M) c ((e : (a : M'') → M) x₂ : M)
⊢ ∃ (c : ↥S), c • x₁ = c • x₂

Tactic:
exact ⟨c, by simpa only [Submonoid.smul_def, map_smul, e.symm_apply_apply]
      using congr(e.symm $hc)⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
inst_5 : IsLocalization S R'
inst_6 : Module R' M
inst_7 : IsScalarTower R R' M
s : ↥S
rw :
  IsUnit.{u_2} (M := End R M)
    ((Algebra.lsmul R R M : (a : R') → End R M) ((algebraMap R R' : (a : R) → R') (↑s : R)) : End R M)
⊢ IsUnit.{u_2} (M := End R M) ((algebraMap R (End R M) : (a : R) → End R M) (↑s : R) : End R M)

Tactic:
rw [← (Algebra.lsmul R (A := R') R M).commutes]

Premises used: Algebra.lsmul, AlgHom.commutes
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
inst_5 : IsLocalization S R'
inst_6 : Module R' M
inst_7 : IsScalarTower R R' M
s : ↥S
⊢ IsUnit.{u_2} (M := End R M)
    ((Algebra.lsmul R R M : (a : R') → End R M) ((algebraMap R R' : (a : R) → R') (↑s : R)) : End R M)

Tactic:
(IsLocalization.map_units R' s).map _

Premises used: IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
inst_5 : IsLocalization S R'
inst_6 : Module R' M
inst_7 : IsScalarTower R R' M
s : ↥S
⊢ IsUnit.{u_2} (M := End R M)
    ((Algebra.lsmul R R M : (a : R') → End R M) ((algebraMap R R' : (a : R) → R') (↑s : R)) : End R M)

Tactic:
exact (IsLocalization.map_units R' s).map _

Premises used: IsLocalization.map_units, IsUnit.map
-- 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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : c • (m', s').2 • (m, s).1 = c • (m, s).2 • (m', s').1
dsimp :
  Eq (α := M'')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R)) ⋯)⁻¹ : End R M'') :
          (a : M'') → M'')
        ((g : (a : M) → M'') m : M'') :
      M'')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s' : R)) ⋯)⁻¹ : End R M'') :
          (a : M'') → M'')
        ((g : (a : M) → M'') m' : M'') :
      M'')
⊢ Eq.{u_4 + 1} (α := M'')
    ((fun (p : Prod.{u_2, u_1} M ↥S) ↦
        (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑p.2 : R)) ⋯)⁻¹ : End R M'') :
              (a : M'') → M'')
            ((g : (a : M) → M'') p.1 : M'') :
          M''))
      (m, s))
    ((fun (p : Prod.{u_2, u_1} M ↥S) ↦
        (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑p.2 : R)) ⋯)⁻¹ : End R M'') :
              (a : M'') → M'')
            ((g : (a : M) → M'') p.1 : M'') :
          M''))
      (m', s'))

Tactic:
dsimp only
-- 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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
rw :
  HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')
⊢ Eq (α := M'')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s : R)) ⋯)⁻¹ : End R M'') :
          (a : M'') → M'')
        ((g : (a : M) → M'') m : M'') :
      M'')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑s' : R)) ⋯)⁻¹ : End R M'') :
          (a : M'') → M'')
        ((g : (a : M) → M'') m' : M'') :
      M'')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, eq_comm,
      Module.End.algebraMap_isUnit_inv_apply_eq_iff]

Premises used: eq_comm, Module.End.algebraMap_isUnit_inv_apply_eq_iff, 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
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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
⊢ c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')

Tactic:
simp only [Submonoid.smul_def, ← g.map_smul, eq1]

Premises used: Submonoid.smul_def, LinearMap.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
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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
⊢ c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')

Tactic:
have : c • s • g m' = c • s' • g m := by
      simp only [Submonoid.smul_def, ← g.map_smul, eq1]
-- 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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
⊢ IsUnit ⋯.unit.inv

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
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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
⊢ Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')

Tactic:
have : Function.Injective (h c).unit.inv := ((Module.End.isUnit_iff _).1 (by simp)).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
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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
apply_fun :
  Eq (α := M'')
    ((⋯.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')) : M'')
    ((⋯.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) : M'')
⊢ HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')

Tactic:
apply_fun (h c).unit.inv

Premises used: IsUnit.unit, Units.inv
-- 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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M''))
⊢ Eq (α := M'')
    ((⋯.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')) : M'')
    ((⋯.unit.inv : (a : M'') → M'') (HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) : M'')

Tactic:
rw [Units.inv_eq_val_inv, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ←
      (h c).unit⁻¹.val.map_smul]

Premises used: Units.val, Units.inv_eq_val_inv, Inv.inv, LinearMap.map_smul, IsUnit.unit, Module.End.algebraMap_isUnit_inv_apply_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
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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
symm :
  ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
⊢ HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'') =
    ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M''))

Tactic:
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
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 g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m_1 : LocalizedModule S M
x x_1 : Prod.{u_2, u_1} M ↥S
m : M
s : ↥S
m' : M
s' : ↥S
h_1 : (m, s) ≈ (m', s')
c : ↥S
eq1 : (↑c : R) • (↑s' : R) • m = (↑c : R) • (↑s : R) • m'
this_1 :
  c • HSMul.hSMul (β := M'') s ((g : (a : M) → M'') m' : M'') =
    c • HSMul.hSMul (β := M'') s' ((g : (a : M) → M'') m : M'')
this : Function.Injective (α := M'') (β := M'') (⇑⋯.unit.inv : (a : M'') → M'')
rw :
  (↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₁ :
  HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m', s').2 : R) • m) : M'') =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₂ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    (↑c : R) • HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')
rw₃ :
  (g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) =
    HSMul.hSMul (β := M'') (↑c : R) ((g : (a : M) → M'') ((↑(m, s).2 : R) • m') : M'')
rw₄ :
  Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') ((↑c : R) • (↑(m', s').2 : R) • m) : M'')
    ((g : (a : M) → M'') ((↑c : R) • (↑(m, s).2 : R) • m') : M'')
rw₅ rw₆ :
  Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') ((↑c : R) • (↑s : R) • m') : M'')
    ((g : (a : M) → M'') ((↑c : R) • (↑(m, s).2 : R) • m') : M'')
⊢ ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
      ((↑c : R) • HSMul.hSMul (β := M'') (↑(m', s').2 : R) ((g : (a : M) → M'') m : M'')) =
    HSMul.hSMul (β := M'') (↑(m, s).2 : R) ((g : (a : M) → M'') m' : M'')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ←
      g.map_smul, eq1]

Premises used: LinearMap.map_smul, Module.End.algebraMap_isUnit_inv_apply_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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
m : M
s : ↥S
⊢ lift' S g h (mk m s) = ((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') m : M'')

Tactic:
rfl

Premises used: LocalizedModule.liftOn, LocalizedModule.lift', 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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
rw :
  ((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑(b * b') : R)) ⋯)⁻¹ : End R M'') :
        (a : M'') → M'')
      ((g : (a : M) → M'') (b' • a + b • a') : M'') =
    HAdd.hAdd (α := M'') (β := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a' : M'') : M'')
⊢ lift' S g h (HAdd.hAdd (α := LocalizedModule S M) (mk a b) (mk a' b')) = lift' S g h (mk a b) + lift' S g h (mk a' b')

Tactic:
rw [mk_add_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk]

Premises used: LocalizedModule.mk_add_mk, LocalizedModule.lift'_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_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M''
inst_3 : Module R M
inst_4 : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
rw :
  HAdd.hAdd (α := M'') (β := M'') ((g : (a : M) → M'') (b' • a) : M'') ((g : (a : M) → M'') (b • a') : M'') =
    HAdd.hAdd (α := M'') (β := M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
          (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
        M'')
⊢ ((↑(IsUnit.unit (a := (algebraMap R (End R M'') : (a : R) → End R M'') (↑(b * b') : R)) ⋯)⁻¹ : End R M'') :
        (a : M'') → M'')
      ((g : (a : M) → M'') (b' • a + b • a') : M'') =
    HAdd.hAdd (α := M'') (β := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'')
      (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a' : M'') : M'')

Tactic:
rw [map_add, Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul,
        ← map_smul, ← map_smul]

Premises used: map_add, smul_add, Module.End.algebraMap_isUnit_inv_apply_eq_iff, map_smul