awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : Eq.{u_4 + 1} (α := N) ((fun (x : N) ↦ c • x) x) ((fun (x : N) ↦ c • x) y)
hS₀ : 0 ∈ S
⊢ Subsingleton N

Tactic:
have : Subsingleton N := (IsLocalizedModule.subsingleton_iff S f).2 fun _ ↦ ⟨0, hS₀, by simp⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : Eq.{u_4 + 1} (α := N) ((fun (x : N) ↦ c • x) x) ((fun (x : N) ↦ c • x) y)
hS₀ : 0 ∈ S
this : Subsingleton N
⊢ x = y

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : Eq.{u_4 + 1} (α := N) ((fun (x : N) ↦ c • x) x) ((fun (x : N) ↦ c • x) y)
hS₀ : 0 ∈ S
this : Subsingleton N
⊢ x = y

Tactic:
exact Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : Eq.{u_4 + 1} (α := N) ((fun (x : N) ↦ c • x) x) ((fun (x : N) ↦ c • x) y)
hS₀ : 0 ∉ S
neg :
  ∀ (a : R) (s : ↥S)
    (hc :
      IsRegular.{u_3} (R := A)
        ((fun (x : R × ↥S) ↦
            (match (motive := R × ↥S → A) x with
              | (r, m) => IsLocalization.mk' A r m :
              A))
          (a, s)))
    (hxy :
      Eq.{u_4 + 1} (α := N)
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          x)
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          y)),
    x = y
⊢ x = y

Tactic:
obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective S c

