awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
mp :
  Membership.mem (γ := Subsemiring R) (closure s) x →
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
mpr :
  (∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) →
    Membership.mem (γ := Subsemiring R) (closure s) x
⊢ Membership.mem (γ := Subsemiring R) (closure s) x ↔
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
hx : Membership.mem (γ := Subsemiring R) (closure s) x
⊢ Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x

Tactic:
rw [mem_closure_iff] at hx

Premises used: Subsemiring.mem_closure_iff
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
this : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
rw : [t.prod].sum = x
rw₁ : t.prod = x
rw₂ rw₃ : x = x
⊢ (List.map List.prod [t]).sum = x

Tactic:
rw [List.map_singleton, List.sum_singleton, ht2]

Premises used: List.map_singleton, List.sum_singleton
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
mp : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x_2 x : R
hx : x ∈ s
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩

Premises used: Iff.mpr, List.forall_mem_singleton, List.cons, List.prod_singleton, And.intro, Exists.intro, List.nil
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x_2 x : R
hx : x ∈ s
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x : R
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = 1

Tactic:
⟨[], List.forall_mem_nil _, rfl⟩

Premises used: And.intro, Exists.intro, List.forall_mem_nil, rfl, List.nil
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x : R
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = 1

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x_2 x y : R
hx : Membership.mem (γ := Submonoid R) (Submonoid.closure s) x
hy : Membership.mem (γ := Submonoid R) (Submonoid.closure s) y
ht : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = y
mp :
  ∀ (t : List R) (ht1 : ∀ y ∈ t, y ∈ s) (ht2 : t.prod = x) (u : List R) (hu1 : ∀ y ∈ u, y ∈ s) (hu2 : u.prod = y),
    ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y

Tactic:
obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu

Premises used: And.intro
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x_2 x y : R
hx : Membership.mem (γ := Submonoid R) (Submonoid.closure s) x
hy : Membership.mem (γ := Submonoid R) (Submonoid.closure s) y
ht : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
rw : t.prod * u.prod = x * y
rw₁ : x * u.prod = x * y
rw₂ rw₃ : x * y = x * y
⊢ (t ++ u).prod = x * y

Tactic:
rw [List.prod_append, ht2, hu2]

Premises used: List.prod_append
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x_2 x y : R
hx : Membership.mem (γ := Submonoid R) (Submonoid.closure s) x
hy : Membership.mem (γ := Submonoid R) (Submonoid.closure s) y
ht : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y

Tactic:
exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x : R
hx : x ∈ (↑(Submonoid.closure s) : Set R)
mp : ∀ (x : R) (hx : x ∈ s), ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x
mp₁ : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = 1
mp₂ :
  ∀ (x y : R),
    Membership.mem (γ := Submonoid R) (Submonoid.closure s) x →
      Membership.mem (γ := Submonoid R) (Submonoid.closure s) y →
        ∀ (ht : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x) (hu : ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = y),
          ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y
⊢ ∃ (t : List R), (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0

Tactic:
⟨[], List.forall_mem_nil _, rfl⟩

Premises used: And.intro, Exists.intro, List.forall_mem_nil, rfl, List.nil
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
mp :
  ∀ (L : List (List R)) (HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s) (HL2 : (List.map List.prod L).sum = x) (M : List (List R))
    (HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s) (HM2 : (List.map List.prod M).sum = y),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y

Tactic:
obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM

Premises used: And.intro
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
rw : (List.map List.prod L ++ List.map List.prod M).sum = x + y
rw₁ : (List.map List.prod L).sum + (List.map List.prod M).sum = x + y
rw₂ : x + (List.map List.prod M).sum = x + y
rw₃ rw₄ : x + y = x + y
⊢ (List.map List.prod (L ++ M)).sum = x + y

Tactic:
rw [List.map_append, List.sum_append, HL2, HM2]

Premises used: List.sum_append, List.map_append
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x_1 x y : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y

Tactic:
exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
x : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x
mp :
  ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
mp₁ : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = 0
mp₂ :
  ∀ (x y : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) x →
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (↑(Submonoid.closure s) : Set R)) y →
        ∀ (hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x)
          (hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y),
          ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
induction hx using AddSubmonoid.closure_induction with
    | mem x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
      induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
    | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
    | add x y _ _ hL hM =>
      obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
      exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
⊢ Membership.mem (γ := Subsemiring R) (closure s) (List.map List.prod L).sum

Tactic:
list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

Premises used: Subsemiring.closure, Set.Mem, _private.0.Subsemiring.mem_closure_iff_exists_list.match_2, Membership.mem, Subsemiring.subset_closure, Eq.rec, list_sum_mem, Subsemiring.list_prod_mem, Iff.mp, List.mem_map
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u_1
inst : Semiring R
s : Set R
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
⊢ Membership.mem (γ := Subsemiring R) (closure s) (List.map List.prod L).sum

Tactic:
exact
      list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

Premises used: list_sum_mem
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Subsemiring R
⊢ closure (↑s : Set R) = s

Tactic:
(Subsemiring.gi R).l_u_eq s

Premises used: Subsemiring.gi, GaloisInsertion.l_u_eq
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ Eq.{u + 1} (α := Subsemiring R) (closure ∅) ⊥

Tactic:
(Subsemiring.gi R).gc.l_bot

Premises used: Subsemiring.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
⊢ Eq.{u + 1} (α := Subsemiring R) (closure Set.univ) ⊤

Tactic:
@coe_top R _ ▸ closure_eq ⊤

Premises used: Eq.rec, Subsemiring.closure_eq, Subsemiring.coe_top, Top.top
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s t : Set R
⊢ Eq (α := Subsemiring R) (closure (s ∪ t)) (closure s ⊔ closure t)

Tactic:
(Subsemiring.gi R).gc.l_sup

Premises used: Subsemiring.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
s : ι → Set R
⊢ Eq.{u + 1} (α := Subsemiring R) (closure (⋃ (i : ι), s i)) (⨆ (i : ι), closure (s i))

Tactic:
(Subsemiring.gi R).gc.l_iSup

Premises used: GaloisConnection.l_iSup, Subsemiring.gi, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set (Set R)
⊢ Eq (α := Subsemiring R) (closure (⋃₀ s)) (⨆ t ∈ s, closure t)

Tactic:
(Subsemiring.gi R).gc.l_sSup

Premises used: Set.sUnion, GaloisConnection.l_sSup, Subsemiring.gi, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
n : ℕ
⊢ Eq (α := Subsemiring R) (closure {(↑n : R)}) ⊥

Tactic:
bot_unique <| closure_le.2 <| Set.singleton_subset_iff.mpr <| natCast_mem _ _

Premises used: Iff.mpr, Subsemiring.closure_le, Set.singleton_subset_iff, natCast_mem, bot_unique
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
n : ℕ
s : Set R
rw : Eq (α := Subsemiring R) (closure {(↑n : R)} ⊔ closure s) (closure s)
⊢ Eq (α := Subsemiring R) (closure (insert (↑n : R) s)) (closure s)

Tactic:
rw [Set.insert_eq, closure_union]

Premises used: Set.insert_eq, Subsemiring.closure_union
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
n : ℕ
s : Set R
⊢ Eq (α := Subsemiring R) (closure {(↑n : R)} ⊔ closure s) (closure s)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
⊢ Eq (α := Subsemiring R) (closure (insert 0 s)) (closure s)

Tactic:
mod_cast closure_insert_natCast 0 s

Premises used: Subsemiring.closure_insert_natCast, Subsemiring.closure, congrArg, cast, Insert.insert, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
s : Set R
⊢ Eq (α := Subsemiring R) (closure (insert 1 s)) (closure s)

Tactic:
mod_cast closure_insert_natCast 1 s

Premises used: Subsemiring.closure_insert_natCast, Subsemiring.closure, congrArg, cast, Insert.insert, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s t : Subsemiring R
f : R →+* S
⊢ map f (s ⊔ t) = map f s ⊔ map f t

Tactic:
(gc_map_comap f).l_sup

