awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') → ∃ (m : ↥M), m • x = 0
x : S
h : ∃ (m : ↥M), m • x = 0
m : R
hm : m ∈ M
e : Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm • x = 0
rw :
  HSMul.hSMul (β := S') m ((f : (a : S) → S') x : S') =
    HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') (0 : S')
⊢ HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') ((f : (a : S) → S') x : S') =
    HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') (0 : S')

Tactic:
rw [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') → ∃ (m : ↥M), m • x = 0
x : S
h : ∃ (m : ↥M), m • x = 0
m : R
hm : m ∈ M
e : Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm • x = 0
⊢ HSMul.hSMul (β := S') m ((f : (a : S) → S') x : S') =
    HMul.hMul (α := S') (β := S') ((algebraMap R S' : (a : R) → S') m : S') (0 : S')

Tactic:
simpa [Submonoid.smul_def] using f.congr_arg e

Premises used: Submonoid.smul_def, AlgHom.congr_arg
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') → ∃ (m : ↥M), m • x = 0
⊢ ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0

Tactic:
replace h₃ := fun x =>
    Iff.intro (h₃ x) fun ⟨⟨m, hm⟩, e⟩ =>
      (h₁ m hm).mul_left_cancel <| by
        rw [← Algebra.smul_def]
        simpa [Submonoid.smul_def] using f.congr_arg e
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
map_units :
  ∀ (x : ↥M), IsUnit.{u_8} (M := End R S') ((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S')
surj : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f.toLinearMap : (a : S) → S') x.1
exists_of_eq :
  ∀ {x₁ x₂ : S},
    Eq.{u_8 + 1} (α := S') ((f.toLinearMap : (a : S) → S') x₁ : S') ((f.toLinearMap : (a : S) → S') x₂ : S') →
      ∃ (c : ↥M), c • x₁ = c • x₂
⊢ IsLocalizedModule M f.toLinearMap

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
map_units :
  Function.Bijective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
⊢ IsUnit.{u_8} (M := End R S') ((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S')

Tactic:
rw [Module.End.isUnit_iff]

Premises used: Module.End.isUnit_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
map_units :
  Function.Injective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
map_units₁ :
  Function.Surjective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')
⊢ Function.Bijective.{u_8 + 1, u_8 + 1} (α := S') (β := S')
    (⇑((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S')

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a b : S'
e : x • a = x • b
⊢ HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') a =
    HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') b

Tactic:
simp_rw [Submonoid.smul_def, Algebra.smul_def] at e

Premises used: Submonoid.smul_def, Algebra.smul_def
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a b : S'
e :
  HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') a =
    HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') b
⊢ a = b

Tactic:
(h₁ x x.2).mul_left_cancel e

Premises used: IsUnit.mul_left_cancel, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a b : S'
e :
  HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') a =
    HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') b
⊢ a = b

Tactic:
exact (h₁ x x.2).mul_left_cancel e

Premises used: IsUnit.mul_left_cancel, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a : S'
⊢ ∃ (a_1 : S'), (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') a_1 = a

Tactic:
⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩

Premises used: Units.val, HMul.hMul, Inv.inv, Exists.intro, IsUnit.unit, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a : S'
map_units :
  (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a
⊢ ∃ (a_1 : S'), (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') a_1 = a

Tactic:
refine ⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x : ↥M
a : S'
map_units : (↑x : R) • ((↑⋯.unit⁻¹ : S') * a) = a
map_units₁ : HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') ((↑⋯.unit⁻¹ : S') * a) = a
map_units₂ : HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') (↑⋯.unit⁻¹ : S') * a = a
map_units₃ : 1 * a = a
map_units₄ map_units₅ : a = a
⊢ (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a

Tactic:
rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]

Premises used: IsUnit.mul_val_inv, mul_assoc, Module.algebraMap_end_apply, Algebra.smul_def, one_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
⊢ ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f.toLinearMap : (a : S) → S') x.1

Tactic:
h₂
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
⊢ ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f.toLinearMap : (a : S) → S') x.1

Tactic:
exact h₂
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x y : S
exists_of_eq :
  Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') ((f : (a : S) → S') y : S') → ∃ (c : ↥M), c • x = c • y
⊢ Eq.{u_8 + 1} (α := S') ((f.toLinearMap : (a : S) → S') x : S') ((f.toLinearMap : (a : S) → S') y : S') →
    ∃ (c : ↥M), c • x = c • y

Tactic:
dsimp only [AlgHom.toLinearMap_apply]

Premises used: AlgHom.toLinearMap_apply
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x y : S
exists_of_eq : (∃ (m : ↥M), m • (x - y) = 0) → ∃ (c : ↥M), c • x = c • y
⊢ Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') ((f : (a : S) → S') y : S') → ∃ (c : ↥M), c • x = c • y

Tactic:
rw [← sub_eq_zero, ← map_sub, h₃]

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x y : S
exists_of_eq : (∃ (m : ↥M), m • x = m • y) → ∃ (c : ↥M), c • x = c • y
⊢ (∃ (m : ↥M), m • (x - y) = 0) → ∃ (c : ↥M), c • x = c • y

Tactic:
simp_rw [smul_sub, sub_eq_zero]

Premises used: sub_eq_zero, smul_sub
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x y : S
⊢ (∃ (m : ↥M), m • x = m • y) → ∃ (c : ↥M), c • x = c • y

Tactic:
id

