awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := Subring R) (closure s) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := Subring R) (closure s) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
h₁ : Membership.mem (γ := Subring R) (closure s) x_1
h₂ : Membership.mem (γ := Subring R) (closure s) y
⊢ Membership.mem (γ := Subring R) (closure s) (x_1 + y)

Tactic:
add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
h₁ : Membership.mem (γ := Subring R) (closure s) x_1
h₂ : Membership.mem (γ := Subring R) (closure s) y
⊢ Membership.mem (γ := Subring R) (closure s) (x_1 + y)

Tactic:
exact add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
h : Membership.mem (γ := Subring R) (closure s) x_1
⊢ Membership.mem (γ := Subring R) (closure s) (-x_1)

Tactic:
neg_mem h

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
h : Membership.mem (γ := Subring R) (closure s) x_1
⊢ Membership.mem (γ := Subring R) (closure s) (-x_1)

Tactic:
exact neg_mem h

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
mem : ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)), Membership.mem (γ := Subring R) (closure s) x
zero : Membership.mem (γ := Subring R) (closure s) 0
add :
  ∀ (x y : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y →
        ∀ (h₁ : Membership.mem (γ := Subring R) (closure s) x) (h₂ : Membership.mem (γ := Subring R) (closure s) y),
          Membership.mem (γ := Subring R) (closure s) (x + y)
neg :
  ∀ (x : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
      ∀ (h : Membership.mem (γ := Subring R) (closure s) x), Membership.mem (γ := Subring R) (closure s) (-x)
⊢ Membership.mem (γ := Subring R) (closure s) x

Tactic:
induction h using AddSubgroup.closure_induction with
      | mem x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
      | zero => exact zero_mem _
      | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
      | neg _ _ h => exact neg_mem h

Premises used: Subring.subset_closure, ZeroMemClass.zero_mem, OneMemClass.one_mem, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
⊢ LE.le (α := Subring R) (closure s) (centralizer (↑(centralizer s) : Set R))

Tactic:
closure_le.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Set.subset_centralizer_centralizer, Subring.closure_le
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring 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: Subring.closure_le_centralizer_centralizer, IsMulCommutative.of_setLike_mul_comm, Set.centralizer_centralizer_comm_of_comm
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
S : Type u_1
R : Type u_2
inst_3 : Ring R
inst_4 : SetLike S R
inst_5 : MulMemClass S R
s : S
inst_6 : 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, Subring.isMulCommutative_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
hx : Membership.mem (γ := Subring R) (closure s) x
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x

Tactic:
rw [mem_closure_iff] at hx

Premises used: Subring.mem_closure_iff
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : x_1 ∈ (↑(Submonoid.closure s) : Set R)
mem :
  ∀ (l : List R) (hl : ∀ y ∈ l, y ∈ s) (h : l.prod = x_1),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1

Tactic:
obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx

Premises used: Submonoid.exists_list_of_mem_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : x_1 ∈ (↑(Submonoid.closure s) : Set R)
l : List R
hl : ∀ y ∈ l, y ∈ s
h : l.prod = x_1
⊢ (∀ t ∈ [l], ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod [l]).sum = x_1

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : x_1 ∈ (↑(Submonoid.closure s) : Set R)
l : List R
hl : ∀ y ∈ l, y ∈ s
h : l.prod = x_1
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1

Tactic:
exact ⟨[l], by simp_all⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (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.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 0

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

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

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

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

Premises used: List.sum_append, List.map_append
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 y : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x_1
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1 + 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.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
neg :
  ∀ (L : List (List R)) (hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x_1
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x_1

Tactic:
obtain ⟨L, hL⟩ := hL
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
⊢ Eq.{u_1 + 1} (α := R) (List.sum (List.map List.prod (List.map (List.cons (-1)) [])))
    (-List.sum (List.map List.prod []))

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
⊢ ∀ (head : List R) (tail : List (List R))
    (tail_ih : (List.map List.prod (List.map (List.cons (-1)) tail)).sum = -(List.map List.prod tail).sum),
    (List.map List.prod (List.map (List.cons (-1)) (head :: tail))).sum = -(List.map List.prod (head :: tail)).sum

Tactic:
simp +contextual [List.map_cons, add_comm]

Premises used: List.map_cons, add_comm
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x_1
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x_1
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x_1

Tactic:
exact ⟨L.map (List.cons (-1)),
      List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
      hL.2 ▸
        List.recOn L (by simp)
          (by simp +contextual [List.map_cons, add_comm])⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
x : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x
mem :
  ∀ (x : R) (hx : x ∈ (↑(Submonoid.closure s) : Set R)),
    ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
zero : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = 0
add :
  ∀ (x y : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) y →
        ∀ (hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x)
          (hM : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y),
          ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x + y
neg :
  ∀ (x : R),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Submonoid.closure s) : Set R)) x →
      ∀ (hL : ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x),
        ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x
⊢ ∃ (L : List (List R)), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x

Tactic:
induction hx using AddSubgroup.closure_induction with
  | mem _ hx =>
    obtain ⟨l, hl, h⟩ := Submonoid.exists_list_of_mem_closure hx
    exact ⟨[l], by simp_all⟩
  | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
  | add _ _ _ _ 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]⟩
  | neg _ _ hL =>
    obtain ⟨L, hL⟩ := hL
    exact ⟨L.map (List.cons (-1)),
      List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
      hL.2 ▸
        List.recOn L (by simp)
          (by simp +contextual [List.map_cons, add_comm])⟩

