awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ StrictMono.{u, u} (α := Subsemiring R) toAddSubmonoid

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ Monotone.{u, u} (α := Subsemiring R) toAddSubmonoid

Tactic:
toAddSubmonoid_strictMono.monotone

Premises used: StrictMono.monotone, Subsemiring.toAddSubmonoid_strictMono
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Subsemiring R
l : List R
⊢ (∀ x ∈ l, x ∈ s) → l.prod ∈ s

Tactic:
list_prod_mem

Premises used: list_prod_mem, Set.Mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
l : List R
⊢ (∀ x ∈ l, x ∈ s) → l.sum ∈ s

Tactic:
list_sum_mem

Premises used: Set.Mem, list_sum_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
s : Subsemiring R
m : Multiset R
⊢ (∀ a ∈ m, a ∈ s) → m.prod ∈ s

Tactic:
multiset_prod_mem m

Premises used: multiset_prod_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
m : Multiset R
⊢ (∀ a ∈ m, a ∈ s) → m.sum ∈ s

Tactic:
multiset_sum_mem m

Premises used: multiset_sum_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
s : Subsemiring R
ι : Type u_2
t : Finset ι
f : ι → R
h : ∀ c ∈ t, f c ∈ s
⊢ ∏ i ∈ t, f i ∈ s

Tactic:
prod_mem h

Premises used: prod_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
ι : Type u_1
t : Finset ι
f : ι → R
h : ∀ c ∈ t, f c ∈ s
⊢ ∑ i ∈ t, f i ∈ s

Tactic:
sum_mem h

Premises used: sum_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring S
f : R →+* S
x : R
⊢ x ∈ comap f s ↔ Membership.mem (α := S) s ((f : (a : R) → S) x : S)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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
s : Subsemiring T
g : S →+* T
f : R →+* S
⊢ comap f (comap g s) = comap (g.comp f) s

Tactic:
rfl

