awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_2
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y_1
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * y_1)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (-x_2 * y_1)

Tactic:
simpa [neg_mul] using neg_mem h

Premises used: neg_mul, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 y x_2 y_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_2
hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y_1
h : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * y_1)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x_2 * -y_1)

Tactic:
simpa [mul_neg] using neg_mem h

Premises used: mul_neg, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x : R
h : Membership.mem (γ := NonUnitalSubring R) (closure s) x
mem :
  ∀ (x : R) (hx : x ∈ s),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x
zero : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) 0
add :
  ∀ (x y : R),
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubring R) (closure s) y →
        ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x)
          (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y),
          Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x + y)
neg :
  ∀ (x : R),
    Membership.mem (γ := NonUnitalSubring R) (closure s) x →
      ∀ (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x),
        Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (-x)
mul :
  ∀ (x y : R) (_hx : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
    (_hy : Membership.mem (γ := NonUnitalSubring R) (closure s) y)
    (hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x)
    (hy : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) y),
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) (x * y)
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x

Tactic:
induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
    | zero => exact zero_mem _
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg x _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Premises used: add_mul, mul_add, neg_mul, ZeroMemClass.zero_mem, mul_neg, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 x_2 : R
h : x_2 ∈ s
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) x_2

Tactic:
subset_closure h

Premises used: NonUnitalSubring.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 x_2 : R
h : x_2 ∈ s
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) x_2

Tactic:
exact subset_closure h

Premises used: NonUnitalSubring.subset_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 x_2 y : R
hx : Membership.mem (γ := Subsemigroup R) (Subsemigroup.closure s) x_2
hy : Membership.mem (γ := Subsemigroup R) (Subsemigroup.closure s) y
h₁ : Membership.mem (γ := NonUnitalSubring R) (closure s) x_2
h₂ : Membership.mem (γ := NonUnitalSubring R) (closure s) y
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) (x_2 * y)

Tactic:
mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 x_2 y : R
hx : Membership.mem (γ := Subsemigroup R) (Subsemigroup.closure s) x_2
hy : Membership.mem (γ := Subsemigroup R) (Subsemigroup.closure s) y
h₁ : Membership.mem (γ := NonUnitalSubring R) (closure s) x_2
h₂ : Membership.mem (γ := NonUnitalSubring R) (closure s) y
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) (x_2 * y)

Tactic:
exact mul_mem h₁ h₂

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 : R
hx : x_1 ∈ (↑(Subsemigroup.closure s) : Set R)
mem : ∀ (x : R) (h : x ∈ s), Membership.mem (γ := NonUnitalSubring R) (closure s) x
mem₁ :
  ∀ (x y : R),
    Membership.mem (γ := Subsemigroup R) (Subsemigroup.closure s) x →
      Membership.mem (γ := Subsemigroup R) (Subsemigroup.closure s) y →
        ∀ (h₁ : Membership.mem (γ := NonUnitalSubring R) (closure s) x)
          (h₂ : Membership.mem (γ := NonUnitalSubring R) (closure s) y),
          Membership.mem (γ := NonUnitalSubring R) (closure s) (x * y)
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) x_1

Tactic:
induction hx using Subsemigroup.closure_induction with
      | mem _ h => exact subset_closure h
      | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) 0

Tactic:
exact zero_mem _

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

Tactic:
add_mem h₁ h₂

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

Tactic:
exact add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1
h : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) (-x_1)

Tactic:
neg_mem h

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : Set R
x x_1 : R
hx : Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (↑(Subsemigroup.closure s) : Set R)) x_1
h : Membership.mem (γ := NonUnitalSubring R) (closure s) x_1
⊢ Membership.mem (γ := NonUnitalSubring R) (closure s) (-x_1)

Tactic:
exact neg_mem h

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

Tactic:
induction h using AddSubgroup.closure_induction with
    | mem _ hx => induction hx using Subsemigroup.closure_induction with
      | mem _ h => exact subset_closure h
      | 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: ZeroMemClass.zero_mem, NonUnitalSubring.subset_closure, NegMemClass.neg_mem
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
⊢ LE.le (α := NonUnitalSubring R) (closure s) (centralizer (↑(centralizer s) : Set R))

Tactic:
closure_le.mpr Set.subset_centralizer_centralizer

Premises used: Iff.mpr, Set.subset_centralizer_centralizer, NonUnitalSubring.closure_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u_1
inst : NonUnitalRing 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, Set.centralizer_centralizer_comm_of_comm, NonUnitalSubring.closure_le_centralizer_centralizer
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R_1 : Type u
S_1 : Type v
inst : NonUnitalNonAssocRing R_1
inst_1 : NonUnitalNonAssocRing S_1
inst_2 : FunLike F R_1 S_1
inst_3 : NonUnitalRingHomClass F R_1 S_1
S : Type u_1
R : Type u_2
inst_4 : NonUnitalRing R
inst_5 : SetLike S R
inst_6 : MulMemClass S R
s : S
inst_7 : 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, NonUnitalSubring.isMulCommutative_closure
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
s : NonUnitalSubring R
⊢ closure (↑s : Set R) = s

