awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ Nonempty.{u + 1} (↑S : Type u)

Tactic:
haveI : Nonempty S := Sne.to_subtype
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subsemiring 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: Subsemiring.mem_iSup_of_directed, SetCoe.exists, exists_prop, DirectedOn.directed_val, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subsemiring 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: Subsemiring.mem_sSup_of_directedOn
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
inst_1 : Nonempty ι
S : ι → Subsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), S i)

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

Premises used: Subsemiring.coe_iSup_of_directed, SetLike.mem_coe, Subsemigroup.isMulCommutative_iSup, Subsemigroup.coe_iSup_of_directed, isMulCommutative_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S_1
inst_2 : NonAssocSemiring T
ι : Type u_1
inst_3 : Nonempty ι
inst_4 : Preorder ι
inst_5 : IsDirectedOrder ι
S : OrderHom.{u_1, u} ι (Subsemiring R)
hS : ∀ (i : ι), IsMulCommutative.{u} ↥((S : (a : ι) → Subsemiring R) i : Subsemiring R)
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), (S : (a : ι) → Subsemiring R) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, Subsemiring.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σS : Type u_2
inst_2 : SetLike σS S
inst_3 : SubsemiringClass σS S
f : R →+* S
s : σS
h : ∀ (x : R), Membership.mem.{v, u_2} (α := S) s ((f : (a : R) → S) x : S)
x : R
⊢ Eq.{v + 1} (α := S) ((↑(((f.codRestrict s h : RingHom.{u, v} R ↥s) : (a : R) → ↥s) x) : S) : S)
    ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σS : Type u_2
inst_2 : SetLike σS S
inst_3 : SubsemiringClass σS S
f : R →+* S
s : σS
h : ∀ (x : R), Membership.mem.{v, u_2} (α := S) s ((f : (a : R) → S) x : S)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := ↥s) (⇑(f.codRestrict s h) : (a : R) → ↥s) ↔
    Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
Set.injective_codRestrict h

Premises used: Set.injective_codRestrict, Set.codRestrict
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σS : Type u_2
inst_2 : SetLike σS S
inst_3 : SubsemiringClass σS S
f : R →+* S
s : σS
h : ∀ (x : R), Membership.mem.{v, u_2} (α := S) s ((f : (a : R) → S) x : S)
⊢ Eq (α := Subsemiring ↥s) (rangeS (f.codRestrict s h)) (comap (SubsemiringClass.subtype s) f.rangeS)

Tactic:
SetLike.coe_injective <| Set.range_codRestrict h

Premises used: SetLike.coe_injective, Set.range_codRestrict
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σS : Type u_2
inst_2 : SetLike σS S
inst_3 : SubsemiringClass σS S
f : R →+* S
s : σS
h : ∀ (x : R), Membership.mem.{v, u_2} (α := S) s ((f : (a : R) → S) x : S)
⊢ Function.Surjective.{u + 1, v + 1} (α := R) (β := ↥s) (⇑(f.codRestrict s h) : (a : R) → ↥s) ↔ f.rangeS = ofClass s

Tactic:
(Set.surjective_codRestrict h).trans <| .symm <| SetLike.coe_set_eq.symm