Premises used: id
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
S : Type u_7
S' : Type u_8
inst : CommSemiring R
inst_1 : Ring S
inst_2 : Ring S'
inst_3 : Algebra R S
inst_4 : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit.{u_8} (M := S') ((algebraMap R S' : (a : R) → S') x : S')
h₂ : ∀ (y : S'), ∃ (x : Prod.{u_7, u_6} S ↥M), x.2 • y = (f : (a : S) → S') x.1
h₃ : ∀ (x : S), Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') (0 : S') ↔ ∃ (m : ↥M), m • x = 0
x y : S
⊢ (∃ (m : ↥M), m • x = m • y) → ∃ (c : ↥M), c • x = c • y

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : IsLocalization S A
f : M →ₗ[R] M'
inst_8 : IsLocalizedModule S f
⊢ IsScalarTower R A M'

Tactic:
(IsLocalizedModule.iso S f).symm.isScalarTower A

Premises used: LinearEquiv.symm, IsLocalizedModule.iso, LinearEquiv.isScalarTower
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
m : M
⊢ m ∈ g.ker ↔ ∃ r ∈ S, r • m = 0

Tactic:
simpa using IsLocalizedModule.eq_zero_iff S g

Premises used: IsLocalizedModule.eq_zero_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
rw : Subsingleton M' ↔ ⊤ ≤ g.ker
⊢ Subsingleton M' ↔ g.ker = ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
⊢ Subsingleton M' ↔ ⊤ ≤ g.ker

Tactic:
⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩

Premises used: Iff.mpr, subsingleton_iff_forall_eq, Iff.intro, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
refine : ∀ (H : ⊤ ≤ g.ker) (x : M'), x = 0
⊢ Subsingleton M' ↔ ⊤ ≤ g.ker

Tactic:
refine ⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
H : ⊤ ≤ g.ker
x : M'
obtain : ∀ (x : M) (s : ↥S), Function.uncurry (mk' g) (x, s) = 0
⊢ x = 0

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_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
H : ⊤ ≤ g.ker
x : M
s : ↥S
⊢ Function.uncurry (mk' g) (x, s) = 0

Tactic:
simpa using @H x Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
simp_rw : g.ker = ⊤ ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
simp_rw₁ : ⊤ ≤ g.ker ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
simp_rw₂ : (∀ ⦃x : M⦄, Membership.mem (γ := Submodule R M) ⊤ x → x ∈ g.ker) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
simp_rw₃ : (∀ ⦃x : M⦄, Membership.mem (γ := Submodule R M) ⊤ x → ∃ r ∈ S, r • x = 0) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
simp_rw₄ : (∀ ⦃x : M⦄, True → ∃ r ∈ S, r • x = 0) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
simp_rw [subsingleton_iff_ker_eq_top S g, ← top_le_iff, SetLike.le_def,
    mem_ker_iff S, Submodule.mem_top, true_implies]

Premises used: SetLike.le_def, IsLocalizedModule.subsingleton_iff_ker_eq_top, IsLocalizedModule.mem_ker_iff, true_implies, top_le_iff, Submodule.mem_top
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
inst_6 : Subsingleton M
rw : ∀ (m : M), ∃ r ∈ S, r • m = 0
⊢ Subsingleton M'

Tactic:
rw [subsingleton_iff S g]

Premises used: IsLocalizedModule.subsingleton_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
inst_6 : Subsingleton M
m : M
h : 1 ∈ S ∧ HSMul.hSMul.{u_6, u_8, u_8} (α := R) 1 m = 0
⊢ ∃ r ∈ S, r • m = 0

Tactic:
use 1
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_6
M : Type u_8
M' : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst_5 : IsLocalizedModule S g
inst_6 : Subsingleton M
m : M
⊢ 1 ∈ S ∧ HSMul.hSMul.{u_6, u_8, u_8} (α := R) 1 m = 0

Tactic:
simp [one_mem, Subsingleton.elim m 0]

Premises used: OneMemClass.one_mem, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submonoid R
m : M
⊢ Membership.mem (γ := Submodule R M) (LinearMap.ker (mkLinearMap S M)) m ↔ ∃ r ∈ S, r • m = 0

Tactic:
IsLocalizedModule.mem_ker_iff S

Premises used: IsLocalizedModule.mem_ker_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submonoid R
⊢ Subsingleton (LocalizedModule S M) ↔ Eq (α := Submodule R M) (LinearMap.ker (mkLinearMap S M)) ⊤

Tactic:
IsLocalizedModule.subsingleton_iff_ker_eq_top S _

Premises used: IsLocalizedModule.subsingleton_iff_ker_eq_top
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submonoid R
⊢ Subsingleton (LocalizedModule S M) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

Tactic:
IsLocalizedModule.subsingleton_iff S (LocalizedModule.mkLinearMap S M)

Premises used: IsLocalizedModule.subsingleton_iff, LocalizedModule.mkLinearMap
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
S : Submonoid R
rw : ∀ (m : M), ∃ r ∈ S, r • m = 0
⊢ Subsingleton (LocalizedModule S M)

Tactic:
rw [IsLocalizedModule.subsingleton_iff S (LocalizedModule.mkLinearMap S M)]

Premises used: IsLocalizedModule.subsingleton_iff, LocalizedModule.mkLinearMap
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
S : Submonoid R
m : M
w : R
left : 1 ∈ S
right : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = 0
⊢ ∃ r ∈ S, r • m = 0

Tactic:
use 1, S.one_mem, Subsingleton.elim _ _

Premises used: Submonoid.one_mem, 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)
pos : ∀ (hS₀ : 0 ∈ S), x = y
neg : ∀ (hS₀ : 0 ∉ S), x = y
⊢ x = y

Tactic:
by_cases hS₀ : 0 ∈ S
-- 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
x_1 : M
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 x_1 = 0

Tactic:
simp