Premises used: Set.Mem, setOf, Subsemiring.comap, Set.preimage, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
s : Subsemiring R
y : S
⊢ y ∈ map f s ↔ ∃ x ∈ s, (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ map (RingHom.id R) s = s

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- 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
s : Subsemiring R
g : S →+* T
f : R →+* S
⊢ map g (map f s) = map (g.comp f) s

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

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
s : Subsemiring R
t : Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: Subsemiring.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : ↥s
⊢ Eq.{v + 1} (α := S) ((↑((s.equivMapOfInjective f hf : (a : ↥s) → ↥(map f 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
f : R →+* S
y : S
⊢ y ∈ f.rangeS ↔ ∃ (x : R), (f : (a : R) → S) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
h : ∀ (x : S), x ∈ f.rangeS ↔ x ∈ Subsemiring.map f ⊤
⊢ f.rangeS = Subsemiring.map f ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
x : S
⊢ x ∈ f.rangeS ↔ x ∈ Subsemiring.map f ⊤

Tactic:
simp
-- 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
⊢ Membership.mem (α := S) f.rangeS ((f : (a : R) → S) x : S)

Tactic:
mem_rangeS.mpr ⟨x, rfl⟩

Premises used: Iff.mpr, RingHom.mem_rangeS, Exists.intro, 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
⊢ Subsemiring.map g f.rangeS = (g.comp f).rangeS

Tactic:
simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f

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

Tactic:
simp [← Set.range_eq_univ, SetLike.ext'_iff]

Premises used: Set.range_eq_univ, SetLike.ext'_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ (↑⊥ : Set R) = Set.range Nat.cast

Tactic:
(Nat.castRingHom R).coe_rangeS

Premises used: Nat.castRingHom, RingHom.coe_rangeS
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
x : R
⊢ Membership.mem (γ := Subsemiring R) ⊥ x ↔ ∃ (n : ℕ), (↑n : R) = x

Tactic:
RingHom.mem_rangeS

Premises used: Set.Mem, RingHom.mem_rangeS
-- 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 : Set (Subsemiring R)
⊢ (↑(⨅ t ∈ s, t.toSubmonoid) : Set R) = ⋂ t ∈ s, (↑t : Set R)

Tactic:
simp
-- 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 : Set (Subsemiring R)
⊢ (↑(⨅ t ∈ s, t.toAddSubmonoid) : Set R) = ⋂ t ∈ s, (↑t : Set R)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
S : Set (Subsemiring R)
⊢ (↑(sInf S) : Set R) = ⋂ s ∈ S, (↑s : Set R)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
S : Set (Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
⊢ (↑(⨅ (i : ι), S i) : Set R) = ⋂ (i : ι), (↑(S i) : Set R)

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

Premises used: iInf, Subsemiring.coe_sInf, Set.biInter_range
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
x : R
⊢ Membership.mem (γ := Subsemiring 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, Subsemiring.mem_sInf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set (Subsemiring R)
⊢ (sInf s).toSubmonoid = ⨅ t ∈ s, t.toSubmonoid

Tactic:
mk'_toSubmonoid _ _

Premises used: Subsemiring.mk'_toSubmonoid
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set (Subsemiring R)
⊢ (sInf s).toAddSubmonoid = ⨅ t ∈ s, t.toAddSubmonoid

Tactic:
mk'_toAddSubmonoid _ _

Premises used: Subsemiring.mk'_toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
A : Subsemiring 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: Subsemiring.mem_top, eq_top_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R_1
M : Submonoid R_1
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R : Type u_1
inst_3 : Semiring R
⊢ Eq (α := Semiring ↥(center R)) CommSemiring.toSemiring (toSemiring (center R))

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocSemiring R_1
M : Submonoid R_1
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
R : Type u_1
inst_3 : Semiring R
⊢ Eq (α := Semiring ↥(center R)) CommSemiring.toSemiring (toSemiring (center R))

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
z : R
⊢ Membership.mem (γ := Subsemiring R) (center R) z ↔ ∀ (g : R), g * z = z * g

Tactic:
Subsemigroup.mem_center_iff

Premises used: Set.Mem, setOf, Subsemigroup.mem_center_iff, Set.center
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := Subsemiring R) (center R) ⊤

Tactic:
SetLike.coe_injective (Set.center_eq_univ R)

Premises used: Set.center_eq_univ, SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
⊢ (↑(centralizer s) : Set R) = s.centralizer

Tactic:
rfl

Premises used: setOf, Set.centralizer, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
⊢ Eq (α := Submonoid R) (toSubmonoid (centralizer s)) (Submonoid.centralizer s)

Tactic:
rfl

Premises used: Submonoid.centralizer, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
z : R
⊢ Membership.mem (γ := Subsemiring R) (centralizer s) z ↔ ∀ g ∈ s, g * z = z * g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.centralizer
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
⊢ LE.le (α := Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s t : Set R
h : s ⊆ t
⊢ LE.le (α := Subsemiring R) (centralizer t) (centralizer s)

Tactic:
Set.centralizer_subset h

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.centralizer_subset
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
⊢ Eq (α := Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := Subsemiring R) (centralizer Set.univ) (center R)

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

Premises used: SetLike.ext', Set.centralizer_univ
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Subsemiring R
⊢ s ≤ centralizer (↑(centralizer (↑s : Set R)) : Set R)

Tactic:
Set.subset_centralizer_centralizer

Premises used: Set.Mem, setOf, Set.centralizer, Set.Subset, Set.subset_centralizer_centralizer
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
a : (↑(centralizer s.centralizer.centralizer) : Set R) = (↑(centralizer s) : Set R)
⊢ Eq (α := Subsemiring R) (centralizer s.centralizer.centralizer) (centralizer s)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
⊢ (↑(centralizer s.centralizer.centralizer) : Set R) = (↑(centralizer s) : Set R)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Premises used: Set.centralizer_centralizer_centralizer, Subsemiring.coe_centralizer
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
x : R
s : Set R
⊢ Membership.mem (γ := Subsemiring R) (closure s) x ↔ ∀ (S : Subsemiring R), s ⊆ (↑S : Set R) → x ∈ S

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, Subsemiring.mem_sInf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
⊢ s ⊆ (↑(closure s) : Set R)

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

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

Tactic:
subset_closure hx

Premises used: Subsemiring.subset_closure
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
P : R
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: Subsemiring.subset_closure, Not
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
t : Subsemiring R
⊢ closure s ≤ t ↔ s ⊆ (↑t : Set R)

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

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

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

Premises used: Iff.mpr, Subsemiring.closure_le, Set.Subset.trans, Subsemiring.subset_closure
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
t : Subsemiring 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, Subsemiring.closure_le, le_antisymm
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
K : Subsemiring 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
K : Subsemiring R
x : S
⊢ Membership.mem (γ := Subsemiring S) (map (↑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 using 1

Premises used: Set.mem_image_equiv
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
K : Subsemiring R
⊢ Eq (α := Subsemiring S) (map (↑f : R →+* S) K) (comap (↑f.symm : S →+* R) 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.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
K : Subsemiring S
⊢ Eq (α := Subsemiring R) (comap (↑f : R →+* S) K) (map (↑f.symm : S →+* R) K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: Subsemiring.map_equiv_eq_comap_symm, Equiv.symm, Eq.symm, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
⊢ (↑M.subsemiringClosure : Set R) = (↑(AddSubmonoid.closure (↑M : Set R)) : Set R)

Tactic:
rfl

Premises used: iInf, Set.iInter, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
⊢ x ∈ M.subsemiringClosure ↔ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) x

Tactic:
Iff.rfl

Premises used: iInf, Set.Mem, Set.iInter, Iff.rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (↑M : Set R)

Tactic:
rfl

Premises used: iInf, Set.iInter, AddSubmonoid.closure, rfl
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure (↑M : Set R)

Tactic:
Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ fun _ hx ↦ ?_)

Premises used: Eq.symm, NonUnitalSubsemiring.closure_eq_of_le
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
refine_1 : (↑M : Set R) ⊆ (↑M.subsemiringClosure.toNonUnitalSubsemiring : Set R)
refine_2 :
  ∀ (x : R) (hx : x ∈ M.subsemiringClosure.toNonUnitalSubsemiring),
    Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x
⊢ M.subsemiringClosure.toNonUnitalSubsemiring = NonUnitalSubsemiring.closure (↑M : Set R)

Tactic:
refine Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ fun _ hx ↦ ?_)

Premises used: Eq.symm, NonUnitalSubsemiring.closure_eq_of_le
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
⊢ (↑M : Set R) ⊆ (↑M.subsemiringClosure.toNonUnitalSubsemiring : Set R)

Tactic:
simp [Submonoid.subsemiringClosure_coe]

Premises used: Submonoid.subsemiringClosure_coe
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
hx : x ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) x

Tactic:
simp only [Subsemiring.mem_toNonUnitalSubsemiring, subsemiringClosure_mem] at hx

Premises used: Subsemiring.mem_toNonUnitalSubsemiring, Submonoid.subsemiringClosure_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) x
refine_2 :
  ∀ x ∈ (↑M : Set R), Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x
refine_2₁ : Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) 0
refine_2₂ :
  ∀ (x y : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) x →
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) y →
        Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x →
          Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) y →
            Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) (x + y)
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x

Tactic:
induction hx using AddSubmonoid.closure_induction
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x x_1 : R
h : x_1 ∈ (↑M : Set R)
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x_1

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x x_1 y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) x_1
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑M : Set R)) y
h : Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) x_1
h_1 : Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) y
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (NonUnitalSubsemiring.closure (↑M : Set R)) (x_1 + y)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
h : ∀ (x : R), x ∈ M.subsemiringClosure ↔ Membership.mem (γ := Subsemiring R) (Subsemiring.closure (↑M : Set R)) x
⊢ M.subsemiringClosure = Subsemiring.closure (↑M : Set R)

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
⊢ x ∈ M.subsemiringClosure ↔ Membership.mem (γ := Subsemiring R) (Subsemiring.closure (↑M : Set R)) x

