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''
x₁ x₂ : M
eq1 :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x₁ : LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) x₂ : LocalizedModule S M)
⊢ ∃ (c : ↥S), c • x₁ = c • x₂

Tactic:
simpa only [eq_comm, one_smul] using LocalizedModule.mk_eq.mp eq1

Premises used: LocalizedModule.mk_eq, eq_comm, one_smul, Iff.mp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x : ↥(Algebra.algebraMapSubmonoid A S)
obtain :
  ∀ (x : R) (hx : x ∈ (↑S : Set R)),
    IsUnit.{u_6} (M := End A N)
      ((algebraMap A (End A N) : (a : A) → End A N)
          (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
                ((algebraMap R A : (a : R) → A) x) ⋯) :
            A) :
        End A N)
⊢ IsUnit.{u_6} (M := End A N) ((algebraMap A (End A N) : (a : A) → End A N) (↑x : A) : End A N)

Tactic:
obtain ⟨_, x, hx, rfl⟩ := x

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x : R
hx : x ∈ (↑S : Set R)
⊢ IsUnit.{u_6} (M := End R N)
    ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) x hx) : R) : End R N)

Tactic:
have := IsLocalizedModule.map_units (f.restrictScalars R) ⟨x, hx⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x : R
hx : x ∈ (↑S : Set R)
this :
  IsUnit.{u_6} (M := End R N)
    ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) x hx) : R) : End R N)
simp :
  ∀
    (this :
      Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
        (⇑((algebraMap R (End R N) : (a : R) → End R N) x : End R N) : (a : N) → N)),
    Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
      (⇑((algebraMap R (End A N) : (a : R) → End A N) x : End A N) : (a : N) → N)
⊢ IsUnit.{u_6} (M := End A N)
    ((algebraMap A (End A N) : (a : A) → End A N)
        (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
              ((algebraMap R A : (a : R) → A) x) ⋯) :
          A) :
      End A N)

Tactic:
simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢

Premises used: Module.End.isUnit_iff, IsScalarTower.algebraMap_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x : R
hx : x ∈ (↑S : Set R)
this :
  Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
    (⇑((algebraMap R (End R N) : (a : R) → End R N) x : End R N) : (a : N) → N)
⊢ Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
    (⇑((algebraMap R (End A N) : (a : R) → End A N) x : End A N) : (a : N) → N)

Tactic:
this
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
x : R
hx : x ∈ (↑S : Set R)
this :
  Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
    (⇑((algebraMap R (End R N) : (a : R) → End R N) x : End R N) : (a : N) → N)
⊢ Function.Bijective.{u_6 + 1, u_6 + 1} (α := N) (β := N)
    (⇑((algebraMap R (End A N) : (a : R) → End A N) x : End A N) : (a : N) → N)

Tactic:
exact this
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
y : N
obtain :
  ∀ (x : M) (t : ↥S)
    (e :
      (x, t).2 • y =
        ((↑R :
                {S : Type u_5} →
                  {M : Type u_2} →
                    {M₂ : Type u_6} →
                      [inst : Semiring R] →
                        [inst_12 : Semiring S] →
                          [inst_13 : AddCommMonoid M] →
                            [inst_14 : AddCommMonoid M₂] →
                              [inst_15 : Module R M] →
                                [inst_16 : Module R M₂] →
                                  [inst_17 : Module S M] →
                                    [inst_18 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              f :
            (a : M) → N)
          (x, t).1),
    ∃ (x : Prod.{u_2, u_5} M ↥(Algebra.algebraMapSubmonoid A S)), x.2 • y = (f : (a : M) → N) x.1
⊢ ∃ (x : Prod.{u_2, u_5} M ↥(Algebra.algebraMapSubmonoid A S)), x.2 • y = (f : (a : M) → N) x.1

Tactic:
obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S (f.restrictScalars R) y

Premises used: LinearMap.restrictScalars, IsLocalizedModule.surj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
y : N
x : M
t : ↥S
e :
  (x, t).2 • y =
    ((↑R :
            {S : Type u_5} →
              {M : Type u_2} →
                {M₂ : Type u_6} →
                  [inst : Semiring R] →
                    [inst_12 : Semiring S] →
                      [inst_13 : AddCommMonoid M] →
                        [inst_14 : AddCommMonoid M₂] →
                          [inst_15 : Module R M] →
                            [inst_16 : Module R M₂] →
                              [inst_17 : Module S M] →
                                [inst_18 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f :
        (a : M) → N)
      (x, t).1
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := ↥(Algebra.algebraMapSubmonoid A S))
      ((x,
            Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
              ((algebraMap R A : (a : R) → A) (↑t : R)) ⋯).2 :
        ↥(Algebra.algebraMapSubmonoid A S))
      y =
    (f : (a : M) → N)
      ((x,
            Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
              ((algebraMap R A : (a : R) → A) (↑t : R)) ⋯) :
          Prod.{u_2, u_5} M ↥(Algebra.algebraMapSubmonoid A S)).1

Tactic:
simpa [Submonoid.smul_def] using e

Premises used: Submonoid.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f)
y : N
x : M
t : ↥S
e :
  (x, t).2 • y =
    ((↑R :
            {S : Type u_5} →
              {M : Type u_2} →
                {M₂ : Type u_6} →
                  [inst : Semiring R] →
                    [inst_12 : Semiring S] →
                      [inst_13 : AddCommMonoid M] →
                        [inst_14 : AddCommMonoid M₂] →
                          [inst_15 : Module R M] →
                            [inst_16 : Module R M₂] →
                              [inst_17 : Module S M] →
                                [inst_18 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f :
        (a : M) → N)
      (x, t).1
⊢ ∃ (x : Prod.{u_2, u_5} M ↥(Algebra.algebraMapSubmonoid A S)), x.2 • y = (f : (a : M) → N) x.1

Tactic:
exact ⟨⟨x, ⟨_, t, t.2, rfl⟩⟩, by simpa [Submonoid.smul_def] using e⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      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 : ↥(Algebra.algebraMapSubmonoid A S)), c • x₁ = c • x₂
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid A S)), c • x₁ = c • x₂

Tactic:
obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f.restrictScalars R) 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
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      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₂
⊢ HSMul.hSMul.{u_5, u_2, u_2} (α := ↥(Algebra.algebraMapSubmonoid A S))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
          ((algebraMap R A : (a : R) → A) (↑c : R)) ⋯ :
        ↥(Algebra.algebraMapSubmonoid A S))
      x₁ =
    HSMul.hSMul.{u_5, u_2, u_2} (α := ↥(Algebra.algebraMapSubmonoid A S))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Algebra.algebraMapSubmonoid A S) x)
          ((algebraMap R A : (a : R) → A) (↑c : R)) ⋯ :
        ↥(Algebra.algebraMapSubmonoid A S))
      x₂

Tactic:
simpa [Submonoid.smul_def]

Premises used: Submonoid.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
A : Type u_5
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : Module R M
S : Submonoid R
N : Type u_6
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : Module A M
inst_8 : Module A N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
inst_11 :
  IsLocalizedModule S
    ((↑R :
        {S : Type u_5} →
          {M : Type u_2} →
            {M₂ : Type u_6} →
              [inst : Semiring R] →
                [inst_12 : Semiring S] →
                  [inst_13 : AddCommMonoid M] →
                    [inst_14 : AddCommMonoid M₂] →
                      [inst_15 : Module R M] →
                        [inst_16 : Module R M₂] →
                          [inst_17 : Module S M] →
                            [inst_18 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      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 : ↥(Algebra.algebraMapSubmonoid A S)), c • x₁ = c • x₂

Tactic:
refine ⟨⟨_, c, c.2, rfl⟩, by simpa [Submonoid.smul_def]⟩
-- 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 : ↥T
obtain :
  ∀ (m : R) (mx : m * (↑x : R) ∈ S),
    IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)

Tactic:
obtain ⟨m, mx⟩ := h' x
-- 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 : ↥T
m : R
mx : m * (↑x : R) ∈ S
⊢ IsUnit.{u_6} (M := End R N)
    ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (m * (↑x : R)) mx) : R) :
      End R N)

Tactic:
have := IsLocalizedModule.map_units f ⟨_, mx⟩
-- 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 : ↥T
m : R
mx : m * (↑x : R) ∈ S
this :
  IsUnit.{u_6} (M := End R N)
    ((algebraMap R (End R N) : (a : R) → End R N) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (m * (↑x : R)) mx) : R) :
      End R N)
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) m : End R N) ∧
    IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)

Tactic:
rw [map_mul, (Algebra.commute_algebraMap_left _ _).isUnit_mul_iff] at this

Premises used: map_mul, Algebra.commute_algebraMap_left, Commute.isUnit_mul_iff
-- 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 : ↥T
m : R
mx : m * (↑x : R) ∈ S
this :
  IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) m : End R N) ∧
    IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)

Tactic:
this.2

Premises used: And.right
-- 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 : ↥T
m : R
mx : m * (↑x : R) ∈ S
this :
  IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) m : End R N) ∧
    IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)
⊢ IsUnit.{u_6} (M := End R N) ((algebraMap R (End R N) : (a : R) → End R N) (↑x : R) : End R N)

Tactic:
exact this.2

Premises used: And.right
-- 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
y : N
obtain :
  ∀ (x : M) (t : ↥S) (e : (x, t).2 • y = (f : (a : M) → N) (x, t).1),
    ∃ (x : Prod.{u_2, u_1} M ↥T), x.2 • y = (f : (a : M) → N) x.1
⊢ ∃ (x : Prod.{u_2, u_1} M ↥T), x.2 • y = (f : (a : M) → N) x.1

Tactic:
obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S f y

Premises used: IsLocalizedModule.surj
-- 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
y : N
x : M
t : ↥S
e : (x, t).2 • y = (f : (a : M) → N) (x, t).1
⊢ ∃ (x : Prod.{u_2, u_1} M ↥T), x.2 • y = (f : (a : M) → N) x.1

Tactic:
⟨⟨x, ⟨t, h t.2⟩⟩, e⟩

Premises used: Prod.mk, 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
y : N
x : M
t : ↥S
e : (x, t).2 • y = (f : (a : M) → N) (x, t).1
⊢ ∃ (x : Prod.{u_2, u_1} M ↥T), x.2 • y = (f : (a : M) → N) x.1

Tactic:
exact ⟨⟨x, ⟨t, h t.2⟩⟩, e⟩