Tactic:
(NonUnitalSubring.gi R).l_u_eq s

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

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

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

Tactic:
@coe_top R _ ▸ closure_eq ⊤

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

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

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

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

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

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

Premises used: Set.sUnion, GaloisConnection.l_sSup, NonUnitalSubring.gi, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s t : NonUnitalSubring R
f : F
⊢ Eq (α := NonUnitalSubring S) (map f (s ⊔ t)) (map f s ⊔ map f t)

Tactic:
(gc_map_comap f).l_sup

Premises used: NonUnitalSubring.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_1
f : F
s : ι → NonUnitalSubring R
⊢ Eq (α := NonUnitalSubring S) (map f (iSup s)) (⨆ (i : ι), map f (s i))

Tactic:
(gc_map_comap f).l_iSup

Premises used: GaloisConnection.l_iSup, NonUnitalSubring.gc_map_comap
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s t : NonUnitalSubring R
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := NonUnitalSubring 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.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_1
inst_4 : Nonempty ι
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → NonUnitalSubring R
a : (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)
⊢ Eq (α := NonUnitalSubring S) (map f (iInf s)) (⨅ (i : ι), map f (s i))

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_1
inst_4 : Nonempty ι
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → NonUnitalSubring 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.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
s t : NonUnitalSubring S
f : F
⊢ Eq (α := NonUnitalSubring R) (comap f (s ⊓ t)) (comap f s ⊓ comap f t)

Tactic:
(gc_map_comap f).u_inf

Premises used: GaloisConnection.u_inf, NonUnitalSubring.gc_map_comap
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
F : Type w
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_1
f : F
s : ι → NonUnitalSubring S
⊢ Eq (α := NonUnitalSubring R) (comap f (iInf s)) (⨅ (i : ι), comap f (s i))

Tactic:
(gc_map_comap f).u_iInf

Premises used: GaloisConnection.u_iInf, NonUnitalSubring.gc_map_comap
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ Eq (α := NonUnitalSubring S) (map f ⊥) ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: GaloisConnection.l_bot, NonUnitalSubring.gc_map_comap
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ Eq (α := NonUnitalSubring R) (comap f ⊤) ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: GaloisConnection.u_top, NonUnitalSubring.gc_map_comap
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s : NonUnitalSubring R
t : NonUnitalSubring S
⊢ (↑(s.prod t) : Set (R × S)) = (↑s : Set R) ×ˢ (↑t : Set S)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s : NonUnitalSubring R
t : NonUnitalSubring 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.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s₁ s₂ : NonUnitalSubring R
hs : s₁ ≤ s₂
t₁ t₂ : NonUnitalSubring 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.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s : NonUnitalSubring R
⊢ Monotone (β := NonUnitalSubring (R × S)) fun (t : NonUnitalSubring S) ↦ s.prod t

Tactic:
prod_mono (le_refl s)

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

Tactic:
fun _s₁ _s₂ hs => prod_mono hs (le_refl t)

Premises used: le_refl, Set.Mem, Monotone, NonUnitalSubring.prod_mono
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s : NonUnitalSubring R
x : R × S
⊢ Membership.mem (γ := NonUnitalSubring (R × S)) (s.prod ⊤) x ↔
    Membership.mem (γ := NonUnitalSubring (R × S)) (comap (F := R × S →ₙ+* R) (NonUnitalRingHom.fst R S) s) x

Tactic:
simp [mem_prod]

Premises used: NonUnitalSubring.mem_prod
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
s : NonUnitalSubring S
x : R × S
⊢ Membership.mem (γ := NonUnitalSubring (R × S)) (prod ⊤ s) x ↔
    Membership.mem (γ := NonUnitalSubring (R × S)) (comap (F := R × S →ₙ+* S) (NonUnitalRingHom.snd R S) s) x

Tactic:
simp [mem_prod]

Premises used: NonUnitalSubring.mem_prod
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
⊢ Eq (α := NonUnitalSubring (R × S)) (prod ⊤ ⊤) ⊤

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

Premises used: NonUnitalSubring.comap_top, NonUnitalSubring.top_prod, Eq.trans
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
⊢ Membership.mem (γ := NonUnitalSubring 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, _private.0.NonUnitalSubring.mem_iSup_of_directed.match_1, Iff.intro
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
refine : Membership.mem (γ := NonUnitalSubring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
⊢ Membership.mem (γ := NonUnitalSubring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i

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

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

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) (⨆ (i : ι), (S i).toAddSubgroup)
    ⋯ ⋯
⊢ ⨆ (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.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) (⨆ (i : ι), (S i).toAddSubgroup)
    ⋯ ⋯
⊢ ⨆ (i : ι), S i ≤ U

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

Premises used: iSup_le
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
ι : Sort u_1
inst_1 : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun (x1 x2 : NonUnitalSubring 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: NonUnitalSubring.mem_iSup_of_directed
-- Module: Mathlib.RingTheory.NonUnitalSubring.Basic
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubring R) ↦ x1 ≤ x2) S
x : R
⊢ Nonempty.{u + 1} (↑S : Type u)

Tactic:
haveI : Nonempty S := Sne.to_subtype