awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : R
⊢ x ∈ s.toAddSubgroup ↔ 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.toAddSubgroup : Set R) = (↑s : Set R)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ StrictMono.{u, u} (α := NonUnitalSubsemiring R) toSubsemigroup

Tactic:
fun _ _ => id

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

Tactic:
toSubsemigroup_strictMono.monotone

Premises used: StrictMono.monotone, NonUnitalSubsemiring.toSubsemigroup_strictMono
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ StrictMono.{u, u} (α := NonUnitalSubsemiring R) toAddSubmonoid

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ Monotone.{u, u} (α := NonUnitalSubsemiring R) toAddSubmonoid

Tactic:
toAddSubmonoid_strictMono.monotone

Premises used: StrictMono.monotone, NonUnitalSubsemiring.toAddSubmonoid_strictMono
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring S
f : F
⊢ (↑(comap f s) : Set R) = (⇑f : (a : R) → S) ⁻¹' (↑s : Set S)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring S
f : F
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (comap f s) x ↔ Membership.mem (α := S) s ((f : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst_3 : FunLike F R S
inst_4 : NonUnitalRingHomClass F R S
inst_5 : FunLike G S T
inst_6 : NonUnitalRingHomClass G S T
s : NonUnitalSubsemiring T
g : G
f : F
⊢ Eq (α := NonUnitalSubsemiring R) (comap f (comap g s))
    (comap (F := R →ₙ+* T) (NonUnitalRingHom.comp (↑g : S →ₙ+* T) (↑f : R →ₙ+* S)) s)

Tactic:
rfl

Premises used: Set.Mem, NonUnitalSubsemiring.comap, setOf, Set.preimage, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : NonUnitalSubsemiring R
⊢ (↑(map f s) : Set S) = (⇑f : (a : R) → S) '' (↑s : Set R)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : NonUnitalSubsemiring R
y : S
⊢ Membership.mem (γ := NonUnitalSubsemiring S) (map f s) y ↔ ∃ x ∈ s, (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
⊢ map (F := R →ₙ+* R) (NonUnitalRingHom.id R) s = s

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst_3 : FunLike F R S
inst_4 : NonUnitalRingHomClass F R S
inst_5 : FunLike G S T
inst_6 : NonUnitalRingHomClass G S T
s : NonUnitalSubsemiring R
g : G
f : F
⊢ Eq (α := NonUnitalSubsemiring T) (map (F := S →ₙ+* T) (↑g : S →ₙ+* T) (map (F := R →ₙ+* S) (↑f : R →ₙ+* S) s))
    (map (F := R →ₙ+* T) (NonUnitalRingHom.comp (↑g : S →ₙ+* T) (↑f : R →ₙ+* S)) s)

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

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
s : NonUnitalSubsemiring R
t : NonUnitalSubsemiring 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.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ GaloisConnection (α := NonUnitalSubsemiring R) (β := NonUnitalSubsemiring S) (map f) (comap f)

Tactic:
fun _ _ => map_le_iff_le_comap

Premises used: NonUnitalSubsemiring.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s : NonUnitalSubsemiring R
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : ↥s
⊢ Eq.{v + 1} (α := S)
    ((↑(((s.equivMapOfInjective f hf : RingEquiv.{u, v} ↥s ↥(map f s)) : (a : ↥s) → ↥(map f s)) x) : S) : S)
    ((f : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ (↑(srange f) : Set S) = Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
y : S
⊢ Membership.mem (γ := NonUnitalSubsemiring S) (srange f) y ↔ ∃ (x : R), (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
h :
  ∀ (x : S),
    Membership.mem (γ := NonUnitalSubsemiring S) (srange f) x ↔ Membership.mem (γ := NonUnitalSubsemiring S) (map f ⊤) x
⊢ Eq (α := NonUnitalSubsemiring S) (srange f) (map f ⊤)

Tactic:
ext
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : S
⊢ Membership.mem (γ := NonUnitalSubsemiring S) (srange f) x ↔ Membership.mem (γ := NonUnitalSubsemiring S) (map f ⊤) x

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
⊢ Membership.mem (α := S) (γ := NonUnitalSubsemiring S) (srange f) ((f : (a : R) → S) x : S)

Tactic:
mem_srange.mpr ⟨x, rfl⟩

Premises used: Iff.mpr, NonUnitalRingHom.mem_srange, Exists.intro, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ Eq (α := NonUnitalSubsemiring T) (map g (srange f)) (srange (g.comp f))

Tactic:
simpa only [srange_eq_map] using (⊤ : NonUnitalSubsemiring R).map_map g f

Premises used: NonUnitalRingHom.srange_eq_map, NonUnitalSubsemiring.map_map, Top.top
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
F : Type u_1
G : Type u_2
inst_3 : FunLike F R S
inst_4 : NonUnitalRingHomClass F R S
inst_5 : FunLike G S T
inst_6 : NonUnitalRingHomClass G S T
f_1 : F
g : G
inst_7 : Finite R
f : F
⊢ Finite.{v + 1} ↥(srange f)

Tactic:
(Set.finite_range f).to_subtype

Premises used: Set.Mem, setOf, Set.finite_range, Set.Finite.to_subtype, Set.range, DFunLike.coe
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s : Set (NonUnitalSubsemiring R)
⊢ (↑(⨅ t ∈ s, t.toSubsemigroup) : Set R) = ⋂ t ∈ s, (↑t : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s : Set (NonUnitalSubsemiring R)
⊢ (↑(⨅ t ∈ s, t.toAddSubmonoid) : Set R) = ⋂ t ∈ s, (↑t : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
⊢ (↑(sInf S) : Set R) = ⋂ s ∈ S, (↑s : Set R)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
x : R
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
⊢ (↑(⨅ (i : ι), S i) : Set R) = ⋂ (i : ι), (↑(S i) : Set R)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, Set.biInter_range, NonUnitalSubsemiring.coe_sInf
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨅ (i : ι), S i) x ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Premises used: iInf, Set.forall_mem_range, NonUnitalSubsemiring.mem_sInf
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set (NonUnitalSubsemiring R)
⊢ (sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup

Tactic:
mk'_toSubsemigroup _ _

Premises used: NonUnitalSubsemiring.mk'_toSubsemigroup
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set (NonUnitalSubsemiring R)
⊢ (sInf s).toAddSubmonoid = ⨅ t ∈ s, t.toAddSubmonoid

Tactic:
mk'_toAddSubmonoid _ _

Premises used: NonUnitalSubsemiring.mk'_toAddSubmonoid
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
A : NonUnitalSubsemiring R
⊢ A = ⊤ ↔ ∀ (x : R), x ∈ A

Tactic:
eq_top_iff.trans ⟨fun h m => h <| mem_top m, fun h m _ => h m⟩

Premises used: eq_top_iff, NonUnitalSubsemiring.mem_top, Iff.intro, Iff.trans
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ (↑(center R) : Set R) = Set.center R

Tactic:
rfl

Premises used: setOf, Set.center, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ Eq (α := Subsemigroup R) (toSubsemigroup (center R)) (Subsemigroup.center R)

Tactic:
rfl

Premises used: setOf, Set.center, Subsemigroup.center, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
a : R
rw :
  ((∀ (a_1 : R), Commute a a_1) ∧ (∀ (b c : R), a * (b * c) = a * b * c) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔
    Eq (α := R →+ R) (AddMonoidHom.mulLeft a) (AddMonoidHom.mulRight a) ∧
      Eq (α := R →+ R →+ R) (AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulLeft a))
          (AddMonoidHom.comp AddMonoidHom.mul (AddMonoidHom.mulLeft a)) ∧
        Eq (α := R →+ R →+ R) (AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulRight a))
          (AddMonoidHom.compl₂ AddMonoidHom.mul (AddMonoidHom.mulRight a))
⊢ a ∈ Set.center R ↔
    Eq (α := R →+ R) (AddMonoidHom.mulLeft a) (AddMonoidHom.mulRight a) ∧
      Eq (α := R →+ R →+ R) (AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulLeft a))
          (AddMonoidHom.comp AddMonoidHom.mul (AddMonoidHom.mulLeft a)) ∧
        Eq (α := R →+ R →+ R) (AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulRight a))
          (AddMonoidHom.compl₂ AddMonoidHom.mul (AddMonoidHom.mulRight a))

Tactic:
rw [Set.mem_center_iff, isMulCentral_iff]

Premises used: isMulCentral_iff, Set.mem_center_iff
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
a : R
⊢ ((∀ (a_1 : R), Commute a a_1) ∧ (∀ (b c : R), a * (b * c) = a * b * c) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔
    Eq (α := R →+ R) (AddMonoidHom.mulLeft a) (AddMonoidHom.mulRight a) ∧
      Eq (α := R →+ R →+ R) (AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulLeft a))
          (AddMonoidHom.comp AddMonoidHom.mul (AddMonoidHom.mulLeft a)) ∧
        Eq (α := R →+ R →+ R) (AddMonoidHom.compr₂ AddMonoidHom.mul (AddMonoidHom.mulRight a))
          (AddMonoidHom.compl₂ AddMonoidHom.mul (AddMonoidHom.mulRight a))

Tactic:
simp [DFunLike.ext_iff, commute_iff_eq]

Premises used: commute_iff_eq, DFunLike.ext_iff
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
x x_1 : ↥(center R)
⊢ (↑(Equiv.toFun (MulEquiv.toEquiv (Subsemigroup.centerCongr (↑e : R ≃* S))) (x + x_1)) : S) =
    (↑(HAdd.hAdd (α := ↥(center S)) (Equiv.toFun (MulEquiv.toEquiv (Subsemigroup.centerCongr (↑e : R ≃* S))) x)
          (Equiv.toFun (MulEquiv.toEquiv (Subsemigroup.centerCongr (↑e : R ≃* S))) x_1)) :
      S)

Tactic:
map_add e ..

Premises used: map_add
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst_1 : NonUnitalNonAssocSemiring S
e : R ≃+* S
x x_1 : ↥(center R)
⊢ (↑(Equiv.toFun (MulEquiv.toEquiv (Subsemigroup.centerCongr (↑e : R ≃* S))) (x + x_1)) : S) =
    (↑(HAdd.hAdd (α := ↥(center S)) (Equiv.toFun (MulEquiv.toEquiv (Subsemigroup.centerCongr (↑e : R ≃* S))) x)
          (Equiv.toFun (MulEquiv.toEquiv (Subsemigroup.centerCongr (↑e : R ≃* S))) x_1)) :
      S)

Tactic:
exact map_add e ..

Premises used: map_add
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
M : Subsemigroup R_1
R : Type u_1
inst_1 : NonUnitalSemiring R
⊢ Eq (α := NonUnitalSemiring ↥(center R)) NonUnitalCommSemiring.toNonUnitalSemiring
    (NonUnitalSubsemiringClass.toNonUnitalSemiring (center R))

Tactic:
rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
M : Subsemigroup R_1
R : Type u_1
inst_1 : NonUnitalSemiring R
⊢ Eq (α := NonUnitalSemiring ↥(center R)) NonUnitalCommSemiring.toNonUnitalSemiring
    (NonUnitalSubsemiringClass.toNonUnitalSemiring (center R))

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
z : R
rw : Membership.mem (γ := NonUnitalSubsemiring R) (center R) z ↔ z ∈ Set.center R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (center R) z ↔ ∀ (g : R), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
z : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (center R) z ↔ z ∈ Set.center R

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.center
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
z : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (center R) z ↔ z ∈ Set.center R

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalCommSemiring R
⊢ Eq (α := NonUnitalSubsemiring R) (center R) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ R)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
⊢ (↑(centralizer s) : Set R) = s.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
⊢ Eq (α := Subsemigroup R) (toSubsemigroup (centralizer s)) (Subsemigroup.centralizer s)

Tactic:
rfl

Premises used: setOf, Subsemigroup.centralizer, Set.centralizer, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
z : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (centralizer s) z ↔ ∀ g ∈ s, g * z = z * g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
⊢ LE.le (α := NonUnitalSubsemiring R) (center R) (centralizer s)

Tactic:
s.center_subset_centralizer

Premises used: Set.Mem, setOf, Set.center, Set.centralizer, Set.Subset, Set.center_subset_centralizer
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s t : Set R
h : s ⊆ t
⊢ LE.le (α := NonUnitalSubsemiring R) (centralizer t) (centralizer s)

Tactic:
Set.centralizer_subset h

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
⊢ Eq (α := NonUnitalSubsemiring R) (centralizer s) ⊤ ↔ s ⊆ (↑(center R) : Set R)

Tactic:
SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Premises used: Set.centralizer_eq_top_iff_subset, SetLike.ext'_iff, Iff.trans
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
⊢ Eq (α := NonUnitalSubsemiring R) (centralizer Set.univ) (center R)

Tactic:
SetLike.ext' (Set.centralizer_univ R)

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
x : R
s : Set R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x ↔ ∀ (S : NonUnitalSubsemiring R), s ⊆ (↑S : Set R) → x ∈ S

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, NonUnitalSubsemiring.mem_sInf
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
⊢ s ⊆ (↑(closure s) : Set R)

Tactic:
fun _ hx => mem_closure.2 fun _ hS => hS hx

Premises used: Iff.mpr, Set.Subset, NonUnitalSubsemiring.mem_closure
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ s
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x

Tactic:
subset_closure hx

Premises used: NonUnitalSubsemiring.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
P : R
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: NonUnitalSubsemiring.subset_closure, Not
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
t : NonUnitalSubsemiring R
⊢ closure s ≤ t ↔ s ⊆ (↑t : Set R)

Tactic:
⟨Set.Subset.trans subset_closure, fun h => sInf_le h⟩

Premises used: NonUnitalSubsemiring.subset_closure, Set.Subset.trans, sInf_le, Iff.intro
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s t : Set R
h : s ⊆ t
⊢ LE.le (α := NonUnitalSubsemiring R) (closure s) (closure t)

Tactic:
closure_le.2 <| Set.Subset.trans h subset_closure

Premises used: Iff.mpr, NonUnitalSubsemiring.subset_closure, Set.Subset.trans, NonUnitalSubsemiring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
t : NonUnitalSubsemiring R
h₁ : s ⊆ (↑t : Set R)
h₂ : t ≤ closure s
⊢ closure s = t

Tactic:
le_antisymm (closure_le.2 h₁) h₂

Premises used: Iff.mpr, le_antisymm, NonUnitalSubsemiring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
⊢ LE.le (α := NonUnitalSubsemiring R) (closure s) (centralizer (↑(centralizer s) : Set R))

Tactic:
closure_le.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Set.subset_centralizer_centralizer, NonUnitalSubsemiring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
⊢ IsMulCommutative.{u_1} ↥(closure s)

Tactic:
have := closure_le_centralizer_centralizer s
  .of_setLike_mul_comm fun _ h₁ _ h₂ ↦
    Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂)

Premises used: NonUnitalSubsemiring.closure_le_centralizer_centralizer, IsMulCommutative.of_setLike_mul_comm, Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
M : Subsemigroup R_1
S : Type u_1
R : Type u_2
inst_1 : NonUnitalSemiring R
inst_2 : SetLike S R
inst_3 : MulMemClass S R
s : S
inst_4 : IsMulCommutative.{u_2} ↥s
⊢ IsMulCommutative.{u_2} ↥(closure (↑s : Set R))

Tactic:
isMulCommutative_closure fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂

Premises used: setLike_mul_comm, NonUnitalSubsemiring.isMulCommutative_closure
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring R
x : S
⊢ Membership.mem (γ := Set S) ((⇑f.toEquiv : (a : R) → S) '' (↑K : Set R)) x ↔
    Membership.mem (α := R) (↑K : Set R) ((f.symm : (a : S) → R) x : R)

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

Premises used: Set.mem_image_equiv
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring R
x : S
⊢ Membership.mem (γ := NonUnitalSubsemiring S) (map (F := R →ₙ+* S) (↑f : R →ₙ+* S) K) x ↔
    Membership.mem (α := R) K ((f.symm : (a : S) → R) x : R)

Tactic:
convert! @Set.mem_image_equiv _ _ (↑K) f.toEquiv x

Premises used: Set.mem_image_equiv
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring R
⊢ Eq (α := NonUnitalSubsemiring 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