awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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'
⊢ (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a
have map_units : (↑x : R) • ((↑sorry.unit⁻¹ : S') * a) = a
Tactic: rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a
have map_units₁ : HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') ((↑sorry.unit⁻¹ : S') * a) = a
Tactic: rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a
have map_units₂ : HMul.hMul (α := S') ((algebraMap R S' : (a : R) → S') (↑x : R) : S') (↑sorry.unit⁻¹ : S') * a = a
Tactic: rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a
have map_units₃ : 1 * a = a
Tactic: rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ (((algebraMap R (End R S') : (a : R) → End R S') (↑x : R) : End R S') : (a : S') → S') ((↑⋯.unit⁻¹ : S') * a) = a
have map_units₄ : a = a
Tactic: rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ 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
have 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
Tactic: dsimp only [AlgHom.toLinearMap_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Eq.{u_8 + 1} (α := S') ((f : (a : S) → S') x : S') ((f : (a : S) → S') y : S') → ∃ (c : ↥M), c • x = c • y
have exists_of_eq : (∃ (m : ↥M), m • (x - y) = 0) → ∃ (c : ↥M), c • x = c • y
Tactic: rw [← sub_eq_zero, ← map_sub, h₃]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 - y) = 0) → ∃ (c : ↥M), c • x = c • y
have exists_of_eq : (∃ (m : ↥M), m • x = m • y) → ∃ (c : ↥M), c • x = c • y
Tactic: simp_rw [smul_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 = ⊤
have rw : Subsingleton M' ↔ ⊤ ≤ g.ker
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
have refine : ∀ (H : ⊤ ≤ g.ker) (x : M'), x = 0
Tactic: refine ⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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'
⊢ x = 0
have obtain : ∀ (x : M) (s : ↥S), Function.uncurry (mk' g) (x, s) = 0
Tactic: obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
have simp_rw : g.ker = ⊤ ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
have simp_rw₁ : ⊤ ≤ g.ker ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
have simp_rw₂ : (∀ ⦃x : M⦄, Membership.mem (γ := Submodule R M) ⊤ x → x ∈ g.ker) ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
have simp_rw₃ : (∀ ⦃x : M⦄, Membership.mem (γ := Submodule R M) ⊤ x → ∃ r ∈ S, r • x = 0) ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
have simp_rw₄ : (∀ ⦃x : M⦄, True → ∃ r ∈ S, r • x = 0) ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Subsingleton M'
have rw : ∀ (m : M), ∃ r ∈ S, r • m = 0
Tactic: rw [subsingleton_iff S g]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ ∃ r ∈ S, r • m = 0
have h : 1 ∈ S ∧ HSMul.hSMul.{u_6, u_8, u_8} (α := R) 1 m = 0
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ Subsingleton (LocalizedModule S M)
have rw : ∀ (m : M), ∃ r ∈ S, r • m = 0
Tactic: rw [IsLocalizedModule.subsingleton_iff S (LocalizedModule.mkLinearMap S M)]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ ∃ r ∈ S, r • m = 0
have w : R
Tactic: use 1, S.one_mem, Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ ∃ r ∈ S, r • m = 0
have left : 1 ∈ S
Tactic: use 1, S.one_mem, Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ ∃ r ∈ S, r • m = 0
have right : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = 0
Tactic: use 1, S.one_mem, Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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)
⊢ x = y
have pos : ∀ (hS₀ : 0 ∈ S), x = y
Tactic: by_cases hS₀ : 0 ∈ S
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ x = y
have neg : ∀ (hS₀ : 0 ∉ S), x = y
Tactic: by_cases hS₀ : 0 ∈ S
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
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 = y
have this : Subsingleton N
Tactic: have : Subsingleton N := (IsLocalizedModule.subsingleton_iff S f).2 fun _ ↦ ⟨0, hS₀, by simp⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 = y
have 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
Tactic: obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective S c
Cleared hypotheses: c, hc, hxy
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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)
⊢ x = y
have 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
Tactic: obtain ⟨⟨m₁, t₁⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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)
⊢ Function.uncurry (mk' f) (m₁, t₁) = y
have 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₂)
Tactic: obtain ⟨⟨m₂, t₂⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
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₂)))
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
have hS₁ : ∀ 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₀
Cleared hypotheses: hS