Premises used: Subsemiring.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ι : Sort u_1
f : R →+* S
s : ι → Subsemiring R
⊢ map f (iSup s) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: Subsemiring.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s t : Subsemiring R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ map f (s ⊓ t) = map f s ⊓ map f t

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ι : Sort u_1
inst_2 : Nonempty ι
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → Subsemiring R
a : (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ι : Sort u_1
inst_2 : Nonempty ι
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → Subsemiring R
⊢ (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s t : Subsemiring S
f : R →+* S
⊢ comap f (s ⊓ t) = comap f s ⊓ comap f t

Tactic:
(gc_map_comap f).u_inf

Premises used: Subsemiring.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ι : Sort u_1
f : R →+* S
s : ι → Subsemiring S
⊢ comap f (iInf s) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: Subsemiring.gc_map_comap, GaloisConnection.u_iInf
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Subsemiring.gc_map_comap, GaloisConnection.l_bot
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R →+* S
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: Subsemiring.gc_map_comap, GaloisConnection.u_top
-- 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 t) : Set (R × S)) = (↑s : Set R) ×ˢ (↑t : Set S)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- 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
p : R × S
⊢ p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s₁ s₂ : Subsemiring R
hs : s₁ ≤ s₂
t₁ t₂ : Subsemiring S
ht : t₁ ≤ t₂
⊢ s₁.prod t₁ ≤ s₂.prod t₂

Tactic:
Set.prod_mono hs ht

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring R
⊢ Monotone (β := Subsemiring (R × S)) fun (t : Subsemiring S) ↦ s.prod t

Tactic:
prod_mono (le_refl s)

Premises used: le_refl, Set.Mem, Monotone, Subsemiring.prod_mono
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
t : Subsemiring S
⊢ Monotone (β := Subsemiring (R × S)) fun (s : Subsemiring R) ↦ s.prod t

Tactic:
fun _ _ hs => prod_mono hs (le_refl t)

Premises used: le_refl, Set.Mem, Monotone, Subsemiring.prod_mono
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring R
x : R × S
⊢ Membership.mem (γ := Subsemiring (R × S)) (s.prod ⊤) x ↔
    Membership.mem (γ := Subsemiring (R × S)) (comap (RingHom.fst R S) s) x

Tactic:
simp [mem_prod]

Premises used: Subsemiring.mem_prod
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
s : Subsemiring S
x : R × S
⊢ Membership.mem (γ := Subsemiring (R × S)) (prod ⊤ s) x ↔
    Membership.mem (γ := Subsemiring (R × S)) (comap (RingHom.snd R S) s) x

Tactic:
simp [mem_prod]

Premises used: Subsemiring.mem_prod
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := Subsemiring (R × S)) (prod ⊤ ⊤) ⊤

Tactic:
(top_prod _).trans <| comap_top _

Premises used: Subsemiring.comap_top, Subsemiring.top_prod, Eq.trans
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Premises used: iSup, Membership.mem, le_iSup, Iff.intro, _private.0.Subsemiring.mem_iSup_of_directed.match_1
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
refine : Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) ⋯ (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
this : ⨆ (i : ι), S i ≤ U
⊢ Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
simpa [U] using @this x
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) ⋯ (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
suffices : ⨆ (i : ι), S i ≤ U
⊢ Membership.mem (γ := Subsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) ⋯ (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
⊢ ⨆ (i : ι), S i ≤ U

Tactic:
iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, iSup_le
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
U : Subsemiring R :=
  Subsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubmonoid) ⋯ (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
⊢ ⨆ (i : ι), S i ≤ U

Tactic:
exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Premises used: iSup_le
-- Module: Mathlib.Algebra.Ring.Subsemiring.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun (x1 x2 : Subsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ x ∈ (↑(⨆ (i : ι), S i) : Set R) ↔ Membership.mem (γ := Set R) (⋃ (i : ι), (↑(S i) : Set R)) x

Tactic:
simp [mem_iSup_of_directed hS]

Premises used: Subsemiring.mem_iSup_of_directed