awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
rw : k * x - k * y = 0
rw₁ : k * x = k * y
rw₂ rw₃ : k * y = k * y
⊢ k * (x - y) = 0

Tactic:
rw [mul_sub, sub_eq_zero, h']

Premises used: mul_sub, sub_eq_zero
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
⊢ IsRightRegular k

Tactic:
fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ ?_)

Premises used: sub_eq_zero, HSub.hSub, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
refine : ∀ (x y : α) (h' : x * k = y * k), (x - y) * k = 0
⊢ IsRightRegular k

Tactic:
refine fun x y (h' : x * k = y * k) => sub_eq_zero.mp (h _ ?_)

Premises used: sub_eq_zero, HSub.hSub, Iff.mp
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
rw : x * k - y * k = 0
rw₁ : x * k = y * k
rw₂ rw₃ : y * k = y * k
⊢ (x - y) * k = 0

Tactic:
rw [sub_mul, sub_eq_zero, h']

Premises used: sub_eq_zero, sub_mul
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
inst_1 : NoZeroDivisors α
k : α
hk : k ≠ 0
⊢ IsRegular k

Tactic:
⟨isLeftRegular_of_non_zero_divisor k fun _ h =>
      (NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left hk,
    isRightRegular_of_non_zero_divisor k fun _ h =>
      (NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hk⟩

Premises used: isLeftRegular_of_non_zero_divisor, isRightRegular_of_non_zero_divisor, Or.resolve_left, IsRegular.mk, Or.resolve_right, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : NonUnitalNonAssocRing α
inst_2 : NoZeroDivisors α
h : IsRegular.{u_1} (R := α) 0
⊢ False

Tactic:
not_not.mpr h.left not_isLeftRegular_zero

Premises used: Iff.mpr, Classical.not_not, not_isLeftRegular_zero, IsRegular.left
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : NonUnitalNonAssocRing α
inst_2 : NoZeroDivisors α
h : IsRegular.{u_1} (R := α) 0
⊢ False

Tactic:
exact not_not.mpr h.left not_isLeftRegular_zero

Premises used: Iff.mpr, Classical.not_not, not_isLeftRegular_zero, IsRegular.left
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z

Tactic:
(isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxy hxz ↦ ?_, fun h x y eq ↦ ?_⟩

Premises used: isDedekindFiniteMonoid_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
refine_1 : ∀ (h : ∀ {a b : α}, a * b = 1 → b * a = 1) (x y z : α) (hxy : x * y = 1) (hxz : x * z = 1), y = z
refine_2 : ∀ (h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z) (x y : α) (eq : x * y = 1), y * x = 1
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z

Tactic:
refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxy hxz ↦ ?_, fun h x y eq ↦ ?_⟩

Premises used: isDedekindFiniteMonoid_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ {a b : α}, a * b = 1 → b * a = 1
x y z : α
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z

Tactic:
simpa [← mul_assoc, h hxz] using congr_arg (z * ·) hxy

Premises used: HMul.hMul, mul_assoc, congr_arg
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
rw : x * (1 - y * x) + x * y = 1
rw₁ : x * 1 - x * (y * x) + x * y = 1
rw₂ : x * 1 - x * y * x + x * y = 1
rw₃ : x * 1 - 1 * x + 1 = 1
rw₄ : x - 1 * x + 1 = 1
rw₅ : x - x + 1 = 1
rw₆ : HAdd.hAdd (α := α) 0 1 = 1
rw₇ rw₈ : Eq.{u_1 + 1} (α := α) 1 1
⊢ x * (1 - y * x + y) = 1

Tactic:
rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]

Premises used: mul_sub, sub_self, mul_assoc, zero_add, mul_add, mul_one, one_mul
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ y = 1 - y * x + y

Tactic:
have := h _ _ (1 - y * x + y) eq <| by
    rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y = 1 - y * x + y
refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
refine_2₁ : ∀ (this : 1 = y * x), y * x = 1
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : ∀ (this : y * x = 1), y * x = 1
⊢ y * x = 1

Tactic:
rwa [right_eq_add, sub_eq_zero, eq_comm] at this

Premises used: sub_eq_zero, eq_comm, right_eq_add
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y

Tactic:
(isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxz hyz ↦ ?_, fun h x y eq ↦ ?_⟩

Premises used: isDedekindFiniteMonoid_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
refine_1 : ∀ (h : ∀ {a b : α}, a * b = 1 → b * a = 1) (x y z : α) (hxz : x * z = 1) (hyz : y * z = 1), x = y
refine_2 : ∀ (h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y) (x y : α) (eq : x * y = 1), y * x = 1
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y

Tactic:
refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxz hyz ↦ ?_, fun h x y eq ↦ ?_⟩

Premises used: isDedekindFiniteMonoid_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ {a b : α}, a * b = 1 → b * a = 1
x y z : α
hxz : x * z = 1
hyz : y * z = 1
⊢ x = y

Tactic:
simpa [mul_assoc, h hyz] using congr_arg (· * y) hxz

Premises used: HMul.hMul, mul_assoc, congr_arg
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
rw : (1 - y * x) * y + x * y = 1
rw₁ : 1 * y - y * x * y + x * y = 1
rw₂ : 1 * y - y * (x * y) + x * y = 1
rw₃ : 1 * y - y * 1 + 1 = 1
rw₄ : y - y * 1 + 1 = 1
rw₅ : y - y + 1 = 1
rw₆ : HAdd.hAdd (α := α) 0 1 = 1
rw₇ rw₈ : Eq.{u_1 + 1} (α := α) 1 1
⊢ (1 - y * x + x) * y = 1

Tactic:
rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]

Premises used: add_mul, sub_self, mul_assoc, zero_add, sub_mul, mul_one, one_mul
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ x = 1 - y * x + x

Tactic:
have := h _ (1 - y * x + x) _ eq <| by
    rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : x = 1 - y * x + x
refine_2 : ∀ (this : 1 - y * x = 0), y * x = 1
refine_2₁ : ∀ (this : 1 = y * x), y * x = 1
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : ∀ (this : y * x = 1), y * x = 1
⊢ y * x = 1

Tactic:
rwa [right_eq_add, sub_eq_zero, eq_comm] at this

Premises used: sub_eq_zero, eq_comm, right_eq_add
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : Distrib R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x + x') (y + y')

Tactic:
simp only [SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]

Premises used: SemiconjBy, SemiconjBy.eq, right_distrib, left_distrib
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : Distrib R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + b) x y

Tactic:
simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]

Premises used: SemiconjBy, SemiconjBy.eq, right_distrib, left_distrib
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)

Tactic:
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

Premises used: SemiconjBy, SemiconjBy.eq, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a x y : R
⊢ SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y

Tactic:
⟨fun h => neg_neg x ▸ neg_neg y ▸ h.neg_right, SemiconjBy.neg_right⟩

Premises used: Eq.rec, neg_neg, Iff.intro, SemiconjBy.neg_right
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y

Tactic:
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

Premises used: SemiconjBy, SemiconjBy.eq, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a x y : R
⊢ SemiconjBy (-a) x y ↔ SemiconjBy a x y

Tactic:
⟨fun h => neg_neg a ▸ h.neg_left, SemiconjBy.neg_left⟩

Premises used: Eq.rec, neg_neg, Iff.intro, SemiconjBy.neg_left
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : MulOneClass R
inst_1 : HasDistribNeg R
a : R
⊢ SemiconjBy a (-1) (-1)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : MulOneClass R
inst_1 : HasDistribNeg R
x : R
⊢ SemiconjBy (-1) x x

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x - x') (y - y')

Tactic:
simpa only [sub_eq_add_neg] using h.add_right h'.neg_right

Premises used: sub_eq_add_neg, SemiconjBy.add_right, SemiconjBy.neg_right
-- Module: Mathlib.Algebra.Ring.Semiconj
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y

Tactic:
simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left

Premises used: sub_eq_add_neg, SemiconjBy.add_left, SemiconjBy.neg_left
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : One R
inst_2 : Mul R
h : ¬IsSumSq.{u_1} (R := R) (-1)
⊢ ∀ {s : R} (hs : IsSumSq s), 1 + s ≠ 0

Tactic:
aesop (add simp add_eq_zero_iff_neg_eq)

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
hn : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (↑(1 + n) : R) 0

Tactic:
rw [add_comm] at hn

Premises used: add_comm
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑(1 + n) : R) 0
⊢ HAdd.hAdd (α := R) 1 (↑n : R) = 0

Tactic:
push_cast at hn
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : HAdd.hAdd (α := R) 1 (↑n : R) = 0
⊢ IsSumSq.{u_1} (R := R) (↑n : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : HAdd.hAdd (α := R) 1 (↑n : R) = 0
⊢ n + 1 = 0

Tactic:
simpa using IsSemireal.one_add_ne_zero (by simp) hn

Premises used: IsSemireal.one_add_ne_zero
-- Module: Mathlib.Algebra.Ring.Semireal.Defs
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : IsSemireal R
n : ℕ
hn : Eq.{u_1 + 1} (α := R) (↑n : R) 0
zero : ∀ (hn : Eq.{u_1 + 1} (α := R) (↑0 : R) 0), Eq (α := ℕ) 0 0
succ : ∀ (n : ℕ) (hn : Eq.{u_1 + 1} (α := R) (↑(n + 1) : R) 0), n + 1 = 0
⊢ n = 0

Tactic:
cases n with
    | zero => rfl
    | succ n =>
      rw [add_comm] at hn
      push_cast at hn
      simpa using IsSemireal.one_add_ne_zero (by simp) hn

Premises used: add_comm, IsSemireal.one_add_ne_zero
-- Module: Mathlib.Algebra.Ring.Shrink
Goal:
α : Type u_1
inst : Small.{v, u_1} α
inst_1 : Semiring α
inst_2 : IsDomain α
⊢ IsDomain.{v} (Shrink.{v, u_1} α)

Tactic:
(Shrink.ringEquiv α).isDomain

Premises used: RingEquiv.toEquiv, Shrink.ringEquiv, Equiv.isDomain
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
rw : -m * n ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -(m * n) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
rw [← neg_mul]

Premises used: neg_mul
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -m * n ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
AddSubmonoid.mul_mem_mul (M.neg_mem hm) hn

Premises used: Set.Mem, AddSubgroup.neg_mem, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -m * n ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
exact AddSubmonoid.mul_mem_mul (M.neg_mem hm) hn

Premises used: AddSubgroup.neg_mem, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
rw : -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -(r₁ + r₂) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
rw [neg_add]

Premises used: neg_add
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
(M.1 * N.1).add_mem h₁ h₂

Premises used: AddSubmonoid.add_mem, HMul.hMul, Set.Mem, AddSubgroup.toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M_1 : Type u_2
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
x : R
h : x ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
r₁ r₂ : R
h₁ : -r₁ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
h₂ : -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
⊢ -r₁ + -r₂ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
exact (M.1 * N.1).add_mem h₁ h₂

Premises used: AddSubmonoid.add_mem, HMul.hMul, AddSubgroup.toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
M N : AddSubgroup R
⊢ (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subgroup
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : AddSubgroup M
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 s = ⊥

Tactic:
simp [eq_bot_iff_forall, pointwise_smul_def]

Premises used: AddSubgroup.eq_bot_iff_forall, AddSubgroup.pointwise_smul_def
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r : R
hr : r ∈ (↑S : Set R)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)

Tactic:
mem_closure.mpr fun y hy => hy (mul_mem hr hb)

Premises used: Iff.mpr, AddSubmonoid.mem_closure, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r : R
hr : r ∈ (↑S : Set R)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)

Tactic:
exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)

Premises used: Iff.mpr, AddSubmonoid.mem_closure, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
hb : b ∈ S
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (0 * b)

Tactic:
simp only [zero_mul, zero_mem _]

Premises used: MulZeroClass.zero_mul, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r s : R
hx : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) r
hy : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) s
hr : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)
hs : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (s * b)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) ((r + s) * b)

Tactic:
simpa only [add_mul] using add_mem hr hs

Premises used: add_mul, AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : b ∈ S
mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b)
zero : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (0 * b)
add :
  ∀ (r s : R),
    Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) r →
      Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) s →
        ∀ (hr : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (r * b))
          (hs : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (s * b)),
          Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) ((r + s) * b)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)

Tactic:
induction ha using closure_induction with
  | mem r hr => exact mem_closure.mpr fun y hy => hy (mul_mem hr hb)
  | zero => simp only [zero_mul, zero_mem _]
  | add r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs

Premises used: add_mul, MulZeroClass.zero_mul, AddSubmonoid.add, ZeroMemClass.zero_mem, AddSubmonoid.zero
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
r : R
hr : r ∈ (↑S : Set R)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)

Tactic:
MulMemClass.mul_right_mem_add_closure ha hr

Premises used: MulMemClass.mul_right_mem_add_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
r : R
hr : r ∈ (↑S : Set R)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)

