awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
inst_2 : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst_3 : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : R) ∈ s

Tactic:
exact natCast_mem s n

Premises used: natCast_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R_1 : Type u
S_1 : Type v
inst : NonAssocSemiring R_1
S : Type u_1
R : Type u
x : NonAssocSemiring R
inst_1 : SetLike S R
h : SubsemiringClass S R
⊢ AddSubmonoidWithOneClass S R

Tactic:
{ h with }

Premises used: AddSubmonoidWithOneClass.mk
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : SetLike S R
hSR : SubsemiringClass S R
s : S
inst_2 : Nontrivial R
⊢ Nontrivial.{u} ↥s

Tactic:
nontrivial_of_ne 0 1 fun H => zero_ne_one (congr_arg Subtype.val H)

Premises used: zero_ne_one, nontrivial_of_ne, congr_arg, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : SetLike S R
hSR : SubsemiringClass S R
s : S
inst_2 : NoZeroDivisors R
⊢ NoZeroDivisors.{u} ↥s

Tactic:
Subtype.coe_injective.noZeroDivisors _ rfl fun _ _ => rfl

Premises used: Subtype.coe_injective, Function.Injective.noZeroDivisors, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : SetLike S R
hSR : SubsemiringClass S R
s : S
⊢ Eq (α := (a : ↥s) → R) (⇑(subtype s) : (a : ↥s) → R) (Subtype.val (p := fun (x : R) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : SetLike S R
hSR : SubsemiringClass S R
s : S
x : ↥s
⊢ (subtype s : (a : ↥s) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : SetLike S R
hSR : SubsemiringClass S R
s : S
x : ↥s
⊢ ∀ ⦃a₂ : ↥s⦄, Eq (α := R) ((subtype s : (a : ↥s) → R) x : R) ((subtype s : (a : ↥s) → R) a₂ : R) → x = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
p q : Subsemiring R
h : Eq.{u + 1} (α := Set R) ((fun (s : Subsemiring R) ↦ s.carrier) p) ((fun (s : Subsemiring R) ↦ s.carrier) q)
mk :
  ∀ (toSubmonoid : Submonoid R)
    (add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
    (zero_mem' : 0 ∈ toSubmonoid.carrier)
    (h :
      Eq.{u + 1} (α := Set R)
        ((fun (s : Subsemiring R) ↦ s.carrier)
          { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
        ((fun (s : Subsemiring R) ↦ s.carrier) q)),
    { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
q : Subsemiring R
toSubmonoid : Submonoid R
add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem' : 0 ∈ toSubmonoid.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
    ((fun (s : Subsemiring R) ↦ s.carrier) q)
mk :
  ∀ (toSubmonoid_1 : Submonoid R)
    (add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier)
    (zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier)
    (h :
      Eq.{u + 1} (α := Set R)
        ((fun (s : Subsemiring R) ↦ s.carrier)
          { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
        ((fun (s : Subsemiring R) ↦ s.carrier)
          { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 })),
    { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } =
      { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 }
⊢ { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
toSubmonoid : Submonoid R
add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem' : 0 ∈ toSubmonoid.carrier
toSubmonoid_1 : Submonoid R
add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier
zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 })
mk : toSubmonoid = toSubmonoid_1
⊢ { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' : Subsemiring R } =
    { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
toSubmonoid : Submonoid R
add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem' : 0 ∈ toSubmonoid.carrier
toSubmonoid_1 : Submonoid R
add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier
zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 })
⊢ toSubmonoid = toSubmonoid_1

Tactic:
SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
toSubmonoid : Submonoid R
add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem' : 0 ∈ toSubmonoid.carrier
toSubmonoid_1 : Submonoid R
add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier
zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid, add_mem' := @add_mem', zero_mem' := zero_mem' })
    ((fun (s : Subsemiring R) ↦ s.carrier)
      { toSubmonoid := toSubmonoid_1, add_mem' := @add_mem'_1, zero_mem' := zero_mem'_1 })
⊢ toSubmonoid = toSubmonoid_1

Tactic:
exact SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x : R
⊢ x ∈ s.toSubmonoid ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S : Subsemiring R
x : R
⊢ x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x : R
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S : Subsemiring R
⊢ (↑S.toNonUnitalSubsemiring : Set R) = (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
toSubmonoid : Submonoid R
add_mem : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem : 0 ∈ toSubmonoid.carrier
x : R
⊢ x ∈ { toSubmonoid := toSubmonoid, add_mem' := @add_mem, zero_mem' := zero_mem : Subsemiring R } ↔ x ∈ toSubmonoid

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
toSubmonoid : Submonoid R
add_mem : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier
zero_mem : 0 ∈ toSubmonoid.carrier
⊢ (↑{ toSubmonoid := toSubmonoid, add_mem' := @add_mem, zero_mem' := zero_mem : Subsemiring R } : Set R) =
    (↑toSubmonoid : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S T : Subsemiring R
h : ∀ (x : R), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S : Subsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ Function.Injective.{u + 1, u + 1} (α := Subsemiring R) toNonUnitalSubsemiring

Tactic:
fun S₁ S₂ h => SetLike.ext'_iff.2
    (show (S₁.toNonUnitalSubsemiring : Set R) = S₂ from SetLike.ext'_iff.1 h)

Premises used: Iff.mpr, Iff.mp, SetLike.ext'_iff, Function.Injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring R
⊢ S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂

Tactic:
toNonUnitalSubsemiring_injective.eq_iff

Premises used: Function.Injective.eq_iff, Subsemiring.toNonUnitalSubsemiring_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S : Subsemiring R
⊢ 1 ∈ S.toNonUnitalSubsemiring

Tactic:
S.one_mem

Premises used: Set.Mem, Subsemiring.toSubmonoid, Submonoid.one_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
simpa only [← hm] using sm.mul_mem

Premises used: Submonoid.mul_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ 1 ∈ s

Tactic:
hm ▸ sm.one_mem

Premises used: Eq.rec, Submonoid.one_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ 1 ∈ s

Tactic:
exact hm ▸ sm.one_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
x y : R
⊢ x ∈ s → y ∈ s → x + y ∈ s

Tactic:
simpa only [← ha] using sa.add_mem

Premises used: AddSubmonoid.add_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ 0 ∈ s

Tactic:
ha ▸ sa.zero_mem

Premises used: AddSubmonoid.zero_mem, Eq.rec
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ 0 ∈ s

Tactic:
exact ha ▸ sa.zero_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
x : R
⊢ x ∈ Subsemiring.mk' s sm hm sa ha ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ (Subsemiring.mk' s sm hm sa ha).toSubmonoid = sm

Tactic:
SetLike.coe_injective hm.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ (Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa

Tactic:
SetLike.coe_injective ha.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ 1 ∈ s

Tactic:
one_mem s

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ 0 ∈ s

Tactic:
zero_mem s

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x y : R
⊢ x ∈ s → y ∈ s → x + y ∈ s

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ Eq.{u + 1} (α := R) (↑1 : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ Eq.{u + 1} (α := R) (↑0 : R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x y : ↥s
⊢ (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x y : ↥s
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring R
inst_2 : Nontrivial R
⊢ Nontrivial.{u} ↥s

Tactic:
nontrivial_of_ne 0 1 fun H => zero_ne_one (congr_arg Subtype.val H)

Premises used: zero_ne_one, nontrivial_of_ne, congr_arg, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u_1
inst : Semiring R
s : Subsemiring R
x : R
hx : x ∈ s
n : ℕ
⊢ x ^ n ∈ s

Tactic:
pow_mem hx n

Premises used: pow_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u_1
inst : Semiring R
s : Subsemiring R
x : ↥s
n : ℕ
⊢ (↑(x ^ n) : R) = (↑x : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x : ↥s
⊢ (s.subtype : (a : ↥s) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ Function.Injective (α := ↥s) (β := R) (⇑s.subtype : (a : ↥s) → R)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ Eq (α := (a : ↥s) → R) (⇑s.subtype : (a : ↥s) → R) (Subtype.val (p := fun (x : R) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x : R
hx : x ∈ s
n : ℕ
⊢ n • x ∈ s

Tactic:
nsmul_mem hx n

Premises used: nsmul_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ (↑s.toSubmonoid : Set R) = (↑s : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ s.carrier = (↑s : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
x : R
⊢ x ∈ s.toAddSubmonoid ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ (↑s.toAddSubmonoid : Set R) = (↑s : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
x : R
⊢ Membership.mem (γ := Subsemiring R) ⊤ x

Tactic:
Set.mem_univ x

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

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
p p' : Subsemiring R
⊢ (↑(p ⊓ p') : Set R) = (↑p : Set R) ∩ (↑p' : Set R)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
p p' : Subsemiring R
x : R
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σR : Type u_1
inst_2 : SetLike σR R
inst_3 : SubsemiringClass σR R
f : R →+* S
s : σR
x : ↥s
⊢ Eq.{v + 1} (α := S) ((f.domRestrict s : (a : ↥s) → S) x : S) ((f : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f g : R →+* S
x : R
⊢ x ∈ f.eqLocusS g ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((g : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
⊢ f.eqLocusS f = ⊤

Tactic:
SetLike.ext fun _ => eq_self_iff_true _

Premises used: SetLike.ext, DFunLike.coe, eq_self_iff_true
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S : Subsemiring R
⊢ S.toNonUnitalSubsemiring.toSubsemiring ⋯ = S

Tactic:
rfl

Premises used: NonUnitalSubsemiring.toSubsemiring, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
R : Type u
inst : NonAssocSemiring R
S : NonUnitalSubsemiring R
h1 : 1 ∈ S
⊢ (S.toSubsemiring h1).toNonUnitalSubsemiring = S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring R
a b : Rᵐᵒᵖ
hx : a ∈ S.op.carrier
hy : b ∈ S.op.carrier
⊢ a + b ∈ S.op.carrier

Tactic:
simp_all [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
x : Rᵐᵒᵖ
S : Subsemiring R
⊢ x ∈ S.op ↔ MulOpposite.unop x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring Rᵐᵒᵖ
a b : R
hx : a ∈ S.unop.carrier
hy : b ∈ S.unop.carrier
⊢ a + b ∈ S.unop.carrier

Tactic:
simp_all [add_mem]

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
x : R
S : Subsemiring Rᵐᵒᵖ
⊢ x ∈ S.unop ↔ MulOpposite.op x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring R
⊢ S.op.unop = S

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, MulOpposite.unop, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring Rᵐᵒᵖ
⊢ S.unop.op = S

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, MulOpposite, setOf, Set.preimage, Subsemiring.op, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ : Subsemiring R
S₂ : Subsemiring Rᵐᵒᵖ
⊢ S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ : Subsemiring Rᵐᵒᵖ
S₂ : Subsemiring R
⊢ S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring R
⊢ S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S₁ S₂ : Subsemiring Rᵐᵒᵖ
⊢ S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subsemiring R) Subsemiring.op

Tactic:
opEquiv.injective

Premises used: OrderIso.injective, Subsemiring.op, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subsemiring Rᵐᵒᵖ) Subsemiring.unop

Tactic:
opEquiv.symm.injective

Premises used: OrderIso.symm, OrderIso.injective, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S T : Subsemiring R
⊢ S.op = T.op ↔ S = T

Tactic:
opEquiv.eq_iff_eq

Premises used: RelIso.eq_iff_eq, Subsemiring.op, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S T : Subsemiring Rᵐᵒᵖ
⊢ S.unop = T.unop ↔ S = T

Tactic:
opEquiv.symm.eq_iff_eq

Premises used: RelIso.eq_iff_eq, OrderIso.symm, Subsemiring.unop, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ Eq.{u_2 + 1} (α := Subsemiring Rᵐᵒᵖ) (Subsemiring.op ⊥) ⊥

Tactic:
opEquiv.map_bot

Premises used: Subsemiring.op, OrderIso.map_bot, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring R
⊢ S.op = ⊥ ↔ S = ⊥

Tactic:
op_injective.eq_iff' op_bot

Premises used: Subsemiring.op_injective, Function.Injective.eq_iff', Subsemiring.op_bot
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ Eq.{u_2 + 1} (α := Subsemiring R) (Subsemiring.unop ⊥) ⊥

Tactic:
opEquiv.symm.map_bot

Premises used: OrderIso.symm, Subsemiring.unop, OrderIso.map_bot, Subsemiring.opEquiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring Rᵐᵒᵖ
⊢ S.unop = ⊥ ↔ S = ⊥

Tactic:
unop_injective.eq_iff' unop_bot

Premises used: Function.Injective.eq_iff', Subsemiring.unop_injective, Subsemiring.unop_bot
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
⊢ Eq.{u_2 + 1} (α := Subsemiring Rᵐᵒᵖ) (Subsemiring.op ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, Set.univ, setOf, Set.preimage, Subsemiring.op, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Goal:
R : Type u_2
inst : NonAssocSemiring R
S : Subsemiring R
⊢ S.op = ⊤ ↔ S = ⊤

Tactic:
op_injective.eq_iff' op_top

Premises used: Subsemiring.op_injective, Function.Injective.eq_iff', Subsemiring.op_top