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_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
e_a :
  Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b' • a) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
e_a₁ :
  Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b • a') : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
      M'')
⊢ 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'')

Tactic:
congr 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_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
e_a :
  Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
    ((g : (a : M) → M'') (b' • a) : M'')
⊢ Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b' • a) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : 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_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
e_a :
  Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
      M'')
    ((g : (a : M) → M'') (b • a') : M'')
⊢ Eq.{u_4 + 1} (α := M'') ((g : (a : M) → M'') (b • a') : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : 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_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
e_a : (g : (a : M) → M'') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M'') (↑b : R) ((g : (a : M) → M'') (b' • a) : M'')
⊢ Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') ((↑(b * b') : R) • a) : M'') : M'')
    ((g : (a : M) → M'') (b' • a) : M'')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff]

Premises used: 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'')
x y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
⊢ (g : (a : M) → M'') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M'') (↑b : R) ((g : (a : M) → M'') (b' • a) : M'')

Tactic:
simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]

Premises used: LinearMap.map_smul_of_tower, Submonoid.coe_mul
-- 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
e_a :
  (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')
e_a₁ e_a₂ :
  (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') a : M'')
⊢ HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a : M'') =
    (↑b : R) • HSMul.hSMul (β := M'') b' ((g : (a : M) → M'') a : M'')

Tactic:
rw [mul_smul, Submonoid.smul_def]

Premises used: Submonoid.smul_def, 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_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
e_a :
  Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a' : M'')) :
      M'')
    ((g : (a : M) → M'') (b • a') : M'')
⊢ Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') (↑(b * b') : R) ((g : (a : M) → M'') a' : M'')) :
      M'')
    ((g : (a : M) → M'') (b • a') : M'')

Tactic:
dsimp
-- 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
e_a :
  HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') ((↑b : R) • a') : M'') =
    HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') (b • a') : M'')
⊢ Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'')
        (HSMul.hSMul (β := M'') ((↑b : R) * (↑b' : R)) ((g : (a : M) → M'') a' : M'')) :
      M'')
    ((g : (a : M) → M'') (b • a') : M'')

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

Premises used: mul_comm, SemigroupAction.mul_smul, 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_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
⊢ HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') ((↑b : R) • a') : M'') =
    HSMul.hSMul (β := M'') (↑b' : R) ((g : (a : M) → M'') (b • a') : M'')

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_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'')
r : R
m : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))
rw₁ :
  HSMul.hSMul (β := M'') r (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') a : M'') : M'') =
    lift' S g h (mk (r • a) b)
rw₂ :
  HSMul.hSMul (β := M'') r (((↑⋯.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'') (r • a) : M'')
rw₃ :
  Eq (α := M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') (HSMul.hSMul (β := M'') r ((g : (a : M) → M'') a : M'')) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
rw₄ rw₅ :
  Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') (r • a) : M'') : M'')
⊢ r • lift' S g h (mk a b) = lift' S g h (HSMul.hSMul (β := LocalizedModule S M) r (mk a b))

Tactic:
rw [LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LocalizedModule.lift'_mk,
      ← map_smul, ← g.map_smul]

Premises used: LocalizedModule.lift'_mk, LocalizedModule.smul'_mk, LinearMap.map_smul, 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'')
r : R
x : LocalizedModule S M
rw : lift' S g h (r • x) = lift' S g h (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x)
rw₁ rw₂ : lift' S g h (r • x) = lift' S g h (r • x)
⊢ lift' S g h (r • x) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (lift' S g h x)

Tactic:
rw [LocalizedModule.lift'_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, LocalizedModule.lift'_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_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
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') (mk m s) : M'')
    (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → 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'')
m : M
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') (mk m 1) : M'') ((g : (a : M) → M'') m : M'')

Tactic:
simp [lift_mk]

Premises used: 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'')
h₁ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := M'') ((lift S g h ∘ₗ mkLinearMap S M : (a : M) → M'') x : M'') ((g : (a : M) → M'') x : M'')
⊢ lift S g h ∘ₗ mkLinearMap S M = g

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_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 : M
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h ∘ₗ mkLinearMap S M : (a : M) → M'') x : M'') ((g : (a : M) → M'') x : M'')

Tactic:
simp [LocalizedModule.lift_mk]

Premises used: 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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
h₁ :
  ∀ (x : LocalizedModule S M),
    Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') x : M'')
      ((l : (a : LocalizedModule S M) → M'') x : M'')
