mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p

Tactic:
]

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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ e.symm x✝ ∈ K ↔ e.symm x✝ ∈ K

Tactic:
]

Goal state after:
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ comap (↑e.symm.symm) K = p ↔ map (↑e) p = K

Tactic:
]

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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ comap (↑e.symm.symm) K = p ↔ map (↑e) p = K
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✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ map f p ≤ map f p

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ

Tactic:
]

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s

Tactic:
]

Goal state after:
S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ 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₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ comap q.subtype (map f (map p.subtype p')) = comap q.subtype (map f (map p.subtype p'))

Tactic:
]

Goal state after:
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
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R ↥q
⊢ comap p.subtype (comap f (map q.subtype p')) = comap p.subtype (comap f (map q.subtype p'))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy✝ : y' ∈ Submodule.map (↑e) p
hy : ∃ y ∈ p, ↑e y = y'
⊢ ↑e.symm ↑⟨y', hy✝⟩ ∈ p

Tactic:
]

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy✝ : y' ∈ Submodule.map (↑e) p
hy : ∃ y ∈ p, ↑e y = y'
⊢ ↑e.symm ↑⟨y', hy✝⟩ ∈ p
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -1 * x✝ ∈ s.carrier

Tactic:
]

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x✝ : R
h : x✝ ∈ s.carrier
⊢ -1 * x✝ ∈ s.carrier
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 = 0

Tactic:
]

Goal state after:
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:
]

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ a * c = a * c

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ ↑n * x✝ = ↑n * x✝

Tactic:
]

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

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = 0

Tactic:
]

Goal state after:
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 * x✝¹ * x✝ + x✝¹ * x✝

Tactic:
]

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i

pp: case hS
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑x

Tactic:
]

Goal state after:
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i

case hS
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑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✝ = x✝¹ * (x✝ * ↑n) + x✝¹ * x✝

Tactic:
]

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

Goal state before:
pp: case hS
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (S ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) Subtype.val

Tactic:
]

Goal state after:
case hS
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (S ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) Subtype.val
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n : ℤ
x✝ : M
⊢ ↑n * x✝ = ↑n * x✝

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑n * x✝¹ * x✝ = ↑n * x✝¹ * x✝

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n * x✝¹ * x✝) = -(↑n * x✝¹ * x✝)

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * (x✝ * ↑n) = x✝¹ * (x✝ * ↑n)

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * (x✝ * ↑n)) = -(x✝¹ * (x✝ * ↑n))

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝ : M
⊢ x✝ * a + x✝ * b = x✝ * a + x✝ * b

Tactic:
]

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

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Tactic:
]

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ (a + b) * x✝¹ * x✝ = (a + b) * x✝¹ * x✝

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * (a + b)) = x✝¹ * (x✝ * (a + b))

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ a * -x✝ = a * -x✝

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(a * x✝¹ * x✝) = -(a * x✝¹ * x✝)

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * (x✝ * a)) = -(x✝¹ * (x✝ * a))

Tactic:
]

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

Goal state before:
pp: M : Type u_1
S : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
⊢ a * c + b * c = a * c + b * c

Tactic:
]

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

Goal state before:
pp: M : Type u_1
S : Set M
a : M
inst✝¹ : Mul M
inst✝ : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ -(a * c) = -(a * c)

Tactic:
]

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

Goal state before:
pp: R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f x * f y = f x * f y

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ

Tactic:
]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝¹ : Mul M
inst✝ : Mul N
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ⇑f
x : ↥f.srange
x' : M
hx' : f x' = ↑x
⊢ f x' = f x'

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ ((∀ (a_1 : R), Commute a a_1) ∧ (∀ (b c : R), a * (b * c) = a * b * c) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Tactic:
]

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ ((∀ (a_1 : R), Commute a a_1) ∧ (∀ (b c : R), a * (b * c) = a * b * c) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ z ∈ Set.center R

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ z ∈ Set.center R
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s

Tactic:
rintro - ⟨H, rfl⟩

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
⊢ x ∈ (fun t ↦ ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g ⇑f
x : ↥(srange f)
x' : R
hx' : f x' = ↑x
⊢ f x' = f x'

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
x : R
⊢ x = 0 ↔ x = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * x - (algebraMap R A) r * x = x * x - (algebraMap R A) r * x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
⊢ (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n * x =
    (x - (algebraMap R A) r) * (x - (algebraMap R A) r) ^ n * x

Tactic:
]

Goal state after:
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:
]

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'
⊢ ↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'
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:
]

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'
⊢ ↑h.unit m' = ↑h.unit (↑h.unit⁻¹ (x • m'))
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ r • f a = r • f a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ (algebraMap R B) r * f a = (algebraMap R B) r * f a

Tactic:
]

Goal state after:
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
⊢ (Injective fun r ↦ r • 1) ↔ Injective fun r ↦ r • 1

Tactic:
]

Goal state after:
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
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² x✝¹ : G
x✝ : R
⊢ x✝² • x✝¹ • (algebraMap R A) x✝ = x✝² • x✝¹ • (algebraMap R A) x✝

Tactic:
]

Goal state after:
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
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : R
⊢ (algebraMap R A) x✝ = (algebraMap R A) x✝

Tactic:
]

Goal state after:
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
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ 0 = 0

Tactic:
]

Goal state after:
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
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝) = (algebraMap R A) (x✝² • x✝¹ + x✝² • x✝)

Tactic:
]

Goal state after:
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
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ 1 = 1

Tactic:
]

Goal state after:
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
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝² : G
x✝¹ x✝ : R
⊢ x✝² • (algebraMap R A) x✝¹ * x✝² • (algebraMap R A) x✝ = x✝² • (algebraMap R A) x✝¹ * x✝² • (algebraMap R A) x✝

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s

Tactic:
rintro - ⟨H, rfl⟩

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
⊢ x ∈ (fun t ↦ ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ (algebraMap R A) r • m = (algebraMap R A) r • m

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
a : A
m : M
⊢ a • r • m = a • r • m

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹¹ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁰ : Semiring A✝
inst✝⁹ : Algebra R✝ A✝
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module A✝ M
inst✝⁶ : Module R✝ M
inst✝⁵ : IsScalarTower R✝ A✝ M
R : Type u_4
S : Type u_5
A : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Algebra S A
r : R
s : S
a : A
⊢ s • r • a = s • r • a

Tactic:
]

Goal state after: