awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : Membership.mem (γ := AddSubmonoid R) ⊥ m
n : R
h : n ∈ S
rw : ∀ (hm : m = 0), ∀ n ∈ S, m * n = 0
⊢ Membership.mem (γ := AddSubmonoid R) ⊥ (m * n)

Tactic:
rw [AddSubmonoid.mem_bot] at hm ⊢

Premises used: AddSubmonoid.mem_bot
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
h : n ∈ S
rw : 0 * n = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ m * n = 0

Tactic:
rw [hm, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P Q : AddSubmonoid R
hmp : M ≤ P
hnq : N ≤ Q
⊢ M * N ≤ P * Q

Tactic:
smul_le_smul hmp hnq

Premises used: Set.Mem, AddSubmonoid.smul_le_smul, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
h : M ≤ N
⊢ M * P ≤ N * P

Tactic:
smul_le_smul_left h

Premises used: Set.Mem, AddSubmonoid.smul_le_smul_left, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
h : N ≤ P
⊢ M * N ≤ M * P

Tactic:
smul_le_smul_right h

Premises used: Set.Mem, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom, AddSubmonoid.smul_le_smul_right
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R)

Tactic:
smul_subset_smul

Premises used: Set.Mem, AddSubmonoid.smul_subset_smul, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
⊢ M * (N ⊔ P) = M * N ⊔ M * P

Tactic:
addSubmonoid_smul_sup

Premises used: Set.Mem, setOf, AddMonoidHom.mulLeft, AddSubmonoid.addSubmonoid_smul_sup, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
mn : R
hmn : mn ∈ M ⊔ N
p : R
hp : p ∈ P
obtain : ∀ (m : R) (hm : m ∈ M) (n : R) (hn : n ∈ N) (hmn : m + n ∈ M ⊔ N), (m + n) * p ∈ M * P ⊔ N * P
⊢ mn * p ∈ M * P ⊔ N * P

Tactic:
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn

Premises used: Iff.mp, AddSubmonoid.mem_sup, rfl
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
rw : m * p + n * p ∈ M * P ⊔ N * P
⊢ (m + n) * p ∈ M * P ⊔ N * P

Tactic:
rw [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P

Tactic:
add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp

Premises used: Set.Mem, AddSubmonoid.add_mem_sup, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P

Tactic:
exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp

Premises used: AddSubmonoid.add_mem_sup, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i) s
t : R
ht : t ∈ T
simp_rw : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) 0
⊢ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (0 * t)

Tactic:
simp_rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i) s
t : R
ht : t ∈ T
⊢ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) 0

Tactic:
apply zero_mem

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i) s
t : R
ht : t ∈ T
x x_1 : R
simp_rw :
  Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t) →
    Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x_1 * t) →
      Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t + x_1 * t)
⊢ (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) x →
    (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) x_1 →
      (fun (x : R) ↦ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t)) (x + x_1)

Tactic:
simp_rw [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i) s
t : R
ht : t ∈ T
x x_1 : R
⊢ Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t) →
    Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x_1 * t) →
      Membership.mem (γ := AddSubmonoid R) (⨆ (i : ι), S i * T) (x * t + x_1 * t)

Tactic:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid R
⊢ T * ⨆ (i : ι), S i = ⨆ (i : ι), T * S i

Tactic:
smul_iSup T S

Premises used: AddSubmonoid.smul_iSup, AddMonoidHom.mulLeft, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
h : ∀ m ∈ M, ∀ n ∈ N, Commute m n
⊢ M * N = N * M

Tactic:
le_antisymm (mul_le.mpr fun m hm n hn ↦ h m hm n hn ▸ mul_mem_mul hn hm)
    (mul_le.mpr fun n hn m hm ↦ h m hm n hn ▸ mul_mem_mul hm hn)

Premises used: Iff.mpr, Eq.rec, le_antisymm, AddSubmonoid.mul_le, Eq.symm, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ -x * y = -(x * y)

Tactic:
le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)

Premises used: Iff.mpr, AddSubmonoid.neg_le, le_antisymm, AddSubmonoid.mul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
refine_1 : ∀ (m : R) (hm : m ∈ -x) (n : R) (hn : n ∈ y), m * n ∈ -(x * y)
refine_2 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ y), m * n ∈ -(-x * y)
⊢ -x * y = -(x * y)