⊢ lift S g h = l

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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
x : LocalizedModule S M
h₁ :
  ∀ (m : M) (s : ↥S),
    Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') (mk m s) : M'')
      ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') x : M'')
    ((l : (a : LocalizedModule S M) → M'') x : M'')

Tactic:
induction x with | _ m s
-- 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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
h₁ :
  Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') m : M'') : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')
⊢ Eq.{u_4 + 1} (α := M'') ((lift S g h : (a : LocalizedModule S M) → M'') (mk m s) : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')

Tactic:
rw [LocalizedModule.lift_mk]

Premises used: 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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
h₁ :
  Eq.{u_4 + 1} (α := M'') ((l : (a : LocalizedModule S M) → M'') (mk m 1) : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk ((↑s : R) • m) s) : M'')
⊢ Eq (α := M'') (((↑⋯.unit⁻¹ : End R M'') : (a : M'') → M'') ((g : (a : M) → M'') m : M'') : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk m s) : M'')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
    Function.comp_apply, LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_mk]

Premises used: LocalizedModule.smul'_mk, LinearMap.coe_comp, LinearMap.map_smul, Function.comp_apply, LocalizedModule.mkLinearMap_apply, 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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
h₁ : Eq (α := LocalizedModule S M) (mk m 1) (mk ((↑s : R) • m) s)
⊢ Eq.{u_4 + 1} (α := M'') ((l : (a : LocalizedModule S M) → M'') (mk m 1) : M'')
    ((l : (a : LocalizedModule S M) → M'') (mk ((↑s : R) • m) s) : M'')

Tactic:
congr 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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
h₁ : ∃ (u : ↥S), u • s • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m)
⊢ Eq (α := LocalizedModule S M) (mk m 1) (mk ((↑s : R) • m) s)

Tactic:
rw [LocalizedModule.mk_eq]

Premises used: LocalizedModule.mk_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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ ∃ (u : ↥S), u • s • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m)

Tactic:
⟨1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- 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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 (s • m) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m))
⊢ ∃ (u : ↥S), u • s • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m)

Tactic:
refine ⟨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_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'')
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 (s • m) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 (HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 ((↑s : R) • m))

Tactic:
simp only [one_smul, Submonoid.smul_def]

Premises used: one_smul, Submonoid.smul_def
-- 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''
s : ↥S
p : LocalizedModule S M
m : M
s_1 : ↥S
⊢ Eq (α := LocalizedModule S M)
    ((((↑{ val := (algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R),
                  inv := LocalizedModule.divBy s, val_inv := ⋯, inv_val := ⋯ } :
              End R (LocalizedModule S M)) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (LocalizedModule.mk m s_1) :
      LocalizedModule S M)
    ((((algebraMap R (End R (LocalizedModule S M)) : (a : R) → End R (LocalizedModule S M)) (↑s : R) :
            End R (LocalizedModule S M)) :
          (a : LocalizedModule S M) → LocalizedModule S M)
        (LocalizedModule.mk m s_1) :
      LocalizedModule S M)

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
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''
p : LocalizedModule S M
m : M
t : ↥S
⊢ ∃ (x : Prod.{u_2, u_1} M ↥S),
    HSMul.hSMul (β := LocalizedModule S M) x.2 (LocalizedModule.mk m t) =
      (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x.1

Tactic:
⟨⟨m, t⟩, ?_⟩

Premises used: Prod.mk, Exists.intro
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
refine :
  HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
⊢ ∃ (x : Prod.{u_2, u_1} M ↥S),
    HSMul.hSMul (β := LocalizedModule S M) x.2 (LocalizedModule.mk m t) =
      (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x.1

Tactic:
refine ⟨⟨m, t⟩, ?_⟩
-- 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''
p : LocalizedModule S M
m : M
t : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M) (↑(m, t).2 : R) (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1
rw₁ :
  Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1)
rw₂ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((↑(m, t).2 : R) • m) t) (LocalizedModule.mk (m, t).1 1)
rw₃ : Eq (α := LocalizedModule S M) (LocalizedModule.mk ((m, t).2 • m) t) (LocalizedModule.mk (m, t).1 1)
rw₄ rw₅ : Eq (α := LocalizedModule S M) (LocalizedModule.mk m 1) (LocalizedModule.mk (m, t).1 1)
⊢ HSMul.hSMul (β := LocalizedModule S M) (m, t).2 (LocalizedModule.mk m t) =
    (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) (m, t).1

Tactic:
rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]

Premises used: LocalizedModule.mk_cancel, LocalizedModule.smul'_mk, Submonoid.smul_def, LocalizedModule.mkLinearMap_apply