Premises used: Set.surjective_codRestrict, Iff.trans, SetLike.coe_set_eq, Set.codRestrict, Iff.symm
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_2 : SetLike σR R
inst_3 : SetLike σS S
inst_4 : SubsemiringClass σR R
inst_5 : SubsemiringClass σS S
f : R →+* S
s' : σR
s : σS
h : ∀ x ∈ s', Membership.mem.{v, u_2} (α := S) s ((f : (a : R) → S) x : S)
x : ↥s'
⊢ Eq.{v + 1} (α := S) ((↑(((f.restrict s' s h : RingHom.{u, v} ↥s' ↥s) : (a : ↥s') → ↥s) x) : S) : S)
    ((f : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst_2 : SetLike σR R
inst_3 : SetLike σS S
inst_4 : SubsemiringClass σR R
inst_5 : SubsemiringClass σS S
f : R →+* S
s' : σR
s : σS
h : ∀ x ∈ s', Membership.mem.{v, u_2} (α := S) s ((f : (a : R) → S) x : S)
⊢ Eq (α := RingHom.{u, v} (↥s') S)
    (@comp _ _ _ _ (SubsemiringClass.toNonAssocSemiring s) _ (SubsemiringClass.subtype s) (f.restrict s' s h))
    (f.comp (SubsemiringClass.subtype s'))

Tactic:
rfl

Premises used: SubsemiringClass.subtype, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
g : S →+* T
f : R →+* S
p : Subsemiring S
h : ∀ (c : R), Membership.mem (α := S) p ((f : (a : R) → S) c : S)
⊢ @comp _ _ _ _ (SubsemiringClass.toNonAssocSemiring p) _ (g.domRestrict p) (f.codRestrict p h) = g.comp f

Tactic:
rfl

Premises used: RingHom.domRestrict, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
x : R
⊢ Eq.{v + 1} (α := S) ((↑((f.rangeSRestrict : (a : R) → ↥f.rangeS) x) : S) : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
⊢ Function.Surjective.{u + 1, v + 1} (α := R) (β := ↥f.rangeS) (⇑f.rangeSRestrict : (a : R) → ↥f.rangeS)

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

Premises used: Exists, RingHom.rangeSRestrict, RingHom.mem_rangeS, Subtype.mk, _private.0.RingHom.rangeSRestrict_surjective.match_1, _private.0.RingHom.rangeSRestrict_surjective.match_2, Exists.intro, Iff.mp, Eq, DFunLike.coe, Function.Surjective, Subtype.ext
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring 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.rangeS : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ

Tactic:
rw [coe_rangeS, coe_top]

Premises used: Subsemiring.coe_top, RingHom.coe_rangeS
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.rangeS = ⊤

Tactic:
rangeS_top_iff_surjective.2 hf

Premises used: Iff.mpr, RingHom.rangeS_top_iff_surjective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring 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.eqLocusS g from closure_le.2 h

Premises used: Iff.mpr, Subsemiring.closure_le, Set.Mem, setOf, Set.EqOn
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring 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 _ => h (mem_top _)

Premises used: Subsemiring.mem_top, RingHom.ext
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Set R
hs : Eq (α := Subsemiring 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_stop <| hs ▸ eqOn_sclosure h

Premises used: RingHom.eq_of_eqOn_stop, Eq.rec, RingHom.eqOn_sclosure
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
s : Set S
⊢ closure ((⇑f : (a : R) → S) ⁻¹' s) ≤ comap f (closure s)

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

Premises used: Iff.mpr, Subsemiring.closure_le, Subsemiring.subset_closure, Subsemiring.mem_comap, SetLike.mem_coe
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
s : Set R
⊢ map f (closure s) = closure ((⇑f : (a : R) → S) '' s)

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

Premises used: GaloisConnection.l_comm_of_u_comm, Subsemiring.gc_map_comap, Set.image_preimage, Subsemiring.gi, Subsemiring.coe_comap, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ comp (g.domRestrict f.rangeS) f.rangeSRestrict = g.comp f

Tactic:
rfl

Premises used: RingHom.domRestrict, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
S T : Subsemiring R
h : S ≤ T
⊢ Function.Injective (α := ↥S) (β := ↥T) (⇑(inclusion h) : (a : ↥S) → ↥T)

Tactic:
Set.inclusion_injective h

Premises used: Set.inclusion_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ s.subtype.rangeS = s

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

Premises used: SetLike.coe_injective, Subtype.range_coe, Eq.trans, RingHom.coe_rangeS
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := Subsemiring R) (rangeS (fst R S)) ⊤

Tactic:
(fst R S).rangeS_top_of_surjective <| Prod.fst_surjective

Premises used: Prod.fst_surjective, RingHom.rangeS_top_of_surjective, RingHom.fst
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := Subsemiring S) (rangeS (snd R S)) ⊤

Tactic:
(snd R S).rangeS_top_of_surjective <| Prod.snd_surjective

Premises used: RingHom.snd, RingHom.rangeS_top_of_surjective, Prod.snd_surjective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring R
t : Subsemiring S
⊢ s.prod ⊥ ⊔ prod ⊥ t = s.prod t

Tactic:
le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) fun p hp =>
    Prod.fst_mul_snd p ▸
      mul_mem
        ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, SetLike.mem_coe.2 <| one_mem ⊥⟩)
        ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨SetLike.mem_coe.2 <| one_mem ⊥, hp.2⟩)

Premises used: Iff.mpr, Prod.fst_mul_snd, le_sup_left, Subsemiring.prod_mono_right, Eq.rec, le_sup_right, Bot.bot, le_antisymm, And.right, And.left, SetLike.mem_coe, And.intro, Subsemiring.prod_mono_left, sup_le, OneMemClass.one_mem, bot_le, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.rangeS
let :
  ∀ (x' : R) (hx' : (f : (a : R) → S) x' = (↑x : S)),
    (↑((fun (x : R) ↦ ((f.rangeSRestrict : (a : R) → ↥f.rangeS) x : ↥f.rangeS))
            ((fun (x : ↥f.rangeS) ↦ (g ∘ (⇑f.rangeS.subtype : (a : ↥f.rangeS) → S)) x) x)) :
        S) =
      (↑x : S)
⊢ (↑((fun (x : R) ↦ ((f.rangeSRestrict : (a : R) → ↥f.rangeS) x : ↥f.rangeS))
          ((fun (x : ↥f.rangeS) ↦ (g ∘ (⇑f.rangeS.subtype : (a : ↥f.rangeS) → S)) x) x)) :
      S) =
    (↑x : S)

Tactic:
let ⟨x', hx'⟩ := RingHom.mem_rangeS.mp x.prop
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
s t : Subsemiring R
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.rangeS
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
⊢ (↑((fun (x : R) ↦ ((f.rangeSRestrict : (a : R) → ↥f.rangeS) x : ↥f.rangeS))
          ((fun (x : ↥f.rangeS) ↦ (g ∘ (⇑f.rangeS.subtype : (a : ↥f.rangeS) → S)) x) x)) :
      S) =
    (↑x : S)

Tactic:
simp [← hx', h x']
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : R
⊢ Eq.{v + 1} (α := S) ((↑((ofLeftInverseS h : (a : R) → ↥f.rangeS) x) : S) : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
g : S → R
f : R →+* S
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥f.rangeS
⊢ ((ofLeftInverseS h).symm : (a : ↥f.rangeS) → R) x = g (↑x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
s : Subsemiring R
x : ↥s
⊢ Eq.{v + 1} (α := S) ((↑((e.subsemiringMap s : (a : ↥s) → ↥(Subsemiring.map (↑e : R →+* S) s)) x) : S) : S)
    ((e : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
s : Subsemiring R
x : ↥(Subsemiring.map e.toRingHom s)
⊢ Eq.{u + 1} (α := R) ((↑(((e.subsemiringMap s).symm : (a : ↥(Subsemiring.map (↑e : R →+* S) s)) → ↥s) x) : R) : R)
    ((e.symm : (a : S) → R) (↑x : S) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R' : Type u_1
α : Type u_2
inst : NonAssocSemiring R'
inst_1 : SMul R' α
S : Subsemiring R'
g : ↥S
m : α
⊢ g • m = (↑g : R') • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S_1
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S_1
inst_4 : NonAssocSemiring R'
inst_5 : SMul R' β
inst_6 : SMul α β
inst_7 : SMulCommClass R' α β
S : Subsemiring R'
⊢ SMulCommClass.{u_1, u_2, u_3} (↥S) α β

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S_1
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S_1
inst_4 : NonAssocSemiring R'
inst_5 : SMul α β
inst_6 : SMul R' β
inst_7 : SMulCommClass α R' β
S : Subsemiring R'
⊢ SMulCommClass.{u_2, u_1, u_3} α (↥S) β

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R_1
M_1 : Submonoid R_1
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S
inst_4 : NonAssocSemiring R'
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : MulAction R M
⊢ SMulCommClass R (↥(center R)) M

Tactic:
inferInstanceAs <| SMulCommClass R (Submonoid.center R) M

Premises used: _private.0.Subsemiring.instSMulCommClassSubtypeMemCenter._proof_1
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R_1
M_1 : Submonoid R_1
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S
inst_4 : NonAssocSemiring R'
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : MulAction R M
⊢ SMulCommClass (↥(center R)) R M

Tactic:
inferInstanceAs <| SMulCommClass (Submonoid.center R) R M

Premises used: _private.0.Subsemiring.instSMulCommClassSubtypeMemCenter_1._proof_1
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S_1
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S_1
inst_4 : NonAssocSemiring R'
inst_5 : SMul α β
inst_6 : SMul R' α
inst_7 : SMul R' β
inst_8 : IsScalarTower R' α β
S : Subsemiring R'
⊢ IsScalarTower.{u_1, u_2, u_3} (↥S) α β

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R' : Type u_1
α_1 : Type u_2
β : Type u_3
S'_1 : Type u_4
inst_3 : SetLike S'_1 R'
s_1 : S
inst_4 : NonAssocSemiring R'
M' : Type u_5
α : Type u_6
inst_5 : SMul M' α
S' : Type u_7
inst_6 : SetLike S' M'
s : S'
inst_7 : FaithfulSMul M' α
⊢ FaithfulSMul.{u_5, u_6} (↥s) α

Tactic:
⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩

Premises used: FaithfulSMul.eq_of_smul_eq_smul, FaithfulSMul.mk, Subtype.ext
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S_1
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S_1
inst_4 : NonAssocSemiring R'
inst_5 : SMul R' α
inst_6 : FaithfulSMul R' α
S : Subsemiring R'
⊢ FaithfulSMul.{u_1, u_2} (↥S) α

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S
inst_4 : Semiring R'
⊢ SMulCommClass (↥(center R')) R' R'

Tactic:
Submonoid.center.smulCommClass_left

Premises used: Set.Mem, setOf, Set.center, Submonoid.center.smulCommClass_left, Subsemiring.center, Submonoid.center
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s : S
inst_4 : Semiring R'
⊢ SMulCommClass R' (↥(center R')) R'

Tactic:
Submonoid.center.smulCommClass_right

Premises used: Set.Mem, setOf, Set.center, Submonoid.center.smulCommClass_right, Subsemiring.center, Submonoid.center
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R' : Type u_1
inst : Semiring R'
s : Set R'
⊢ LE.le (α := Subsemiring R') (closure s) (centralizer (↑(centralizer s) : Set R'))

Tactic:
closure_le.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Subsemiring.closure_le, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R' : Type u_1
inst : Semiring 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: IsMulCommutative.of_setLike_mul_comm, Subsemiring.closure_le_centralizer_centralizer, Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocSemiring R
M : Submonoid R
inst_1 : NonAssocSemiring S_1
inst_2 : NonAssocSemiring T
R' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst_3 : SetLike S' R'
s_1 : S_1
inst_4 : Semiring R'
S : Type u_5
inst_5 : SetLike S R'
inst_6 : MulMemClass S R'
s : S
inst_7 : IsMulCommutative.{u_1} ↥s
⊢ IsMulCommutative.{u_1} ↥(closure (↑s : Set R'))

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

Premises used: setLike_mul_comm, Subsemiring.isMulCommutative_closure
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
⊢ map f (comap f t) = t ⊓ f.rangeS

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
h : t ≤ f.rangeS
⊢ map f (comap f t) = t

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

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

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : Subsemiring 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.Subsemiring.Defs
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
s : S
inst_2 : AddSubmonoidWithOneClass S R
n : ℕ
zero : (↑0 : R) ∈ s
succ : ∀ (n : ℕ), (↑n : R) ∈ s → (↑(n + 1) : R) ∈ s
⊢ (↑n : R) ∈ s

Tactic:
induction n
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
s : S
inst_2 : AddSubmonoidWithOneClass S R
⊢ (↑0 : R) ∈ s

Tactic:
simp [zero_mem, add_mem, one_mem, *]

Premises used: AddMemClass.add_mem, ZeroMemClass.zero_mem, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Defs
Goal:
S : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : SetLike S R
s : S
inst_2 : AddSubmonoidWithOneClass S R
n : ℕ
h : (↑n : R) ∈ s
⊢ (↑(n + 1) : R) ∈ s

Tactic:
simp [zero_mem, add_mem, one_mem, *]

Premises used: AddMemClass.add_mem, ZeroMemClass.zero_mem, OneMemClass.one_mem
-- 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
rw : (↑(OfNat.ofNat n) : R) ∈ s
⊢ OfNat.ofNat n ∈ s

Tactic:
rw [← Nat.cast_ofNat]

Premises used: Nat.cast_ofNat
-- 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:
natCast_mem s n

Premises used: Set.Mem, natCast_mem