Tactic:
refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)

Premises used: Iff.mpr, le_antisymm, AddSubmonoid.mul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ -x
n : R
hn : n ∈ y
refine_1 : ∀ (hm : -m ∈ x), -m * n ∈ x * y
⊢ m * n ∈ -(x * y)

Tactic:
simp only [AddSubmonoid.mem_neg, ← neg_mul] at *

Premises used: AddSubmonoid.mem_neg, neg_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
refine_2 : -m * n ∈ -x * y
⊢ m * n ∈ -(-x * y)

Tactic:
simp only [AddSubmonoid.mem_neg, ← neg_mul] at *

Premises used: AddSubmonoid.mem_neg, neg_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m n : R
hn : n ∈ y
hm : -m ∈ x
⊢ -m * n ∈ x * y

Tactic:
mul_mem_mul hm hn

Premises used: Set.Mem, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m n : R
hn : n ∈ y
hm : -m ∈ x
⊢ -m * n ∈ x * y

Tactic:
exact mul_mem_mul hm hn

Premises used: AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y

Tactic:
mul_mem_mul (neg_mem_neg.2 hm) hn

Premises used: Iff.mpr, Set.Mem, AddSubmonoid.mul_mem_mul, Set.neg_mem_neg
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y

Tactic:
exact mul_mem_mul (neg_mem_neg.2 hm) hn

Premises used: Iff.mpr, AddSubmonoid.mul_mem_mul, Set.neg_mem_neg
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ x * -y = -(x * y)

Tactic:
le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)

Premises used: Iff.mpr, AddSubmonoid.neg_le, le_antisymm, AddSubmonoid.mul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
refine_1 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ -y), m * n ∈ -(x * y)
refine_2 : ∀ (m : R) (hm : m ∈ x) (n : R) (hn : n ∈ y), m * n ∈ -(x * -y)
⊢ x * -y = -(x * y)

Tactic:
refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_)

Premises used: Iff.mpr, le_antisymm, AddSubmonoid.mul_le
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ -y
refine_1 : ∀ (hn : -n ∈ y), m * -n ∈ x * y
⊢ m * n ∈ -(x * y)

Tactic:
simp only [AddSubmonoid.mem_neg, ← mul_neg] at *

Premises used: AddSubmonoid.mem_neg, mul_neg
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
refine_2 : m * -n ∈ x * -y
⊢ m * n ∈ -(x * -y)

Tactic:
simp only [AddSubmonoid.mem_neg, ← mul_neg] at *

Premises used: AddSubmonoid.mem_neg, mul_neg
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : -n ∈ y
⊢ m * -n ∈ x * y

Tactic:
mul_mem_mul hm hn

Premises used: Set.Mem, AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : -n ∈ y
⊢ m * -n ∈ x * y

Tactic:
exact mul_mem_mul hm hn

Premises used: AddSubmonoid.mul_mem_mul
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * -n ∈ x * -y

Tactic:
mul_mem_mul hm (neg_mem_neg.2 hn)

Premises used: Iff.mpr, Set.Mem, AddSubmonoid.mul_mem_mul, Set.neg_mem_neg
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M : Type u_1
R : Type u_2
A : Type u_3
inst : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * -n ∈ x * -y

Tactic:
exact mul_mem_mul hm (neg_mem_neg.2 hn)

Premises used: Iff.mpr, AddSubmonoid.mul_mem_mul, Set.neg_mem_neg
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
rw : closure 1 * M = M
rw₁ : HMul.hMul (α := AddSubmonoid R) (closure 1) (closure (↑M : Set R)) = closure (↑M : Set R)
rw₂ : Eq (α := AddSubmonoid R) (closure (1 * (↑M : Set R))) (closure (↑M : Set R))
rw₃ rw₄ : Eq (α := AddSubmonoid R) (closure (↑M : Set R)) (closure (↑M : Set R))
⊢ 1 * M = M

Tactic:
rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]

