mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.ULift

Goal state before:
pp: R : Type u
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : ULift M₀
⊢ Equiv.ulift (x✝ * 0) = Equiv.ulift 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Distrib R
x✝² x✝¹ x✝ : ULift R
⊢ Equiv.ulift (x✝² * (x✝¹ + x✝)) = Equiv.ulift (x✝² * x✝¹ + x✝² * x✝)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Distrib R
x✝² x✝¹ x✝ : ULift R
⊢ Equiv.ulift ((x✝² + x✝¹) * x✝) = Equiv.ulift (x✝² * x✝ + x✝¹ * x✝)

Tactic:
by

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map f p ≤ map (a • f) p

Tactic:
by

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
by

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
by

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✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : p ≤ q
x : ↥(comap q.subtype p)
⊢ (fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨↑↑x, ⋯⟩) x) = x

Tactic:
by

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✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : p ≤ q
x : ↥p
⊢ (fun x ↦ ⟨↑↑x, ⋯⟩) ((fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) x) = x

Tactic:
by

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₂
x : M₂
hx : e.symm x ∈ p
⊢ ↑e (e.symm x) = x

Tactic:
by

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₂
x : M₂
⊢ x ∈ map (↑e) p ↔ e.symm x ∈ p

Tactic:
by

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 τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ x✝ ∈ map (↑e) K ↔ x✝ ∈ comap (↑e.symm) K

Tactic:
by

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₂
⊢ map (↑e.symm) K = p ↔ map (↑e) p = K

Tactic:
by

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₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q

Tactic:
by

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✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ comap f q ≤ comap (c • f) q

Tactic:
by

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✝⁵ : 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 (c • f) p ≤ map f p

Tactic:
by

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ₗ}
⊢ f₁ + f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
by

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₂
⊢ 0 ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
by

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₂
c : S
fₗ : N →ₗ[S] N₂
h : fₗ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ c • fₗ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
by

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₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective ⇑f
y : ↥q
⊢ ∃ a, (f.submoduleComap q) a = y

Tactic:
by

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

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

Goal state after:
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 z : R
hx : x ∈ s
hy : -y ∈ s
hz : z ∈ s
⊢ x * -y * z ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
s : S
⊢ ∀ (x y : ↥s), ↑(x + y) = ↑x + ↑y

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝⁵ : NonUnitalNonAssocSemiring R✝
inst✝⁴ : SetLike S R✝
inst✝³ : NonUnitalSubsemiringClass S R✝
s : S
R : Type ?u.15
inst✝² : NonUnitalNonAssocCommSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), ↑(x + y) = ↑x + ↑y

Tactic:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝⁵ : NonUnitalNonAssocSemiring R✝
inst✝⁴ : SetLike S R✝
inst✝³ : NonUnitalSubsemiringClass S R✝
s : S
R : Type ?u.15
inst✝² : NonUnitalSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), ↑(x + y) = ↑x + ↑y

Tactic:
by

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₂
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:
by

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

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
inst✝⁵ : NonUnitalNonAssocSemiring R✝
inst✝⁴ : SetLike S R✝
inst✝³ : NonUnitalSubsemiringClass S R✝
s : S
R : Type ?u.15
inst✝² : NonUnitalCommSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), ↑(x + y) = ↑x + ↑y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
x✝ t : NonUnitalSubsemiring R
s : AddSubmonoid R
hs : ∀ {a b : R}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
⊢ { toAddSubmonoid := s, mul_mem' := hs }.toAddSubmonoid = t.toAddSubmonoid →
    { toAddSubmonoid := s, mul_mem' := hs } = t

Tactic:
by

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₂
inst✝ : RingHomSurjective σ₁₂
p : Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : InjOn ⇑f ↑p
⊢ Injective ⇑(f.submoduleMap p)

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s

Tactic:
by

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
inst✝ : RingHomSurjective σ₂₁
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ (c : M₂), f c ∈ p
p' : Submodule R₂ M₂
x✝ : ↥p
x : M
hx : x ∈ p
⊢ ⟨x, hx⟩ ∈ map (codRestrict p f h) p' ↔ ⟨x, hx⟩ ∈ comap p.subtype (map f p')

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈ s

Tactic:
by

Goal state after:
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
s : S
inst✝ : AddSubmonoidWithOneClass S R
n : ℕ
⊢ ↑n ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a * b ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : NonUnitalSubsemiring R
⊢ S.toAddSubmonoid = ⊤ ↔ S = ⊤

Tactic:
by

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

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ + b✝ ∈ {0}

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
x✝ : ↥s
⊢ ∀ ⦃a₂ : ↥s⦄, (subtype s) x✝ = (subtype s) a₂ → x✝ = a₂

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ * b✝ ∈ {0}

Tactic:
by

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
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
⊢ x ∈ comap f (map p.subtype p') → x ∈ comap (codRestrict p f hf) p'

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
p q : Subsemiring R
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 1 ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈ s → y ∈ s → x + y ∈ s

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈ s

Tactic:
by

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 (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p'))

Tactic:
by

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
x : ↥p
⊢ ↑x ∈ ↑p ∧ ↑e ↑x = ((↑e).domRestrict p) x

Tactic:
by

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 : ↥(Submodule.map (↑e) p)
⊢ ↑e.symm ↑y ∈ p

Tactic:
by

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
x : ↥p
⊢ (fun y ↦ ⟨↑e.symm ↑y, ⋯⟩) ((LinearMap.codRestrict (Submodule.map (↑e) p) ((↑e).domRestrict p) ⋯).toFun x) = x

Tactic:
by

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 : ↥(Submodule.map (↑e) p)
⊢ (LinearMap.codRestrict (Submodule.map (↑e) p) ((↑e).domRestrict p) ⋯).toFun ((fun y ↦ ⟨↑e.symm ↑y, ⋯⟩) y) = y

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : NonUnitalNonAssocRing R
p q : NonUnitalSubring R
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝) = ↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)) = -↑(x✝ + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).1 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).2 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : SetLike S R
hSR : SubringClass S R
s : S
n : ℤ
⊢ ↑n ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
x✝ t : Subring R
s : Subsemiring R
hs : ∀ {x : R}, x ∈ s.carrier → -x ∈ s.carrier
⊢ { toSubsemiring := s, neg_mem' := hs }.toSubsemiring = t.toSubsemiring → { toSubsemiring := s, neg_mem' := hs } = t

Tactic:
by

Goal state after:
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
⊢ -x✝ ∈ s.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toNonUnitalSubring.toSubring ⋯ = S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ (S.toSubring h1).toNonUnitalSubring = S

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
s : Set M₀
⊢ 0 ∈ s.centralizer

Tactic:
by

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ center G₀ˣ ⊆ Units.val ⁻¹' center G₀

Tactic:
by

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

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

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

Tactic:
by

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

Goal state after:
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
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ Commute (↑n) x✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
⊢ x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
by

Goal state after: