mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
x : M
⊢ x ∈ ker 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
hf : Injective ⇑f
x : M
hx : x ∈ f.ker
⊢ x ∈ ⊥

Tactic:
simpa only [mem_ker, mem_bot, ← map_zero f, hf.eq_iff] using hx

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

Goal state before:
pp: R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
u v : Aˣ
x : A
⊢ ((mulLeftLinearEquiv R A) (u * v)) x = ((mulLeftLinearEquiv R A) u) (((mulLeftLinearEquiv R A) v) x)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ (inclusion h).ker = ⊥

Tactic:
inclusion,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ (codRestrict p' p.subtype ⋯).ker = ⊥
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
⊢ a ∈ map LinearMap.id p ↔ a ∈ p

Tactic:
by simp

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : p ≤ comap (f ^ k) p
⊢ p ≤ comap (f ^ (k + 1)) p

Tactic:
| succ k ih =>

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₂
⊢ ∀ (x : M), x ∈ comap 0 q ↔ x ∈ ⊤

Tactic:
by simp

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
inst✝² : RingHomSurjective σ₁₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ map (↑e) p ≠ ⊥ ↔ p ≠ ⊥

Tactic:
by simp

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
inst✝² : RingHomSurjective σ₁₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ map (↑e) p ≠ ⊤ ↔ p ≠ ⊤

Tactic:
by simp

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

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

Tactic:
by simp

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

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 simp

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 simp

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 simp

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 simp

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 simp

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:
intro ⟨x, hx⟩ ⟨y, hy⟩ hxy

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⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
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 simp

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 simp

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 simp

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

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

Tactic:
neg_mul,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(1 * (x✝¹ * x✝)) + -↑n * (x✝¹ * x✝) = -1 * x✝¹ * x✝ + -↑n * x✝¹ * x✝
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:
neg_mul,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n * (x✝¹ * x✝)) = -↑n * x✝¹ * x✝
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:
neg_mul,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n * x✝¹ * x✝) = -(↑n * x✝¹) * x✝
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:
neg_mul,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(a * (x✝¹ * x✝)) = -a * x✝¹ * x✝
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:
neg_mul,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(a * x✝¹ * x✝) = -(a * x✝¹) * x✝
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R), (x * y, 0) = (x, 0) * (y, 0)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R), (x + y, 0) = (x, 0) + (y, 0)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R), (0, x * y) = (0, x) * (0, y)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
⊢ ∀ (x y : R), (0, x + y) = (0, x) + (0, y)

Tactic:
by simp

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

Goal state before:
pp: P : Type u_3
inst✝ : Mul P
S : Subsemigroup P
⊢ ∀ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S

Tactic:
by simp

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 : Set (NonUnitalSubsemiring R)
⊢ ↑(⨅ t ∈ s, t.toSubsemigroup) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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 : Set (NonUnitalSubsemiring R)
⊢ ↑(⨅ t ∈ s, t.toAddSubmonoid) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set (NonUnitalSubring R)
⊢ ↑(⨅ t ∈ s, t.toSubsemigroup) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set (NonUnitalSubring R)
⊢ ↑(⨅ t ∈ s, t.toAddSubgroup) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
M : Type u_3
R : Type u_4
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
z : ℕ
⊢ (algebraMap R A) ↑(Int.negSucc z) = -↑(z + 1)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set (Subsemiring R)
⊢ ↑(⨅ t ∈ s, t.toSubmonoid) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set (Subsemiring R)
⊢ ↑(⨅ t ∈ s, t.toAddSubmonoid) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
⊢ (algebraMap R A) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
⊢ ∀ (x y : R), (algebraMap R A) (x * y) = (algebraMap R A) x * (algebraMap R A) y

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsCancelMulZero A
⊢ (algebraMap R A) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsCancelMulZero A
⊢ ∀ (x y : R), (algebraMap R A) (x * y) = (algebraMap R A) x * (algebraMap R A) y

Tactic:
by simp

Goal state after:
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) (m : M), (algebraMap R A) r • m = r • m

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ f ((algebraMap ℕ R) n) = (algebraMap ℕ S) n

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
n : ℤ
⊢ (↑↑f).toFun ((algebraMap ℤ R) n) = (algebraMap ℤ S) n

Tactic:
by simp

Goal state after:
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
s : Set (Subring R)
⊢ ↑(⨅ t ∈ s, t.toSubmonoid) = ⋂ t ∈ s, ↑t

Tactic:
by simp

Goal state after:
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
s : Set (Subring R)
⊢ ↑(⨅ t ∈ s, t.toAddSubgroup) = ⋂ t ∈ s, ↑t

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
L : List (List R)
hL : (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ (List.map List.prod (List.map (List.cons (-1)) [])).sum = -(List.map List.prod []).sum

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
x✝ : 0 ≠ 1
⊢ ¬Irreducible (x ^ 0)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
⊢ Irreducible (y * ↑u) ↔ Irreducible y

Tactic:
simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]

Goal state after:
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
⊢ ¬IsUnit y → ((∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b) ↔ ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
a : M
⊢ e.symm (e a) = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
h : Prime p
a : N
⊢ e (e.symm a) = a

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
ih : p ^ n ∣ a * b → p ^ n ∣ b
h' : p ^ (n + 1) ∣ a * b
⊢ p ^ (n + 1) ∣ b

Tactic:
obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')

Goal state after:
case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
hp : Prime p
h : ¬p ∣ a
n : ℕ
c : M
ih : p ^ n ∣ a * (p ^ n * c) → p ^ n ∣ p ^ n * c
h' : p ^ (n + 1) ∣ a * (p ^ n * c)
⊢ p ^ (n + 1) ∣ p ^ n * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ x * ↑1 = x

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * ↑u * ↑u⁻¹ = x

Tactic:
rw [mul_assoc, Units.mul_inv, mul_one]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ 1 ∈ {x | ∀ (y : M₀), x * y = 0 → y = 0}

Tactic:
by simp

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ 1 ∈ {x | ∀ (y : M₀), y * x = 0 → y = 0}

Tactic:
by simp

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

Goal state before:
pp: N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ u * a ~ᵤ a

Tactic:
by
  rw [mul_comm]
  exact associated_mul_unit_left _ _ hu

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), q ∣ a * b → q ∣ a ∨ q ∣ b

Tactic:
rw [← hu]
      simp only [Units.isUnit, IsUnit.mul_right_dvd]
      intro a b
      exact hp.dvd_or_dvd

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
obtain (h | h) := hx.isUnit_or_isUnit hz

Goal state after:
case mp.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit y
⊢ IsUnit y ∨ x ~ᵤ y

case mp.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ x ~ᵤ y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ p = p * ↑u * ↑u⁻¹

Tactic:
by simp

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

Goal state before:
pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0

Tactic:
mul_comm a b,

Goal state after:
case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (b * a) = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
x : G₀
u : G₀ˣ
⊢ (fun u ↦ Units.mk0 ↑u ⋯) ((fun u ↦ ⟨↑u, ⋯⟩) u) = u

Tactic:
by simp

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

Goal state before:
pp: G₀ : Type u_1
inst✝ : GroupWithZero G₀
x : G₀
u v : ↥G₀⁰
⊢ Units.mk0 ↑(u * v) ⋯ = Units.mk0 ↑u ⋯ * Units.mk0 ↑v ⋯

Tactic:
by simp

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

Goal state before:
pp: M₀ : Type ?u.3
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ ⟨↑u, ⋯⟩ * ⟨↑u⁻¹, ⋯⟩ = 1

Tactic:
by simp

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

Goal state before:
pp: M₀ : Type ?u.3
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ ⟨↑u⁻¹, ⋯⟩ * ⟨↑u, ⋯⟩ = 1

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
refine Iff.rfl.and ?_

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ x, ¬IsUnit x ∧ b = a * x
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ comap f ⊥ = ⊤ ↔ f = 0

Tactic:
exact ker_eq_top

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

Goal state before:
pp: case h
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : f.ker ≤ p
⊢ 0 ∈ ↑f.range ∧ ⇑f ⁻¹' {0} ⊆ ↑p

Tactic:
coe_range

Goal state after:
case h
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
h : f.ker ≤ p
⊢ 0 ∈ Set.range ⇑f ∧ ⇑f ⁻¹' {0} ⊆ ↑p
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Semiring T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
f : S →ₐ[R] T
x✝ : ULift.{u₂, u_1} R
⊢ (↑↑((↑ULift.algEquiv.{u_1, u_3, u₃}.symm).comp (f.comp ↑ULift.algEquiv.{u_1, u_2, u₁})).toRingHom).toFun
      ((algebraMap (ULift.{u₂, u_1} R) (ULift.{u₁, u_2} S)) x✝) =
    (algebraMap (ULift.{u₂, u_1} R) (ULift.{u₃, u_3} T)) x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ map p.subtype ⊤ = p

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ map (inclusion h) ⊤ = comap q.subtype p

Tactic:
inclusion,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ map (codRestrict q p.subtype ⋯) ⊤ = comap q.subtype p