Tactic:
⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩

Premises used: Subsemiring.mem_closure, Submonoid.subsemiringClosure, Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
h : ∀ (hx : x ∈ M.subsemiringClosure), Membership.mem (γ := Subsemiring R) (Subsemiring.closure (↑M : Set R)) x
h₁ :
  ∀ (hx : Membership.mem (γ := Subsemiring R) (Subsemiring.closure (↑M : Set R)) x) (s : R) (sM : s ∈ (↑M : Set R)),
    s ∈ (↑M.subsemiringClosure : Set R)
⊢ x ∈ M.subsemiringClosure ↔ Membership.mem (γ := Subsemiring R) (Subsemiring.closure (↑M : Set R)) x

Tactic:
refine
    ⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
hx : x ∈ M.subsemiringClosure
H1 : Subsemiring R
H2 : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    x

Tactic:
AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Premises used: Set.Mem, AddSubmonoid.mem_closure, Iff.mp, Subsemiring.toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
hx : x ∈ M.subsemiringClosure
H1 : Subsemiring R
H2 : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (Subsemiring R)) {S : Subsemiring R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    x

Tactic:
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Premises used: AddSubmonoid.mem_closure, Iff.mp, Subsemiring.toAddSubmonoid
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
M : Submonoid R
x : R
hx : Membership.mem (γ := Subsemiring R) (Subsemiring.closure (↑M : Set R)) x
s : R
sM : s ∈ (↑M : Set R)
H1 : AddSubmonoid R
H2 : Membership.mem (γ := Set (AddSubmonoid R)) {S : AddSubmonoid R | (↑M : Set R) ⊆ (↑S : Set R)} H1
⊢ Membership.mem (γ := Set R)
    ((fun (h : Membership.mem (γ := Set (AddSubmonoid R)) {S : AddSubmonoid R | (↑M : Set R) ⊆ (↑S : Set R)} H1) ↦
        (↑H1 : Set R))
      H2)
    s

Tactic:
H2 sM

Premises used: Set.Mem