Premises used: AddSubmonoid.closure_eq, AddSubmonoid.one_eq_closure_one_set, one_mul, AddSubmonoid.closure_mul_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
M_1 : Type u_1
R : Type u_2
A : Type u_3
inst : NonAssocSemiring R
M : AddSubmonoid R
rw : M * closure 1 = M
rw₁ : HMul.hMul (α := AddSubmonoid R) (closure (↑M : Set R)) (closure 1) = closure (↑M : Set R)
rw₂ : Eq (α := AddSubmonoid R) (closure ((↑M : Set R) * 1)) (closure (↑M : Set R))
rw₃ rw₄ : Eq (α := AddSubmonoid R) (closure (↑M : Set R)) (closure (↑M : Set R))
⊢ M * 1 = M

Tactic:
rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]

Premises used: AddSubmonoid.closure_eq, AddSubmonoid.one_eq_closure_one_set, mul_one, AddSubmonoid.closure_mul_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : Semiring R
s : Set R
rw : Eq (α := AddSubmonoid R) 1 (closure (HPow.hPow (β := ℕ) s 0))
rw₁ : Eq.{u_2 + 1} (α := AddSubmonoid R) 1 (closure 1)
rw₂ rw₃ : Eq.{u_2 + 1} (α := AddSubmonoid R) (closure 1) (closure 1)
⊢ HPow.hPow (α := AddSubmonoid R) (β := ℕ) (closure s) 0 = closure (HPow.hPow (β := ℕ) s 0)

Tactic:
rw [pow_zero, pow_zero, one_eq_closure_one_set]

Premises used: pow_zero, AddSubmonoid.one_eq_closure_one_set
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : Semiring R
s : Set R
n : ℕ
rw : HPow.hPow (α := AddSubmonoid R) (closure s) n * closure s = closure (s ^ (n + 1))
rw₁ : HPow.hPow (α := AddSubmonoid R) (closure s) n * closure s = closure (s ^ n * s)
rw₂ : HMul.hMul (α := AddSubmonoid R) (closure (s ^ n)) (closure s) = closure (s ^ n * s)
rw₃ rw₄ : Eq (α := AddSubmonoid R) (closure (s ^ n * s)) (closure (s ^ n * s))
⊢ HPow.hPow (α := AddSubmonoid R) (closure s) (n + 1) = closure (s ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

Premises used: pow_succ, AddSubmonoid.closure_mul_closure
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : Semiring R
s : AddSubmonoid R
n : ℕ
rw : s ^ n = HPow.hPow (α := AddSubmonoid R) (closure (↑s : Set R)) n
rw₁ rw₂ : s ^ n = s ^ n
⊢ s ^ n = closure ((↑s : Set R) ^ n)

Tactic:
rw [← closure_pow, closure_eq]

Premises used: AddSubmonoid.closure_eq, AddSubmonoid.closure_pow
-- Module: Mathlib.Algebra.Ring.Submonoid.Pointwise
Goal:
R : Type u_2
inst : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ (↑s : Set R) ^ n ⊆ (↑(s ^ n) : Set R)

Tactic:
(pow_eq_closure_pow_set s n).symm ▸ subset_closure

Premises used: AddSubmonoid.subset_closure, Eq.rec, AddSubmonoid.pow_eq_closure_pow_set, Eq.symm
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ StrictMono.{u, u} (α := Subring R) toSubsemiring

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ Monotone.{u, u} (α := Subring R) toSubsemiring

Tactic:
toSubsemiring_strictMono.monotone

Premises used: StrictMono.monotone, Subring.toSubsemiring_strictMono
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ StrictMono.{u, u} (α := Subring R) toAddSubgroup

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ Monotone.{u, u} (α := Subring R) toAddSubgroup

Tactic:
toAddSubgroup_strictMono.monotone

Premises used: StrictMono.monotone, Subring.toAddSubgroup_strictMono
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ StrictMono (β := Submonoid R) fun (s : Subring R) ↦ s.toSubmonoid

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ Monotone (β := Submonoid R) fun (s : Subring R) ↦ s.toSubmonoid

Tactic:
toSubmonoid_strictMono.monotone

Premises used: StrictMono.monotone, Subring.toSubmonoid_strictMono
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Subring R
l : List R
⊢ (∀ x ∈ l, x ∈ s) → l.prod ∈ s

Tactic:
list_prod_mem

Premises used: list_prod_mem, Set.Mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
l : List R
⊢ (∀ x ∈ l, x ∈ s) → l.sum ∈ s

Tactic:
list_sum_mem

Premises used: Set.Mem, list_sum_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : CommRing R
s : Subring R
m : Multiset R
⊢ (∀ a ∈ m, a ∈ s) → m.prod ∈ s

Tactic:
multiset_prod_mem _

Premises used: multiset_prod_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Subring R
m : Multiset R
⊢ (∀ a ∈ m, a ∈ s) → m.sum ∈ s

Tactic:
multiset_sum_mem _

Premises used: multiset_sum_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : CommRing R
s : Subring R
ι : Type u_2
t : Finset ι
f : ι → R
h : ∀ c ∈ t, f c ∈ s
⊢ ∏ i ∈ t, f i ∈ s

Tactic:
prod_mem h

Premises used: prod_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Subring R
ι : Type u_2
t : Finset ι
f : ι → R
h : ∀ c ∈ t, f c ∈ s
⊢ ∑ i ∈ t, f i ∈ s

Tactic:
sum_mem h

Premises used: sum_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
x : R
⊢ Membership.mem (γ := Subring R) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ (↑⊤ : Set R) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ Eq.{u + 1} (α := Subsemiring R) (toSubsemiring ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ Eq.{u + 1} (α := AddSubgroup R) (toAddSubgroup ⊤) ⊤

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Subring R
⊢ S.toSubsemiring = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
S : Subring R
⊢ S.toAddSubgroup = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Fintype R
⊢ Fintype.card.{u_1} ↥⊤ = Fintype.card R

Tactic:
Fintype.card_congr topEquiv.toEquiv

Premises used: Fintype.card_congr, RingEquiv.toEquiv, Subring.topEquiv
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring S
f : R →+* S
⊢ (↑(comap f s) : Set R) = (⇑f : (a : R) → S) ⁻¹' (↑s : Set S)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring S
f : R →+* S
x : R
⊢ x ∈ comap f s ↔ Membership.mem (α := S) s ((f : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
s : Subring T
g : S →+* T
f : R →+* S
⊢ comap f (comap g s) = comap (g.comp f) s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Subring.comap, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
⊢ (↑(map f s) : Set S) = (⇑f : (a : R) → S) '' (↑s : Set R)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
y : S
⊢ y ∈ map f s ↔ ∃ x ∈ s, (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
⊢ map (RingHom.id R) s = s

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
s : Subring R
g : S →+* T
f : R →+* S
⊢ map g (map f s) = map (g.comp f) s

Tactic:
SetLike.coe_injective <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
t : Subring S
⊢ map f s ≤ t ↔ s ≤ comap f t

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: Subring.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : ↥s
⊢ Eq.{v + 1} (α := S) ((↑((s.equivMapOfInjective f hf : (a : ↥s) → ↥(map f s)) x) : S) : S)
    ((f : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
⊢ (↑f.range : Set S) = Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
y : S
⊢ y ∈ f.range ↔ ∃ (x : R), (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
h : ∀ (x : S), x ∈ f.range ↔ x ∈ Subring.map f ⊤
⊢ f.range = Subring.map f ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
x : S
⊢ x ∈ f.range ↔ x ∈ Subring.map f ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
x : R
⊢ Membership.mem (α := S) f.range ((f : (a : R) → S) x : S)

Tactic:
mem_range.mpr ⟨x, rfl⟩

Premises used: Iff.mpr, RingHom.mem_range, Exists.intro, rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
g : S →+* T
f : R →+* S
⊢ Subring.map g f.range = (g.comp f).range

Tactic:
simpa only [range_eq_map] using (⊤ : Subring R).map_map g f

Premises used: Subring.map_map, RingHom.range_eq_map, Top.top
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
⊢ (↑⊥ : Set R) = Set.range Int.cast

Tactic:
RingHom.coe_range (Int.castRingHom R)

Premises used: Int.castRingHom, RingHom.coe_range
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
x : R
⊢ Membership.mem (γ := Subring R) ⊥ x ↔ ∃ (n : ℤ), (↑n : R) = x

Tactic:
RingHom.mem_range

Premises used: RingHom.mem_range, Set.Mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
p p' : Subring R
⊢ (↑(p ⊓ p') : Set R) = (↑p : Set R) ∩ (↑p' : Set R)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl