awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
this : Nonempty.{u + 1} (↑S : Type u)
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists,
    exists_prop]

Premises used: NonUnitalSubring.mem_iSup_of_directed, SetCoe.exists, exists_prop, DirectedOn.directed_val, sSup_eq_iSup'
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
⊢ x ∈ (↑(sSup S) : Set R) ↔ Membership.mem (γ := Set R) (⋃ s ∈ S, (↑s : Set R)) x

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Premises used: NonUnitalSubring.mem_sSup_of_directedOn
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
inst_1 : Nonempty ι
S : ι → NonUnitalSubring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, NonUnitalSubsemiring.coe_iSup_of_directed dir,
    coe_iSup_of_directed dir] using NonUnitalSubsemiring.isMulCommutative_iSup dir

Premises used: NonUnitalSubsemiring.isMulCommutative_iSup, NonUnitalSubsemiring.coe_iSup_of_directed, SetLike.mem_coe, NonUnitalSubring.coe_iSup_of_directed, isMulCommutative_iff
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S_1 : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S_1
inst_2 : FunLike F R S_1
inst_3 : NonUnitalRingHomClass F R S_1
ι : Type u_1
inst_4 : Nonempty ι
inst_5 : Preorder ι
inst_6 : IsDirectedOrder ι
S : OrderHom.{u_1, u} ι (NonUnitalSubring R)
hS : ∀ (i : ι), IsMulCommutative.{u} ↥((S : (a : ι) → NonUnitalSubring R) i : NonUnitalSubring R)
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), (S : (a : ι) → NonUnitalSubring R) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, NonUnitalSubring.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R ≃+* S
K : NonUnitalSubring R
x : S
⊢ Membership.mem (γ := NonUnitalSubring S) (map (F := R →ₙ+* S) (↑f : R →ₙ+* S) K) x ↔
    Membership.mem (α := R) K ((f.symm : (a : S) → R) x : R)

Tactic:
@Set.mem_image_equiv _ _ (K : Set R) f.toEquiv x

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R ≃+* S
K : NonUnitalSubring R
⊢ Eq (α := NonUnitalSubring S) (map (F := R →ₙ+* S) (↑f : R →ₙ+* S) K) (comap f.symm K)

Tactic:
SetLike.coe_injective (f.toEquiv.image_eq_preimage_symm K)

Premises used: RingEquiv.toEquiv, SetLike.coe_injective, Equiv.image_eq_preimage_symm, SetLike.coe
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R ≃+* S
K : NonUnitalSubring S
⊢ Eq (α := NonUnitalSubring R) (comap (F := R →ₙ+* S) (↑f : R →ₙ+* S) K) (map f.symm K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: NonUnitalSubring.map_equiv_eq_comap_symm, NonUnitalSubring.comap, NonUnitalSubring.map, NonUnitalRingHomClass.toNonUnitalRingHom, Eq.symm, RingEquiv.symm
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
x : R
⊢ Eq.{v + 1} (α := S) ((↑((f.rangeRestrict : (a : R) → ↥f.range) x) : S) : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ Function.Surjective.{u + 1, v + 1} (α := R) (β := ↥f.range) (⇑f.rangeRestrict : (a : R) → ↥f.range)

Tactic:
fun ⟨_y, hy⟩ =>
  let ⟨x, hx⟩ := mem_range.mp hy
  ⟨x, Subtype.ext hx⟩

Premises used: NonUnitalRingHom.mem_range, _private.0.NonUnitalRingHom.rangeRestrict_surjective.match_1, Exists, _private.0.NonUnitalRingHom.rangeRestrict_surjective.match_2, Subtype.mk, Exists.intro, Iff.mp, Eq, DFunLike.coe, Function.Surjective, NonUnitalRingHom.rangeRestrict, Subtype.ext
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
rw :
  Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
rw₁ rw₂ :
  Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
⊢ (↑f.range : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ

Tactic:
rw [coe_range, coe_top]

Premises used: NonUnitalSubring.coe_top, NonUnitalRingHom.coe_range
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.range = ⊤

Tactic:
range_eq_top.2 hf

Premises used: Iff.mpr, NonUnitalRingHom.range_eq_top
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f g : R →ₙ+* S
x : R
⊢ x ∈ f.eqLocus 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.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ f.eqLocus f = ⊤

Tactic:
SetLike.ext fun _ => eq_self_iff_true _

Premises used: SetLike.ext, DFunLike.coe, eq_self_iff_true
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f g : R →ₙ+* S
s : Set R
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) s
⊢ Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) (↑(closure s) : Set R)

Tactic:
show closure s ≤ f.eqLocus g from closure_le.2 h

Premises used: Iff.mpr, Set.Mem, setOf, Set.EqOn, NonUnitalSubring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f g : R →ₙ+* S
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) (↑⊤ : Set R)
⊢ f = g

Tactic:
ext fun _x => h trivial

Premises used: trivial, NonUnitalRingHom.ext
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s : Set R
hs : Eq (α := NonUnitalSubring R) (closure s) ⊤
f g : R →ₙ+* S
h : Set.EqOn.{u, v} (β := S) (⇑f : (a : R) → S) (⇑g : (a : R) → S) s
⊢ f = g

Tactic:
eq_of_eqOn_set_top <| hs ▸ eqOn_set_closure h

Premises used: NonUnitalRingHom.eqOn_set_closure, Eq.rec, NonUnitalRingHom.eq_of_eqOn_set_top
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
s : Set S
⊢ LE.le (α := NonUnitalSubring R) (closure ((⇑f : (a : R) → S) ⁻¹' s)) (comap f (closure s))

Tactic:
closure_le.2 fun _x hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Premises used: Iff.mpr, NonUnitalSubring.mem_comap, SetLike.mem_coe, NonUnitalSubring.subset_closure, NonUnitalSubring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
s : Set R
⊢ Eq (α := NonUnitalSubring S) (map f (closure s)) (closure ((⇑f : (a : R) → S) '' s))

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (NonUnitalSubring.gi S).gc
    (NonUnitalSubring.gi R).gc fun _ ↦ rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Set.image_preimage, NonUnitalSubring.gi, NonUnitalSubring.gc_map_comap, rfl, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
⊢ range (R := ↥s) (NonUnitalSubringClass.subtype s) = s

Tactic:
SetLike.coe_injective <| (coe_srange _).trans Subtype.range_coe

Premises used: SetLike.coe_injective, Subtype.range_coe, NonUnitalRingHom.coe_srange, Eq.trans
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
⊢ Eq (α := NonUnitalSubsemiring R) (srange (F := R × S →ₙ+* R) (fst R S)) ⊤

Tactic:
NonUnitalSubsemiring.range_fst

Premises used: NonUnitalSubsemiring.range_fst
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
⊢ Eq (α := NonUnitalSubsemiring S) (srange (F := R × S →ₙ+* S) (snd R S)) ⊤

Tactic:
NonUnitalSubsemiring.range_snd

Premises used: NonUnitalSubsemiring.range_snd
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalRing R
inst_1 : NonUnitalRing S
s t : NonUnitalSubring R
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.range
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g ((f : (a : R) → S) x')) : S) ((f : (a : R) → S) x' : S)
rw₁ rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x' : S)
⊢ (f : (a : R) → S) (g (↑x : S)) = (↑x : S)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalRing R
inst_1 : NonUnitalRing S
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S) ((↑((ofLeftInverse' h : (a : R) → ↥f.range) x) : S) : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalRing R
inst_1 : NonUnitalRing S
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.range
⊢ ((ofLeftInverse' h).symm : (a : ↥f.range) → R) x = g (↑x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : Set S
⊢ LE.le (α := NonUnitalSubring R) (closure ((⇑f : (a : R) → S) ⁻¹' s)) (comap f (closure s))

Tactic:
closure_le.2 fun _x hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Premises used: Iff.mpr, NonUnitalSubring.mem_comap, SetLike.mem_coe, NonUnitalSubring.subset_closure, NonUnitalSubring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R_1 : Type u
S_1 : Type v
inst : NonUnitalNonAssocRing R_1
S : Type u_1
R : Type u
inst_1 : SetLike S R
inst_2 : NonUnitalNonAssocRing R
h : NonUnitalSubringClass S R
⊢ AddSubgroupClass S R

Tactic:
{ h with }

Premises used: AddSubgroupClass.mk
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
x : ↥s
⊢ (subtype s : (a : ↥s) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ Function.Injective (α := ↥s) (β := R) (⇑(subtype s) : (a : ↥s) → R)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : SetLike S R
hSR : NonUnitalSubringClass 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.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
p q : NonUnitalSubring R
h :
  Eq.{u + 1} (α := Set R) ((fun (s : NonUnitalSubring R) ↦ s.carrier) p) ((fun (s : NonUnitalSubring R) ↦ s.carrier) q)
mk :
  ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
    (neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier)
    (h :
      Eq.{u + 1} (α := Set R)
        ((fun (s : NonUnitalSubring R) ↦ s.carrier)
          { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' })
        ((fun (s : NonUnitalSubring R) ↦ s.carrier) q)),
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
q : NonUnitalSubring R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' })
    ((fun (s : NonUnitalSubring R) ↦ s.carrier) q)
mk :
  ∀ (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R)
    (neg_mem'_1 : ∀ {x : R}, x ∈ toNonUnitalSubsemiring_1.carrier → -x ∈ toNonUnitalSubsemiring_1.carrier)
    (h :
      Eq.{u + 1} (α := Set R)
        ((fun (s : NonUnitalSubring R) ↦ s.carrier)
          { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' })
        ((fun (s : NonUnitalSubring R) ↦ s.carrier)
          { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := @neg_mem'_1 })),
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := @neg_mem'_1 }
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R } = q

Tactic:
cases q
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
neg_mem'_1 : ∀ {x : R}, x ∈ toNonUnitalSubsemiring_1.carrier → -x ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' })
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := @neg_mem'_1 })
mk : toNonUnitalSubsemiring = toNonUnitalSubsemiring_1
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := @neg_mem'_1 }

Tactic:
congr
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
neg_mem'_1 : ∀ {x : R}, x ∈ toNonUnitalSubsemiring_1.carrier → -x ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' })
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := @neg_mem'_1 })
⊢ toNonUnitalSubsemiring = toNonUnitalSubsemiring_1

Tactic:
SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
toNonUnitalSubsemiring : NonUnitalSubsemiring R
neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier
toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R
neg_mem'_1 : ∀ {x : R}, x ∈ toNonUnitalSubsemiring_1.carrier → -x ∈ toNonUnitalSubsemiring_1.carrier
h :
  Eq.{u + 1} (α := Set R)
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' })
    ((fun (s : NonUnitalSubring R) ↦ s.carrier)
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, neg_mem' := @neg_mem'_1 })
⊢ toNonUnitalSubsemiring = toNonUnitalSubsemiring_1

Tactic:
exact SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : R
⊢ x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : NonUnitalSubsemiring R
x : R
h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier
⊢ x ∈ { toNonUnitalSubsemiring := S, neg_mem' := @h : NonUnitalSubring R } ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : NonUnitalSubsemiring R
h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier
⊢ (↑{ toNonUnitalSubsemiring := S, neg_mem' := @h : NonUnitalSubring R } : Set R) = (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S S' : NonUnitalSubsemiring R
h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier
h' : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier
⊢ { toNonUnitalSubsemiring := S, neg_mem' := @h : NonUnitalSubring R } ≤
      { toNonUnitalSubsemiring := S', neg_mem' := @h' } ↔
    S ≤ S'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S T : NonUnitalSubring R
h : ∀ (x : R), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : NonUnitalSubring R
s : Set R
hs : s = (↑S : Set R)
⊢ (↑(S.copy s hs) : Set R) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : NonUnitalSubring 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.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ StrictMono.{u, u} (α := NonUnitalSubring R) toNonUnitalSubsemiring

Tactic:
fun _ _ =>
  id

Premises used: StrictMono, id
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ Monotone.{u, u} (α := NonUnitalSubring R) toNonUnitalSubsemiring

Tactic:
toNonUnitalSubsemiring_strictMono.monotone

Premises used: NonUnitalSubring.toNonUnitalSubsemiring_strictMono, StrictMono.monotone
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ StrictMono.{u, u} (α := NonUnitalSubring R) toAddSubgroup

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ Monotone.{u, u} (α := NonUnitalSubring R) toAddSubgroup

Tactic:
toAddSubgroup_strictMono.monotone

Premises used: StrictMono.monotone, NonUnitalSubring.toAddSubgroup_strictMono
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ StrictMono.{u, u} (α := NonUnitalSubring R) toSubsemigroup

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
⊢ Monotone.{u, u} (α := NonUnitalSubring R) toSubsemigroup

Tactic:
toSubsemigroup_strictMono.monotone

Premises used: StrictMono.monotone, NonUnitalSubring.toSubsemigroup_strictMono
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
sm : Subsemigroup R
hm : (↑sm : Set R) = s
sa : AddSubgroup R
ha : (↑sa : Set R) = s
⊢ (↑(NonUnitalSubring.mk' s sm sa hm ha) : Set R) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
sm : Subsemigroup R
hm : (↑sm : Set R) = s
sa : AddSubgroup R
ha : (↑sa : Set R) = s
x : R
⊢ x ∈ NonUnitalSubring.mk' s sm sa hm ha ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
sm : Subsemigroup R
hm : (↑sm : Set R) = s
sa : AddSubgroup R
ha : (↑sa : Set R) = s
⊢ (NonUnitalSubring.mk' s sm sa hm ha).toSubsemigroup = sm

Tactic:
SetLike.coe_injective hm.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
sm : Subsemigroup R
hm : (↑sm : Set R) = s
sa : AddSubgroup R
ha : (↑sa : Set R) = s
⊢ (NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa

Tactic:
SetLike.coe_injective ha.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
⊢ 0 ∈ s

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x y : R
⊢ x ∈ s → y ∈ s → x + y ∈ s

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : R
⊢ x ∈ s → -x ∈ s

Tactic:
neg_mem

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x y : R
hx : x ∈ s
hy : y ∈ s
⊢ x - y ∈ s

Tactic:
sub_mem hx hy

Premises used: sub_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : R
hx : x ∈ s
n : ℤ
⊢ n • x ∈ s

Tactic:
zsmul_mem hx n

Premises used: zsmul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x y : ↥s
⊢ (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : ↥s
⊢ (↑(-x) : R) = -(↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x y : ↥s
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
⊢ Eq.{u + 1} (α := R) (↑0 : R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : ↥s
⊢ (↑x : R) = 0 ↔ x = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : R
⊢ x ∈ s.toSubsemigroup ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
⊢ (↑s.toSubsemigroup : Set R) = (↑s : Set R)

Tactic:
rfl

Premises used: rfl