Premises used: Submonoid.exists_list_of_mem_closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Subring R
⊢ closure (↑s : Set R) = s

Tactic:
(Subring.gi R).l_u_eq s

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

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

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

Tactic:
@coe_top R _ ▸ closure_eq ⊤

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

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

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

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

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

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

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

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

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

Tactic:
rw [Set.insert_eq, closure_union]

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

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
n : ℕ
s : Set R
⊢ Eq (α := Subring R) (closure (insert (↑n : R) s)) (closure s)

Tactic:
mod_cast closure_insert_intCast n s

Premises used: Int.cast_natCast, congrArg, cast, Insert.insert, Nat.cast, congrFun', Eq, Subring.closure_insert_intCast, Subring.closure
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
s : Set R
⊢ Eq (α := Subring R) (closure (insert 0 s)) (closure s)

Tactic:
mod_cast closure_insert_natCast 0 s

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

Tactic:
mod_cast closure_insert_natCast 1 s

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

Tactic:
(gc_map_comap f).l_sup

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

Tactic:
(gc_map_comap f).l_iSup

Premises used: GaloisConnection.l_iSup, Subring.gc_map_comap
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s t : Subring 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.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
ι : Sort u_1
inst_2 : Nonempty ι
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → Subring 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.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
ι : Sort u_1
inst_2 : Nonempty ι
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → Subring 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.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s t : Subring S
f : R →+* S
⊢ comap f (s ⊓ t) = comap f s ⊓ comap f t

Tactic:
(gc_map_comap f).u_inf

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

Tactic:
(gc_map_comap f).u_iInf

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

Tactic:
(gc_map_comap f).l_bot

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

Tactic:
(gc_map_comap f).u_top

Premises used: GaloisConnection.u_top, Subring.gc_map_comap
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring R
t : Subring 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.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring R
t : Subring 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.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s₁ s₂ : Subring R
hs : s₁ ≤ s₂
t₁ t₂ : Subring 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.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
s : Subring R
⊢ Monotone (β := Subring (R × S)) fun (t : Subring S) ↦ s.prod t

Tactic:
prod_mono (le_refl s)

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

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

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

Tactic:
simp [mem_prod]

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

Tactic:
simp [mem_prod]

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

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

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

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

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

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

Tactic:
simpa [U] using @this x