awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
t : Subring S
h : t ≤ f.range
⊢ map f (comap f t) = t

Tactic:
simpa only [inf_of_le_left h] using Subring.map_comap_eq f t

Premises used: inf_of_le_left, Subring.map_comap_eq
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
t : Subring S
⊢ t ≤ f.range

Tactic:
simp [hf]
-- 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
a : comap f (map f s) ≤ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
a₁ : s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ≤ comap f (map f s)
⊢ comap f (map f s) = s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
x : R
hx : x ∈ comap f (map f s)
⊢ ∃ x_1 ∈ s, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)

Tactic:
rw [mem_comap, mem_map] at hx

Premises used: Subring.mem_map, Subring.mem_comap
-- 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
x : R
hx : ∃ x_1 ∈ s, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)
a :
  ∀ (y : R) (hy : y ∈ s) (hxy : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)),
    x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
⊢ x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})

Tactic:
obtain ⟨y, hy, hxy⟩ := hx
-- 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
x y : R
hy : y ∈ s
hxy : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)
⊢ Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)

Tactic:
simp [hxy]
-- 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
x y : R
hy : y ∈ s
hxy : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)
⊢ Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)

Tactic:
replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
-- 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
x y : R
hy : y ∈ s
hxy : Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)
a :
  Membership.mem (γ := Subring R) (closure ((↑s : Set R) ∪ Set.preimage (β := S) (⇑f : (a : R) → S) {0})) (y + (x - y))
⊢ x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})

Tactic:
rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]

Premises used: Subring.closure_union, Subring.closure_eq, add_sub_cancel
-- 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
x y : R
hy : y ∈ s
hxy : Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)
⊢ Membership.mem (γ := Subring R) (closure ((↑s : Set R) ∪ Set.preimage (β := S) (⇑f : (a : R) → S) {0})) (y + (x - y))

Tactic:
Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)

Premises used: Subring.add_mem, Set.Mem, Subring.subset_closure, Or.inl, Or.inr
-- 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
x y : R
hy : y ∈ s
hxy : Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)
⊢ Membership.mem (γ := Subring R) (closure ((↑s : Set R) ∪ Set.preimage (β := S) (⇑f : (a : R) → S) {0})) (y + (x - y))

Tactic:
exact Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)
-- 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
a :
  map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) ≤
    map f s
⊢ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ≤ comap f (map f s)

Tactic:
rw [← map_le_iff_le_comap, map_sup, f.map_closure]

Premises used: Subring.map_le_iff_le_comap, Subring.map_sup, RingHom.map_closure
-- 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
a :
  map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) =
    map f s
⊢ map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) ≤
    map f s

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- 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
a : Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ⊆ (↑(map f s) : Set S)
⊢ map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) =
    map f s

Tactic:
rw [sup_eq_left, closure_le]

Premises used: sup_eq_left, Subring.closure_le
-- 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
⊢ Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ⊆ (↑(map f s) : Set S)

Tactic:
(Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)

Premises used: Iff.mpr, Set.singleton_subset_iff, Subring.zero_mem, Subring.map, HasSubset.Subset.trans, Set.image_preimage_subset, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- 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
⊢ Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ⊆ (↑(map f s) : Set S)

Tactic:
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)

Premises used: Iff.mpr, Set.singleton_subset_iff, Subring.zero_mem, Subring.map, HasSubset.Subset.trans, Set.image_preimage_subset, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- 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
h : Set.preimage (β := S) (⇑f : (a : R) → S) {0} ⊆ (↑s : Set R)
⊢ comap f (map f s) = s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})

Tactic:
comap_map_eq f s

Premises used: Subring.comap_map_eq
-- 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
h : Set.preimage (β := S) (⇑f : (a : R) → S) {0} ⊆ (↑s : Set R)
h₁ : closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ≤ s
h₂ h₃ h₄ h₅ : Set.preimage (β := S) (⇑f : (a : R) → S) {0} ⊆ (↑s : Set R)
⊢ s = s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})

Tactic:
rwa [left_eq_sup, closure_le]

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

Tactic:
SetLike.coe_injective (Set.preimage_image_eq _ hf)

Premises used: SetLike.coe_injective, Set.preimage_image_eq
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ k • g ∈ G

Tactic:
AddSubgroup.zsmul_mem G h k

Premises used: AddSubgroup.zsmul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
h₁ : (↑k : R) * g = k • g
⊢ (↑k : R) * g ∈ G

Tactic:
convert! AddSubgroup.zsmul_mem G h k using 1

Premises used: AddSubgroup.zsmul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
h₁ h₂ : (↑k : R) * g = (↑k : R) * g
⊢ (↑k : R) * g = k • g

Tactic:
rw [zsmul_eq_mul]

Premises used: zsmul_eq_mul
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
S : Type u_1
R : Type u
inst_1 : SetLike S R
inst_2 : NonAssocRing R
h : SubringClass S R
⊢ AddSubgroupClass S R

Tactic:
{ h with }

Premises used: AddSubgroupClass.mk
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : SetLike S R
hSR : SubringClass S R
s : S
n : ℤ
⊢ (↑n : R) ∈ s

Tactic:
simp only [← zsmul_one, zsmul_mem, one_mem]

Premises used: zsmul_mem, zsmul_one, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : SetLike S R_1
hSR : SubringClass S R_1
s : S
R : Type u_1
inst_2 : Ring R
inst_3 : IsDomain R
inst_4 : SetLike S R
inst_5 : SubringClass S R
⊢ IsDomain.{u_1} ↥s

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : SetLike S R
hSR : SubringClass S R
s : S
x : ↥s
⊢ (subtype s : (a : ↥s) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : SetLike S R
hSR : SubringClass S R
s : S
⊢ Function.Injective (α := ↥s) (β := R) (⇑(subtype s) : (a : ↥s) → R)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : SetLike S R
hSR : SubringClass 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.Subring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : SetLike S R
hSR : SubringClass S R
s : S
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(↑n : ↥s) : R) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : SetLike S R
hSR : SubringClass S R
s : S
n : ℤ
⊢ Eq.{u + 1} (α := R) (↑(↑n : ↥s) : R) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
x t : Subring R
s : Subsemiring R
hs : ∀ {x : R}, x ∈ s.carrier → -x ∈ s.carrier
⊢ { toSubsemiring := s, neg_mem' := @hs : Subring R }.toSubsemiring = t.toSubsemiring →
    { toSubsemiring := s, neg_mem' := @hs : Subring R } = t

Tactic:
congr!
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s t : Subring R
⊢ s.toSubsemiring = t.toSubsemiring ↔ s = t

Tactic:
toSubsemiring_injective.eq_iff

Premises used: Subring.toSubsemiring_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
⊢ Function.Injective.{u + 1, u + 1} (α := Subring R) toAddSubgroup

Tactic:
fun _ _ h ↦ SetLike.ext (SetLike.ext_iff.mp h :)

Premises used: SetLike.ext_iff, SetLike.ext, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
⊢ Function.Injective (β := Submonoid R) fun (s : Subring R) ↦ s.toSubmonoid

Tactic:
fun _ _ h ↦ SetLike.ext (SetLike.ext_iff.mp h :)

Premises used: SetLike.ext_iff, SetLike.ext, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : R
⊢ x ∈ s.toSubsemiring ↔ x ∈ s

Tactic:
Iff.rfl

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

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S : Subsemiring R
x : R
h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier
⊢ x ∈ { toSubsemiring := S, neg_mem' := @h : Subring R } ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S : Subsemiring R
h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier
⊢ (↑{ toSubsemiring := S, neg_mem' := @h : Subring R } : Set R) = (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S S' : Subsemiring R
h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier
h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier
⊢ { toSubsemiring := S, neg_mem' := @h₁ : Subring R } ≤ { toSubsemiring := S', neg_mem' := @h₂ } ↔ S ≤ S'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S : Subring R
⊢ 1 ∈ S.toNonUnitalSubring

Tactic:
S.one_mem

Premises used: Subring.toSubsemiring, Set.Mem, Subsemiring.one_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S T : Subring R
h : ∀ (x : R), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S : Subring 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.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
sm : Submonoid R
hm : (↑sm : Set R) = s
sa : AddSubgroup R
ha : (↑sa : Set R) = s
x : R
⊢ x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s

Tactic:
Iff.rfl

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

Tactic:
SetLike.coe_injective hm.symm

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

Tactic:
SetLike.coe_injective ha.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x : R
h : x ∈ s.carrier
rw : -1 * x ∈ s.carrier
⊢ -x ∈ s.carrier

Tactic:
rw [← neg_one_mul]

Premises used: neg_one_mul
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x : R
h : x ∈ s.carrier
⊢ -1 * x ∈ s.carrier

Tactic:
mul_mem hneg h

Premises used: Set.Mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x : R
h : x ∈ s.carrier
⊢ -1 * x ∈ s.carrier

Tactic:
exact mul_mem hneg h

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
⊢ 1 ∈ s

Tactic:
one_mem _

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

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
mul_mem

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

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : R
⊢ x ∈ s → -x ∈ s

Tactic:
neg_mem

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x y : R
hx : x ∈ s
hy : y ∈ s
⊢ x - y ∈ s

Tactic:
sub_mem hx hy

Premises used: sub_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : R
hx : x ∈ s
n : ℤ
⊢ n • x ∈ s

Tactic:
zsmul_mem hx n

Premises used: zsmul_mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u_1
inst : Ring R
s : Subring R
x : R
hx : x ∈ s
n : ℕ
⊢ x ^ n ∈ s

Tactic:
pow_mem hx n

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
SubmonoidClass.coe_pow x n

Premises used: SubmonoidClass.coe_pow
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : ↥s
⊢ (↑x : R) = 0 ↔ x = 0

Tactic:
⟨fun h => Subtype.ext (Trans.trans h s.coe_zero.symm), fun h => h.symm ▸ s.coe_zero⟩

Premises used: Trans.trans, Eq.rec, Subring.coe_zero, Iff.intro, Eq.symm, Subtype.ext
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : R
hx : x ∈ s
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ s) x hx = 0 ↔ x = 0

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
s_1 : Subring R_1
R : Type u_1
inst_1 : NonAssocRing R
inst_2 : Nontrivial R
s : Subring R
⊢ Nontrivial.{u_1} ↥s

Tactic:
s.toSubsemiring.nontrivial

Premises used: Subring.toSubsemiring, Subsemiring.nontrivial, Set.Mem
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
s_1 : Subring R_1
R : Type u_1
inst_1 : NonAssocRing R
inst_2 : NoZeroDivisors R
s : Subring R
⊢ NoZeroDivisors.{u_1} ↥s

Tactic:
s.toSubsemiring.noZeroDivisors

Premises used: Subring.toSubsemiring, Set.Mem, Subsemiring.noZeroDivisors
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
s_1 : Subring R_1
R : Type u_1
inst_1 : Ring R
inst_2 : IsDomain R
s : Subring R
⊢ IsDomain.{u_1} ↥s

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : ↥s
⊢ (s.subtype : (a : ↥s) → R) x = (↑x : R)

Tactic:
rfl

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

Tactic:
s.toSubmonoid.subtype_injective

Premises used: Subring.toSubsemiring, Set.Mem, Subsemiring.toSubmonoid, Submonoid.subtype_injective
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring 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.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(↑n : ↥s) : R) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
n : ℤ
⊢ Eq.{u + 1} (α := R) (↑(↑n : ↥s) : R) (↑n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
⊢ (↑s.toSubsemiring : Set R) = (↑s : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : R
⊢ x ∈ s.toSubmonoid ↔ x ∈ s

Tactic:
Iff.rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
x : R
⊢ x ∈ s.toAddSubgroup ↔ x ∈ s

Tactic:
Iff.rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S : Subring R
mk :
  ∀ (toSubsemiring : Subsemiring R) (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier),
    { toSubsemiring := toSubsemiring, neg_mem' := @neg_mem' : Subring R }.toNonUnitalSubring.toSubring ⋯ =
      { toSubsemiring := toSubsemiring, neg_mem' := @neg_mem' }
⊢ S.toNonUnitalSubring.toSubring ⋯ = S

Tactic:
cases S
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
toSubsemiring : Subsemiring R
neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier
⊢ { toSubsemiring := toSubsemiring, neg_mem' := @neg_mem' : Subring R }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring, neg_mem' := @neg_mem' }

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
S : NonUnitalSubring R
h1 : 1 ∈ S
mk :
  ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
    (neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier)
    (h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R }),
    ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R }.toSubring
          h1).toNonUnitalSubring =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' }
⊢ (S.toSubring h1).toNonUnitalSubring = S

Tactic:
cases S
-- Module: Mathlib.Algebra.Ring.Subring.Defs
Goal:
R : Type u
inst : NonAssocRing R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R }.toSubring
        h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' }

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
rw : n ∈ P.support ↔ ¬Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ = 0
rw₁ : n ∈ P.support ↔ ¬(↑(Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯) : K) = 0
rw₂ rw₃ : P.coeff n ≠ 0 ↔ ¬(↑(Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯) : K) = 0
⊢ n ∈ P.support ↔ Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ ≠ 0

Tactic:
rw [ne_eq, ← Subring.coe_eq_zero_iff, mem_support_iff]

Premises used: Polynomial.mem_support_iff, ne_eq, Subring.coe_eq_zero_iff
-- Module: Mathlib.Algebra.Ring.Subring.IntPolynomial
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
⊢ (↑((int R P hP).coeff n) : K) = P.coeff n

Tactic:
rfl

Premises used: Polynomial.coeff, rfl