mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : -x ∈ s
hy : y ∈ s
⊢ -(x * y) ∈ s

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : -x ∈ s
hy : y ∈ s
⊢ -(x * y) ∈ s
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : x ∈ s
hy : -y ∈ s
⊢ -(x * y) ∈ s

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Mul R
inst✝² : HasDistribNeg R
inst✝¹ : SetLike S R
inst✝ : MulMemClass S R
s : S
x y : R
hx : x ∈ s
hy : -y ∈ s
⊢ -(x * y) ∈ s
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
p : Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : InjOn ⇑f ↑p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
hxy : (f.submoduleMap p) ⟨x, hx⟩ = (f.submoduleMap p) ⟨y, hy⟩
⊢ f x = f y

Tactic:
simpa using

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
p : Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : InjOn ⇑f ↑p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
hxy : (f.submoduleMap p) ⟨x, hx⟩ = (f.submoduleMap p) ⟨y, hy⟩
⊢ f x = f y
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa using

Goal state after:
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
this : x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer

Tactic:
exact zero_mem_centralizer

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ (x y : M),
    x ∈ closure (⋃ i, ↑(S i)) → y ∈ closure (⋃ i, ↑(S i)) → (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i

Tactic:
rintro x y _ _ ⟨i, hi⟩ ⟨j, hj⟩

Goal state after:
case refine_2
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
⊢ ∃ i, x * y ∈ S i
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a b : G₀
ha : a ∈ s.centralizer
hb : b ∈ s.centralizer
⊢ a / b ∈ s.centralizer

Tactic:
simpa using

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a b : G₀
ha : a ∈ s.centralizer
hb : b ∈ s.centralizer
⊢ a * b⁻¹ ∈ s.centralizer
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑n * (x✝¹ * x✝) + x✝¹ * x✝ = (↑n + 1) * x✝¹ * x✝

Tactic:
ihn,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑n * x✝¹ * x✝ + x✝¹ * x✝ = (↑n + 1) * x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * ↑n + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * (↑n + 1))

Tactic:
ihn,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * (↑n + 1))
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: case add
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : r * b ∈ closure ↑S
hs : s * b ∈ closure ↑S
⊢ (r + s) * b ∈ closure ↑S

Tactic:
simpa using

Goal state after:
case add
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : r * b ∈ closure ↑S
hs : s * b ∈ closure ↑S
⊢ r * b + s * b ∈ closure ↑S
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: case add
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : a * r ∈ closure ↑S
hs : a * s ∈ closure ↑S
⊢ a * (r + s) ∈ closure ↑S

Tactic:
simpa using

Goal state after:
case add
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : a * r ∈ closure ↑S
hs : a * s ∈ closure ↑S
⊢ a * r + a * s ∈ closure ↑S
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_5
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f : R →ₙ+* S × T
x : R
⊢ (((fst S T).comp f).prod ((snd S T).comp f)) x = f x

Tactic:
by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
f : R →+* S × T
x : R
⊢ (((fst S T).comp f).prod ((snd S T).comp f)) x = f x

Tactic:
by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f : M →ₙ* N
⊢ map g f.srange = (g.comp f).srange

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f : M →ₙ* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
S : Subsemigroup N
h : S ≤ f.srange
⊢ map f (comap f S) = S

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
S : Subsemigroup N
h : S ≤ f.srange
⊢ map f (comap f S) = S
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
by
  have : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g f.range = (g.comp f).range

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
T : Type u_1
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : NonUnitalNonAssocRing S
inst✝ : NonUnitalNonAssocRing T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ NonUnitalSubring.map g (NonUnitalSubring.map f ⊤) = NonUnitalSubring.map (g.comp f) ⊤
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ x • x • ↑h.unit⁻¹ m' = x • m'
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ Subsemiring.map g f.rangeS = (g.comp f).rangeS

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f : R →+* S
⊢ Subsemiring.map g (Subsemiring.map f ⊤) = Subsemiring.map (g.comp f) ⊤
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit m' = ↑h.unit (↑h.unit⁻¹ (x • m'))

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ x • m' = x • x • ↑h.unit⁻¹ m'
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul.add_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ (x✝ + y✝) * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
case mul.add_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * z✝ + y✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul.add_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
case mul.add_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ + x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul.neg_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
case mul.neg_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul.neg_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * -y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
case mul.neg_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using

Goal state after:
F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : CharZero R
⊢ FaithfulSMul ℕ R

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : CharZero R
⊢ Injective ⇑(algebraMap ℕ R)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A
inst✝³ : Algebra R✝ A
inst✝² : FaithfulSMul R✝ A
R : Type u_3
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ FaithfulSMul ℤ R

Tactic:
simpa using

Goal state after:
R✝ : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A
inst✝³ : Algebra R✝ A
inst✝² : FaithfulSMul R✝ A
R : Type u_3
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ Injective ⇑(algebraMap ℤ R)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → NonUnitalSubring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → NonUnitalSubring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : R) (x : ι), a ∈ ↑(S x) → ∀ (a_1 : R) (x : ι), a_1 ∈ ↑(S x) → a * a_1 = a_1 * a
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : FaithfulSMul R A
inst✝⁶ : Nontrivial R
inst✝⁵ : IsCancelMulZero A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module A M
inst✝² : Module R M
inst✝¹ : IsTorsionFree A M
inst✝ : IsScalarTower R A M
r : R
hr : IsRegular r
⊢ (algebraMap R A) r ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_3
M : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : FaithfulSMul R A
inst✝⁶ : Nontrivial R
inst✝⁵ : IsCancelMulZero A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module A M
inst✝² : Module R M
inst✝¹ : IsTorsionFree A M
inst✝ : IsScalarTower R A M
r : R
hr : IsRegular r
⊢ ¬r = 0
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
r : R
⊢ (↑↑(algebraMap S A)).toFun ((algebraMap R S) r) = (algebraMap R A) r

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
r : R
⊢ (algebraMap S A) ((algebraMap R S) r) = (algebraMap R A) r
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
h : t ≤ f.rangeS
⊢ map f (comap f t) = t

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
h : t ≤ f.rangeS
⊢ map f (comap f t) = t
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
g : S →+* T
f : R →+* S
⊢ Subring.map g f.range = (g.comp f).range

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
g : S →+* T
f : R →+* S
⊢ Subring.map g (Subring.map f ⊤) = Subring.map (g.comp f) ⊤
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p : M
hp : ¬IsUnit p
⊢ Irreducible p ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : Monoid M
p : M
hp : ¬IsUnit p
⊢ (∀ ⦃a b : M⦄, p = a * b → IsUnit a ∨ IsUnit b) ∨ ∃ a, ¬IsUnit a ∧ ∃ x, ¬IsUnit x ∧ p = a * x
Module: Mathlib.Algebra.Group.Irreducible.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a b : M
inst✝ : Subsingleton Mˣ
hab : Irreducible (a * b)
⊢ a = 1 ∨ b = 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
a b : M
inst✝ : Subsingleton Mˣ
hab : Irreducible (a * b)
⊢ a = 1 ∨ b = 1
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mul.add_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ (x✝ + y✝) * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa using

Goal state after:
case mul.add_left
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * z✝ + y✝ * z✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)