Premises used: IsLocalization.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
x y : N
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular.{u_3} (R := A)
    ((fun (x : R × ↥S) ↦
        (match (motive := R × ↥S → A) x with
          | (r, m) => IsLocalization.mk' A r m :
          A))
      (a, s))
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      x)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      y)
neg :
  ∀ (m₁ : M) (t₁ : ↥S)
    (hxy :
      Eq.{u_4 + 1} (α := N)
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          (Function.uncurry (mk' f) (m₁, t₁)))
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          y)),
    Function.uncurry (mk' f) (m₁, t₁) = y
⊢ x = y

Tactic:
obtain ⟨⟨m₁, t₁⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
y : N
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular.{u_3} (R := A)
    ((fun (x : R × ↥S) ↦
        (match (motive := R × ↥S → A) x with
          | (r, m) => IsLocalization.mk' A r m :
          A))
      (a, s))
m₁ : M
t₁ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      y)
neg :
  ∀ (m₂ : M) (t₂ : ↥S)
    (hxy :
      Eq.{u_4 + 1} (α := N)
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          (Function.uncurry (mk' f) (m₁, t₁)))
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          (Function.uncurry (mk' f) (m₂, t₂)))),
    Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
⊢ Function.uncurry (mk' f) (m₁, t₁) = y

Tactic:
obtain ⟨⟨m₂, t₂⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y

Premises used: IsLocalizedModule.mk'_surjective, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular.{u_3} (R := A)
    ((fun (x : R × ↥S) ↦
        (match (motive := R × ↥S → A) x with
          | (r, m) => IsLocalization.mk' A r m :
          A))
      (a, s))
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
⊢ ∀ s ∈ S, IsRegular s

Tactic:
replace hS : ∀ s ∈ S, IsRegular s := fun s hs ↦ hS s hs <| ne_of_mem_of_not_mem hs hS₀
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular.{u_3} (R := A)
    ((fun (x : R × ↥S) ↦
        (match (motive := R × ↥S → A) x with
          | (r, m) => IsLocalization.mk' A r m :
          A))
      (a, s))
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
hS : ∀ s ∈ S, IsRegular s
neg :
  ∀ (hc : IsRegular a) (m₁ : M) (t₁ : ↥S) (m₂ : M) (t₂ : ↥S)
    (hxy :
      Eq.{u_4 + 1} (α := N)
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          (Function.uncurry (mk' f) (m₁, t₁)))
        ((fun (x : N) ↦
            HSMul.hSMul.{u_3, u_4, u_4} (α := A)
              ((fun (x : R × ↥S) ↦
                  (match (motive := R × ↥S → A) x with
                    | (r, m) => IsLocalization.mk' A r m :
                    A))
                (a, s))
              x)
          (Function.uncurry (mk' f) (m₂, t₂))))
    (hS : ∀ s ∈ S, IsRegular s), Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)

Tactic:
rw [IsLocalization.isRegular_mk' hS] at hc

Premises used: IsLocalization.isRegular_mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
hS : ∀ s ∈ S, IsRegular s
⊢ ∀ (s : ↥S) (x y : M), s • x = s • y ↔ x = y

Tactic:
have (s : S) (x y : M) : s • x = s • y ↔ x = y := (hS _ s.2).isSMulRegular.eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₁, t₁)))
    ((fun (x : N) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := A)
          ((fun (x : R × ↥S) ↦
              (match (motive := R × ↥S → A) x with
                | (r, m) => IsLocalization.mk' A r m :
                A))
            (a, s))
          x)
      (Function.uncurry (mk' f) (m₂, t₂)))
hS : ∀ s ∈ S, IsRegular s
this : ∀ (s : ↥S) (x y : M), s • x = s • y ↔ x = y
neg : ∀ (hxy : t₁ • a • m₂ = t₂ • a • m₁), t₁ • m₂ = t₂ • m₁
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)

Tactic:
simp only [Function.uncurry_apply_pair, mk'_smul_mk', mk'_eq_mk'_iff, mul_smul, this,
      exists_const] at hxy ⊢

Premises used: IsLocalizedModule.mk'_eq_mk'_iff, IsLocalizedModule.mk'_smul_mk', exists_const, Function.uncurry_apply_pair, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
inst_9 : IsTorsionFree R M
inst_10 : IsLocalization S A
inst_11 : IsLocalizedModule S f
hS₀ : 0 ∉ S
a : R
s : ↥S
hc : IsRegular a
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hS : ∀ s ∈ S, IsRegular s
this : ∀ (s : ↥S) (x y : M), s • x = s • y ↔ x = y
hxy : t₁ • a • m₂ = t₂ • a • m₁
⊢ t₁ • m₂ = t₂ • m₁

Tactic:
simpa [smul_comm _ a, hc.isSMulRegular.eq_iff] using hxy

Premises used: Function.Injective.eq_iff, IsRegular.isSMulRegular, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
S : Submonoid R
inst_11 : IsLocalization S A
inst_12 : IsLocalizedModule S f
⊢ ∀ s ∈ S, s ≠ 0 → IsRegular s

Tactic:
simp [isRegular_iff_ne_zero]

Premises used: isRegular_iff_ne_zero
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : AddCommMonoid N
inst_5 : Module A N
inst_6 : Algebra R A
inst_7 : Module R N
inst_8 : IsScalarTower R A N
f : M →ₗ[R] N
inst_9 : IsDomain R
S : Submonoid R
inst_10 : IsTorsionFree R M
⊢ IsTorsionFree (Localization (M := R) S) (LocalizedModule S M)

Tactic:
isTorsionFree (LocalizedModule.mkLinearMap S M) S

Premises used: IsLocalizedModule.isTorsionFree, LocalizedModule.mkLinearMap
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy :
  Eq (α := LocalizedModule S M₂)
    ((((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂) :
                (a : M₁ →ₗ[R] M₂) → LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂)
              h :
            LocalizedModule S M₁ →ₗ[R] LocalizedModule S M₂) :
          (a : LocalizedModule S M₁) → LocalizedModule S M₂)
        (mk m s) :
      LocalizedModule S M₂)
    (0 : LocalizedModule S M₂)
⊢ ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0

Tactic:
rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy

Premises used: LocalizedModule.mk_eq, smul_zero, one_smul, OfNat.ofNat, LocalizedModule.zero_mk, IsLocalizedModule.map_LocalizedModules
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
obtain :
  ∀ (a : R) (aS : a ∈ S)
    (ha :
      HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) ((h : (a : M₁) → M₂) m : M₂) =
        HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) 0),
    Membership.mem (γ := Set (LocalizedModule S M₁))
      (Set.range (ι := LocalizedModule S M₀)
        (⇑((IsLocalizedModule.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₁))
      (mk m s)
⊢ Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.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₁))
    (mk m s)

Tactic:
obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy

Premises used: Subtype.exists, Iff.mp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
a : R
aS : a ∈ S
ha :
  HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) ((h : (a : M₁) → M₂) m : M₂) =
    HSMul.hSMul (β := M₂) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) a aS) 0
⊢ Membership.mem (γ := Set M₁) (Set.range.{u_3, u_2 + 1} (ι := M₀) (⇑g : (a : M₀) → M₁)) (a • m)

Tactic:
rw [smul_zero, mk_smul, ← map_smul, ex (a • m)] at ha

Premises used: smul_zero, Submonoid.mk_smul, HSMul.hSMul, map_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
a : R
aS : a ∈ S
ha : Membership.mem (γ := Set M₁) (Set.range.{u_3, u_2 + 1} (ι := M₀) (⇑g : (a : M₀) → M₁)) (a • m)
rcases :
  ∀ (x : M₀) (hx : (g : (a : M₀) → M₁) x = a • m),
    Membership.mem (γ := Set (LocalizedModule S M₁))
      (Set.range (ι := LocalizedModule S M₀)
        (⇑((IsLocalizedModule.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₁))
      (mk m s)
⊢ Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.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₁))
    (mk m s)

Tactic:
rcases ha with ⟨x, hx⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Exact
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst_1 : AddCommMonoid M₀
inst_2 : Module R M₀
M₁ : Type u_3
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
M₂ : Type u_4
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact.{u_2, u_3, u_4} (M := M₀) (N := M₁) (P := M₂) (⇑g : (a : M₀) → M₁) (⇑h : (a : M₁) → M₂)
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ (u : ↥S), HSMul.hSMul (β := M₂) u ((h : (a : M₁) → M₂) m : M₂) = HSMul.hSMul (β := M₂) u 0
a : R
aS : a ∈ S
x : M₀
hx : (g : (a : M₀) → M₁) x = a • m
h₁ :
  Eq (α := LocalizedModule S M₁)
    ((((IsLocalizedModule.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₁)
        (mk x (Subtype.mk (p := fun (x : R) ↦ x ∈ S) a aS * s)) :
      LocalizedModule S M₁)
    (mk m s : LocalizedModule S M₁)
⊢ Membership.mem (γ := Set (LocalizedModule S M₁))
    (Set.range (ι := LocalizedModule S M₀)
      (⇑((IsLocalizedModule.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₁))
    (mk m s)

Tactic:
use mk x (⟨a, aS⟩ * s)

Premises used: HMul.hMul, LocalizedModule.mk