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
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)
⊢ ∃ a ∈ S, a • s • y = a • t • x

Tactic:
exact ⟨c, hc, h_inj (by simpa)⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
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_surj : Function.Surjective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : N'
obtain :
  ∀ (x : N) (s : ↥S),
    ∃ (a : M'),
      (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a =
        Function.uncurry (mk' g) (x, s)
⊢ ∃ (a : M'), (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a = x

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g 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_surj : Function.Surjective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
x : N
s : ↥S
obtain :
  ∀ (x : M),
    ∃ (a : M'),
      (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a =
        Function.uncurry (β := ↥S) (mk' g) ((h : (a : M) → N) x, s)
⊢ ∃ (a : M'),
    (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a = Function.uncurry (mk' g) (x, s)

Tactic:
obtain ⟨x, rfl⟩ := h_surj x

Premises used: 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_surj : Function.Surjective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
s : ↥S
x : M
⊢ (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') (mk' f x s) =
    Function.uncurry (β := ↥S) (mk' g) ((h : (a : M) → N) x, s)

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_surj : Function.Surjective.{u_2 + 1, u_6 + 1} (α := M) (β := N) (⇑h : (a : M) → N)
s : ↥S
x : M
⊢ ∃ (a : M'),
    (((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h : M' →ₗ[R] N') : (a : M') → N') a =
      Function.uncurry (β := ↥S) (mk' g) ((h : (a : M) → N) x, s)

Tactic:
exact ⟨mk' f x s, by simp⟩
-- 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
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
obtain :
  ∀ (e : LocalizedModule S M →ₗ[R] LocalizedModule S M),
    e ∘ₗ f = f →
      ∀
        (univ :
          ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M),
            (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f) y → y = e),
        Eq (α := LocalizedModule S M ≃ₗ[R] LocalizedModule S M) (iso S (mkLinearMap S M))
          (LinearEquiv.refl R (LocalizedModule S M))
⊢ Eq (α := LocalizedModule S M ≃ₗ[R] LocalizedModule S M) (iso S (mkLinearMap S M))
    (LinearEquiv.refl R (LocalizedModule S M))

Tactic:
obtain ⟨e, _, univ⟩ := is_universal S f f (map_units f)

Premises used: IsLocalizedModule.is_universal, IsLocalizedModule.map_units
-- 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
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left : e ∘ₗ f = f
univ :
  ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M),
    (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f) y → y = e
rw : e = (↑(LinearEquiv.refl R (LocalizedModule S M)) : LocalizedModule S M →ₗ[R] LocalizedModule S M)
⊢ Eq (α := LocalizedModule S M ≃ₗ[R] LocalizedModule S M) (iso S (mkLinearMap S M))
    (LinearEquiv.refl R (LocalizedModule S M))

Tactic:
rw [← toLinearMap_inj, univ (iso S f) ((eq_toLinearMap_symm_comp f f).1 (iso_symm_comp S f).symm)]

Premises used: IsLocalizedModule.iso, LinearEquiv.toLinearMap_inj, IsLocalizedModule.iso_symm_comp, LinearEquiv.eq_toLinearMap_symm_comp, LinearEquiv.toLinearMap, Iff.mp, Eq.symm
-- 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
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left : e ∘ₗ f = f
univ :
  ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M),
    (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f) y → y = e
⊢ (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f)
    (↑(LinearEquiv.refl R (LocalizedModule S M)) : LocalizedModule S M →ₗ[R] LocalizedModule 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
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
e : LocalizedModule S M →ₗ[R] LocalizedModule S M
left : e ∘ₗ f = f
univ :
  ∀ (y : LocalizedModule S M →ₗ[R] LocalizedModule S M),
    (fun (l : LocalizedModule S M →ₗ[R] LocalizedModule S M) ↦ l ∘ₗ f = f) y → y = e
⊢ e = (↑(LinearEquiv.refl R (LocalizedModule S M)) : LocalizedModule S M →ₗ[R] LocalizedModule S M)

Tactic:
exact Eq.symm <| univ (refl R (LocalizedModule S M)) (by simp)

Premises used: LocalizedModule, LinearEquiv.toLinearMap, LinearEquiv.refl, Eq.symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_7
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ Eq (α := LocalizedModule S M₁)
    (((↑(IsUnit.unit ⋯)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
      LocalizedModule S M₁)
    ((iso S (mkLinearMap S M₁) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₁)

Tactic:
have := (iso_apply_mk S (mkLinearMap S M₁) (g m) s).symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_7
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this :
  Eq (α := LocalizedModule S M₁)
    (((↑(IsUnit.unit ⋯)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
      LocalizedModule S M₁)
    ((iso S (mkLinearMap S M₁) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s) :
      LocalizedModule S M₁)
⊢ Eq (α := LocalizedModule S M₁)
    (((↑(IsUnit.unit ⋯)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
      LocalizedModule S M₁)
    (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s : LocalizedModule S M₁)

Tactic:
rw [iso_localizedModule_eq_refl, refl_apply] at this

Premises used: LinearEquiv.refl_apply, IsLocalizedModule.iso_localizedModule_eq_refl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_7
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this :
  Eq (α := LocalizedModule S M₁)
    (((↑(IsUnit.unit ⋯)⁻¹ : End R (LocalizedModule S M₁)) : (a : LocalizedModule S M₁) → LocalizedModule S M₁)
        ((mkLinearMap S M₁ : (a : M₁) → LocalizedModule S M₁) ((g : (a : M₀) → M₁) m)) :
      LocalizedModule S M₁)
    (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s : LocalizedModule S M₁)
⊢ Eq (α := LocalizedModule S M₁)
    ((((map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
            LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁) :
          (a : LocalizedModule S M₀) → LocalizedModule S M₁)
        (LocalizedModule.mk m s) :
      LocalizedModule S M₁)
    (LocalizedModule.mk ((g : (a : M₀) → M₁) m) s : LocalizedModule S M₁)

Tactic:
simpa [map, lift, iso_localizedModule_eq_refl S M₀]

Premises used: IsLocalizedModule.lift, IsLocalizedModule.map, IsLocalizedModule.iso_localizedModule_eq_refl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
h :
  ∀ (x : LocalizedModule S M₀),
    Eq.{u_8 + 1} (α := M₁')
      (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
            (a : LocalizedModule S M₀) → M₁')
          x :
        M₁')
      (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
              (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
            (a : LocalizedModule S M₀) → M₁')
          x :
        M₁')
⊢ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') =
    (↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
      (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
          (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule 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_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
h :
  ∀ (m : M₀) (s : ↥S),
    Eq.{u_8 + 1} (α := M₁')
      (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
            (a : LocalizedModule S M₀) → M₁')
          (LocalizedModule.mk m s) :
        M₁')
      (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
              (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                  (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                g :
            (a : LocalizedModule S M₀) → M₁')
          (LocalizedModule.mk m s) :
        M₁')
⊢ Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        x :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        x :
      M₁')

Tactic:
induction x using induction_on with | _ m s
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')

Tactic:
((Module.End.isUnit_iff _).1 (map_units f₁ s)).1 ?_

Premises used: Module.End.isUnit_iff, And.left, Iff.mp, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
h :
  Eq.{u_8 + 1} (α := M₁')
    ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
        (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
              (a : LocalizedModule S M₀) → M₁')
            (LocalizedModule.mk m s) :
          M₁') :
      M₁')
    ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
        (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
                (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                    (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                  g :
              (a : LocalizedModule S M₀) → M₁')
            (LocalizedModule.mk m s) :
          M₁') :
      M₁')
⊢ Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m s) :
      M₁')

Tactic:
refine ((Module.End.isUnit_iff _).1 (map_units f₁ s)).1 ?_

Premises used: Module.End.isUnit_iff, And.left, Iff.mp, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
h :
  Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m 1) :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m 1) :
      M₁')
⊢ Eq.{u_8 + 1} (α := M₁')
    ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
        (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
              (a : LocalizedModule S M₀) → M₁')
            (LocalizedModule.mk m s) :
          M₁') :
      M₁')
    ((((algebraMap R (End R M₁') : (a : R) → End R M₁') (↑s : R) : End R M₁') : (a : M₁') → M₁')
        (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
                (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                    (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
                  g :
              (a : LocalizedModule S M₀) → M₁')
            (LocalizedModule.mk m s) :
          M₁') :
      M₁')

Tactic:
rw [Module.algebraMap_end_apply, Module.algebraMap_end_apply,
    ← CompatibleSMul.map_smul, ← CompatibleSMul.map_smul, smul'_mk, ← mk_smul _ s.2, mk_cancel]

Premises used: LocalizedModule.mk_cancel, Submonoid.mk_smul, LocalizedModule.smul'_mk, Module.algebraMap_end_apply, LinearMap.CompatibleSMul.map_smul, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_8
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ Eq.{u_8 + 1} (α := M₁')
    (((map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g ∘ₗ (↑(iso S f₀) : LocalizedModule S M₀ →ₗ[R] M₀') :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m 1) :
      M₁')
    (((↑(iso S f₁) : LocalizedModule S M₁ →ₗ[R] M₁') ∘ₗ
            (map S (mkLinearMap S M₀) (mkLinearMap S M₁) :
                (a : M₀ →ₗ[R] M₁) → LocalizedModule S M₀ →ₗ[R] LocalizedModule S M₁)
              g :
          (a : LocalizedModule S M₀) → M₁')
        (LocalizedModule.mk m 1) :
      M₁')

Tactic:
simp [map, lift, iso_localizedModule_eq_refl, lift_mk]

Premises used: IsLocalizedModule.lift, LocalizedModule.lift_mk, IsLocalizedModule.map, IsLocalizedModule.iso_localizedModule_eq_refl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_11
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : AddCommMonoid M₂'
inst_13 : Module R M₂
inst_14 : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst_15 : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
h₁ :
  ∀ (x : M₀'),
    Eq.{u_10 + 1} (α := M₂')
      ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂') x : M₂')
      (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
            (a : M₀') → M₂')
          x :
        M₂')
⊢ Eq (α := M₀' →ₗ[R] M₂') ((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂')
    ((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
      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_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_11
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : AddCommMonoid M₂'
inst_13 : Module R M₂
inst_14 : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst_15 : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀'
h₁ :
  ∀ (x : M₀) (s : ↥S),
    Eq.{u_10 + 1} (α := M₂')
      ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂')
          (Function.uncurry (mk' f₀) (x, s)) :
        M₂')
      (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
            (a : M₀') → M₂')
          (Function.uncurry (mk' f₀) (x, s)) :
        M₂')
⊢ Eq.{u_10 + 1} (α := M₂')
    ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂') x : M₂')
    (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
          (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_6
M₀' : Type u_9
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₁ : Type u_7
M₁' : Type u_11
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₁'
inst_8 : Module R M₁
inst_9 : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst_10 : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : AddCommMonoid M₂'
inst_13 : Module R M₂
inst_14 : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst_15 : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀
s : ↥S
⊢ Eq.{u_10 + 1} (α := M₂')
    ((((map S f₀ f₂ : (a : M₀ →ₗ[R] M₂) → M₀' →ₗ[R] M₂') (h ∘ₗ g) : M₀' →ₗ[R] M₂') : (a : M₀') → M₂')
        (Function.uncurry (mk' f₀) (x, s)) :
      M₂')
    (((map S f₁ f₂ : (a : M₁ →ₗ[R] M₂) → M₁' →ₗ[R] M₂') h ∘ₗ (map S f₀ f₁ : (a : M₀ →ₗ[R] M₁) → M₀' →ₗ[R] M₁') g :
          (a : M₀') → M₂')
        (Function.uncurry (mk' f₀) (x, s)) :
      M₂')

Tactic:
simp