Tactic:
exact MulMemClass.mul_right_mem_add_closure ha hr

Premises used: MulMemClass.mul_right_mem_add_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * 0)

Tactic:
simp only [mul_zero, zero_mem _]

Premises used: MulZeroClass.mul_zero, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
r s : R
hx : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) r
hy : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) s
hr : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)
hs : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * s)
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * (r + s))

Tactic:
simpa only [mul_add] using add_mem hr hs

Premises used: AddMemClass.add_mem, mul_add
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) a
hb : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) b
mem : ∀ (r : R) (hr : r ∈ (↑S : Set R)), Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r)
zero : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * 0)
add :
  ∀ (r s : R),
    Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) r →
      Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) s →
        ∀ (hr : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * r))
          (hs : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * s)),
          Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * (r + s))
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)

Tactic:
induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | zero => simp only [mul_zero, zero_mem _]
  | add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs

Premises used: AddSubmonoid.add, MulZeroClass.mul_zero, mul_add, ZeroMemClass.zero_mem, AddSubmonoid.zero
-- Module: Mathlib.Algebra.Ring.Submonoid.Basic
Goal:
M : Type u_1
R : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike M R
inst_2 : MulMemClass M R
S : M
a b : R
ha : a ∈ S
hb : Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) b
⊢ Membership.mem (γ := AddSubmonoid R) (closure (↑S : Set R)) (a * b)

Tactic:
mul_mem_add_closure (mem_closure.mpr fun _sT hT => hT ha) hb

Premises used: Iff.mpr, MulMemClass.mul_mem_add_closure, AddSubmonoid.mem_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
⊢ Eq (α := AddSubmonoid R) 1 (AddMonoidHom.mrange (F := ℕ →+ R) (Nat.castAddMonoidHom R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
n : ℕ
⊢ Membership.mem (γ := AddSubmonoid R) 1 (↑n : R)

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
x : R
⊢ Membership.mem (γ := AddSubmonoid R) 1 x ↔ ∃ (n : ℕ), (↑n : R) = x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
rw :
  Eq (α := AddSubmonoid R) (AddMonoidHom.mrange (F := ℕ →+ R) (Nat.castAddMonoidHom R))
    (AddMonoidHom.mrange (F := ℕ →+ R) ((multiplesHom R : (a : R) → ℕ →+ R) 1))
⊢ Eq (α := AddSubmonoid R) 1 (closure {1})

Tactic:
rw [closure_singleton_eq, one_eq_mrange]

Premises used: AddSubmonoid.closure_singleton_eq, AddSubmonoid.one_eq_mrange
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
e_f : Eq (α := ℕ →+ R) (Nat.castAddMonoidHom R) ((multiplesHom R : (a : R) → ℕ →+ R) 1)
⊢ Eq (α := AddSubmonoid R) (AddMonoidHom.mrange (F := ℕ →+ R) (Nat.castAddMonoidHom R))
    (AddMonoidHom.mrange (F := ℕ →+ R) ((multiplesHom R : (a : R) → ℕ →+ R) 1))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
e_f :
  Eq (α := R) ((Nat.castAddMonoidHom R : (a : ℕ) → R) 1 : R)
    (((multiplesHom R : (a : R) → ℕ →+ R) 1 : (a : ℕ) → R) 1 : R)
⊢ Eq (α := ℕ →+ R) (Nat.castAddMonoidHom R) ((multiplesHom R : (a : R) → ℕ →+ R) 1)

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : AddMonoidWithOne R
⊢ Eq (α := R) ((Nat.castAddMonoidHom R : (a : ℕ) → R) 1 : R)
    (((multiplesHom R : (a : R) → ℕ →+ R) 1 : (a : ℕ) → R) 1 : R)

Tactic:
simp