awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
e : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N)
obtain : ∀ (c : ↥S) (hc : c • x₁ = c • x₂), ∃ (c : ↥T), c • x₁ = c • x₂
⊢ ∃ (c : ↥T), c • x₁ = c • x₂

Tactic:
obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f) e

Premises used: IsLocalizedModule.exists_of_eq
-- 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
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
e : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N)
c : ↥S
hc : c • x₁ = c • x₂
⊢ ∃ (c : ↥T), c • x₁ = c • x₂

Tactic:
⟨⟨c, h c.2⟩, hc⟩

Premises used: Subtype.mk, Exists.intro, 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
N : Type u_6
inst_3 : AddCommMonoid N
inst_4 : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ (m : R), m * (↑x : R) ∈ S
f : M →ₗ[R] N
inst_5 : IsLocalizedModule S f
x₁ x₂ : M
e : Eq.{u_6 + 1} (α := N) ((f : (a : M) → N) x₁ : N) ((f : (a : M) → N) x₂ : N)
c : ↥S
hc : c • x₁ = c • x₂
⊢ ∃ (c : ↥T), c • x₁ = c • x₂

Tactic:
exact ⟨⟨c, h c.2⟩, hc⟩
-- 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
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
dsimp :
  Eq (α := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((fun (x : Prod.{u_2, u_1} M ↥S) ↦ (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') x.1 : M') : M'))
      (a, b))
    ((fun (x : Prod.{u_2, u_1} M ↥S) ↦ (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') x.1 : M') : M'))
      (a', b'))

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_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
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑(a, b).2 : R) • a') : M')
    ((f : (a : M) → M') ((↑(a', b').2 : R) • a) : M')
⊢ Eq (α := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')

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

Premises used: Module.End.algebraMap_isUnit_inv_apply_eq_iff', 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 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑(a, b).2 : R) • a') : M')
    ((f : (a : M) → M') ((↑(a', b').2 : R) • a) : M')

Tactic:
(IsLocalizedModule.eq_iff_exists S f).mpr ⟨c, eq1.symm⟩

Premises used: Iff.mpr, Exists.intro, IsLocalizedModule.eq_iff_exists, Eq.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 : M →ₗ[R] M''
inst_12 : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑(a, b).2 : R) • a') : M')
    ((f : (a : M) → M') ((↑(a', b').2 : R) • a) : M')

Tactic:
exact (IsLocalizedModule.eq_iff_exists S f).mpr ⟨c, eq1.symm⟩

Premises used: Iff.mpr, Exists.intro, IsLocalizedModule.eq_iff_exists, Eq.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
m : M
s : ↥S
⊢ fromLocalizedModule' S f (LocalizedModule.mk m s) =
    ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M')

Tactic:
rfl

Premises used: LocalizedModule.liftOn, rfl, IsLocalizedModule.fromLocalizedModule'
-- 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 y : LocalizedModule S M
a a' : M
b b' : ↥S
simp :
  ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') (b' • a + b • a') : M') =
    HAdd.hAdd (α := M') (β := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')
⊢ fromLocalizedModule' S f (HAdd.hAdd (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')) =
    fromLocalizedModule' S f (LocalizedModule.mk a b) + fromLocalizedModule' S f (LocalizedModule.mk a' b')

Tactic:
simp only [LocalizedModule.mk_add_mk, fromLocalizedModule'_mk]

Premises used: LocalizedModule.mk_add_mk, IsLocalizedModule.fromLocalizedModule'_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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
rw :
  HAdd.hAdd (α := M') (β := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M') =
    HAdd.hAdd (α := M') (β := M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) :
        M')
⊢ ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') (b' • a + b • a') : M') =
    HAdd.hAdd (α := M') (β := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')

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

Premises used: map_add, smul_add, 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
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 y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
e_a₁ :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b • a') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) : M')
⊢ HAdd.hAdd (α := M') (β := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M') =
    HAdd.hAdd (α := M') (β := M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : M')
      (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (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_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 y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a : (f : (a : M) → M') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') (b' • a) : M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') ((↑(b * b') : R) • a) : M') : 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_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 y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b • a') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M')) : 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_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 y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (f : (a : M) → M') ((↑(b * b') : R) • a) = HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') (b' • a) : M')

Tactic:
simp [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_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 y : LocalizedModule S M
a a' : M
b b' : ↥S
e_a :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')
e_a₁ :
  HSMul.hSMul (β := M') ((↑b : R) * (↑b' : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
e_a₂ :
  HSMul.hSMul (β := M') ((↑b' : R) * (↑b : R)) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
e_a₃ :
  (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') b ((f : (a : M) → M') a' : M')
e_a₄ e_a₅ :
  (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    (↑b' : R) • HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M')
⊢ HSMul.hSMul (β := M') (↑(b * b') : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') (b • a') : M')

Tactic:
rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, mul_smul, Submonoid.smul_def]

Premises used: Submonoid.smul_def, mul_comm, LinearMap.map_smul_of_tower, SemigroupAction.mul_smul, 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_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
r : R
x : LocalizedModule S M
a : M
b : ↥S
rw :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    fromLocalizedModule' S f (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk a b))
rw₁ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    fromLocalizedModule' S f (LocalizedModule.mk (r • a) b)
rw₂ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') (r • a) : M')
rw₃ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') (HSMul.hSMul (β := M') r ((f : (a : M) → M') a : M'))
rw₄ rw₅ :
  HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M') =
    HSMul.hSMul (β := M') r (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) =
    fromLocalizedModule' S f (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk a b))

Tactic:
rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk,
        f.map_smul, map_smul]

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

Tactic:
rw [fromLocalizedModule'_smul, RingHom.id_apply]

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

Tactic:
rfl

Premises used: LocalizedModule.liftOn, rfl, IsLocalizedModule.fromLocalizedModule'
-- 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 y : LocalizedModule S M
eq1 :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') x : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') y : M')
h :
  ∀ (a : M) (b : ↥S)
    (eq1 :
      Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a b) : M')
        ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') y : M')),
    LocalizedModule.mk a b = y
⊢ x = y

Tactic:
induction x with | _ a b
-- 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
y : LocalizedModule S M
a : M
b : ↥S
eq1 :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a b) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') y : M')
h :
  ∀ (a' : M) (b' : ↥S)
    (eq1 :
      Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a b) : M')
        ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk a' b') : M')),
    Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = y

Tactic:
induction y with | _ a' b'
-- 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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  Eq (α := M') (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a : M') : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') a' : M') : M')
⊢ HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')

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

Premises used: Module.End.algebraMap_isUnit_inv_apply_eq_iff', 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
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 :
  HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
h : ∃ (u : ↥S), u • b' • a = u • b • a'
h₁ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (b' • a) : M') ((f : (a : M) → M') (b • a') : M')
h₂ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') (b • a') : M')
h₃ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') ((↑b' : R) • a) : M') ((f : (a : M) → M') ((↑b : R) • a') : M')
h₄ : HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') = (f : (a : M) → M') ((↑b : R) • a')
h₅ :
  HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') =
    HSMul.hSMul (β := M') (↑b : R) ((f : (a : M) → M') a' : M')
h₆ h₇ :
  HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M') =
    HSMul.hSMul (β := M') (↑b' : R) ((f : (a : M) → M') a : M')
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk a b) (LocalizedModule.mk a' b')

Tactic:
rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.map_smul, eq1]

Premises used: LocalizedModule.mk_eq, Submonoid.smul_def, LinearMap.map_smul, IsLocalizedModule.eq_iff_exists
-- 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
eq1 : (m, s).2 • x = (f : (a : M) → M') (m, s).1
rw : ((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M') = x
rw₁ : (f : (a : M) → M') m = (↑s : R) • x
rw₂ : (m, s).2 • x = (↑s : R) • x
rw₃ rw₄ : (↑(m, s).2 : R) • x = (↑s : R) • x
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) = x

Tactic:
rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
      Submonoid.smul_def]

Premises used: IsLocalizedModule.fromLocalizedModule_mk, Submonoid.smul_def, 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
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
⊢ Function.Bijective (α := LocalizedModule S M) (β := M') (⇑(fromLocalizedModule S f) : (a : LocalizedModule S M) → M')

Tactic:
⟨fromLocalizedModule.inj _ _, fromLocalizedModule.surj _ _⟩

Premises used: IsLocalizedModule.fromLocalizedModule.inj, And.intro, Function.Bijective, IsLocalizedModule.fromLocalizedModule.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
m : M
s : ↥S
⊢ Eq.{u_3 + 1} (α := M') ((iso S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
    (((↑⋯.unit⁻¹ : End R M') : (a : M') → M') ((f : (a : M) → M') m : M') : M')

Tactic:
rfl

Premises used: LocalizedModule.liftOn, rfl, IsLocalizedModule.fromLocalizedModule'
-- 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
⊢ Eq.{u_3 + 1} (α := M') ((iso S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk x 1) : M')
    ((f : (a : M) → M') x : M')

Tactic:
simp [iso_apply_mk]

Premises used: IsLocalizedModule.iso_apply_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
m : M'
⊢ Function.Injective (α := LocalizedModule S M) (β := M') (⇑(iso S f) : (a : LocalizedModule S M) → M')

Tactic:
LinearEquiv.injective (iso S f)

Premises used: IsLocalizedModule.iso, LinearEquiv.injective