mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = 1 • SMul.smul n a

Tactic:
rfl

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

Goal state before:
pp: M : Type uM
inst✝ : AddCommGroup M
⊢ instRing.toAddCommGroup.toSubNegMonoid = instRing.toAddGroupWithOne.toAddGroup.toSubNegMonoid

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ f (DomMulAct.mk.symm (s + s') • m) = f ((DomMulAct.mk.symm s + DomMulAct.mk.symm s') • m)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ : R →+* S
r : R
x : M
inst✝ : RingHomId (RingHom.id R)
⊢ r • x = (RingHom.id R) r • x

Tactic:
rfl

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

Goal state before:
pp: case refl
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M✝ : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝³ : Semiring R
inst✝² : Semiring S
ι : Type u_14
M : ι → Type u_15
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x✝¹ : R
x✝ : M i
__AddEquiv✝ : M i ≃+ M i := AddEquiv.cast ⋯
⊢ (AddEquiv.cast ⋯).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (AddEquiv.cast ⋯).toFun x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (m : R₁) (x : M), (⇑f + ⇑g) (m • x) = σ₁₂ m • (⇑f + ⇑g) x

Tactic:
by simp [smul_add]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x✝ : M
⊢ (toAddMonoidHom 0) x✝ = 0 x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x✝¹ y✝ : M →ₛₗ[σ₁₂] M₂
x✝ : M
⊢ (x✝¹ + y✝).toAddMonoidHom x✝ = (x✝¹.toAddMonoidHom + y✝.toAddMonoidHom) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
X : Type u_5
inst✝¹ : SMul M X
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝² : SMul M X
inst✝¹ : AddZeroClass Y
inst✝ : DistribSMul N Y
f g : X →ₑ[σ] Y
⊢ ∀ (m : M) (x : X), (⇑f + ⇑g) (m • x) = σ m • (⇑f + ⇑g) x

Tactic:
by simp [smul_add]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = f (g 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
A : Type u_4
inst✝¹ : Monoid A
inst✝ : MulDistribMulAction M A
x : A
⊢ (MulDistribMulActionHom.id M) x = x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn.1 • mn.2 • a + mn.1 • mn.2 • a' = mn • a + mn • a'

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ x✝¹ (DomMulAct.mk.symm (x✝³ + x✝²) • x✝) = x✝¹ ((DomMulAct.mk.symm x✝³ + DomMulAct.mk.symm x✝²) • x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
| SMul.smul m a

Tactic:
← one_smul N a

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
| SMul.smul m (1 • a)
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4.e_5
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
| SMul.smul n a

Tactic:
rw [← one_smul M (SMul.smul n a)]

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
| 1 • SMul.smul n a
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = 1 • SMul.smul n a

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
⊢ f.smulRight (c • m) = (RingHom.id R) c • f.smulRight m

Tactic:
by
        ext
        apply smul_comm

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

Goal state before:
pp: a✝ : PUnit
⊢ 0 * a✝ = 0

Tactic:
rfl

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

Goal state before:
pp: a✝ : PUnit
⊢ a✝ * 0 = 0

Tactic:
rfl

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

Goal state before:
pp: a✝ b✝ c✝ : PUnit
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝

Tactic:
rfl

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

Goal state before:
pp: a✝ b✝ c✝ : PUnit
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i

Tactic:
rfl

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

Goal state before:
pp: case e'_2
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ e (c • a) = e.toAddMonoidHom (c • a)

pp: case e'_3
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ c • e a = c • e.toAddMonoidHom a

Tactic:
· exact congr(e $(int_smul_eq_zsmul ..))

Goal state after:
case e'_3
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ c • e a = c • e.toAddMonoidHom a
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
x✝ : M
⊢ ↑e.toIntLinearEquiv x✝ = e x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
have := le_sSup hs
  rw [LE.le] at this
  exact this

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : 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₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Subsingleton R
inst✝ : Subsingleton R₂
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)

Tactic:
haveI := Module.subsingleton R M

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : 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₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Subsingleton R
inst✝ : Subsingleton R₂
this : Subsingleton M
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p q : Submodule R M
inst✝ : Subsingleton R
⊢ Unique (Submodule R M)

Tactic:
haveI := Module.subsingleton R M

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p q : Submodule R M
inst✝ : Subsingleton R
this : Subsingleton M
⊢ Unique (Submodule R M)
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
h' : ∀ x ∈ p, (f' ^ n) x ∈ p
x : ↥p
this : Semiconj Subtype.val ⇑(f'.restrict h) ⇑f'
⊢ ↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)

Tactic:
simp [Module.End.coe_pow, this.iterate_right _ _]

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₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ ∀ (a : M) (b : a ∈ N), (f ∘ₛₗ N.subtype) ⟨a, b⟩ = 0 ⟨a, b⟩

Tactic:
rfl

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₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap f (map p.subtype ⊥) = f.ker

Tactic:
Submodule.map_bot

Goal state after:
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₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap f ⊥ = f.ker
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₂
p : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ comap f ⊥ = f.ker

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
x y : ULift α
inst✝ : MulOneClass α
x✝ y✝ : ULift α
⊢ Equiv.ulift (x✝ * y✝) = Equiv.ulift x✝ * Equiv.ulift y✝

Tactic:
rfl

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✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x✝ y✝ : ↥p
⊢ ⟨f ↑x✝ + f ↑y✝, ⋯⟩ = ⟨f ↑x✝, ⋯⟩ + ⟨f ↑y✝, ⋯⟩

Tactic:
rfl

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✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
m✝ : R
x✝ : ↥p
⊢ ⟨σ₁₂ m✝ • f ↑x✝, ⋯⟩ = σ₁₂ m✝ • ⟨f ↑x✝, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝ : MulZeroOneClass α
a✝ b✝ : ULift α
⊢ Equiv.ulift (a✝ * b✝) = Equiv.ulift a✝ * Equiv.ulift b✝

Tactic:
rfl

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

Goal state before:
pp: case pos
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 (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
simp [h, Submodule.map_smul]

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

Goal state before:
pp: case neg
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 (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
simp [h, Submodule.map_smul]

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

Goal state before:
pp: case mk
R : Type u
inst✝ : NonAssocRing R
toSubsemiring✝ : Subsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toSubsemiring✝.carrier → -x ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }.toNonUnitalSubring.toSubring ⋯ =
    { toSubsemiring := toSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
R : Type u
inst✝ : NonAssocRing R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }.toSubring h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
rfl

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:
rw [Int.cast_natCast, (natCast_mem_center _ n).right_assoc _ _]

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

Goal state before:
pp: case mp.left
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ (fst M N) (y1, y2) ∈ s

Tactic:
exact (h hy1).1

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ IsMulCentral 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:
isMulCentral_iff

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
S : Type v
T : Type w
inst✝¹ : NonUnitalNonAssocSemiring R✝
M : Subsemigroup R✝
R : Type u_1
inst✝ : NonUnitalSemiring R
⊢ (center.instNonUnitalCommSemiring R).toNonUnitalSemiring = NonUnitalSubsemiringClass.toNonUnitalSemiring (center R)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalRing R
⊢ (center.instNonUnitalCommRing R).toNonUnitalRing = NonUnitalSubringClass.toNonUnitalRing (center R)

Tactic:
rfl

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
R : Type u_1
inst✝ : Semiring R
⊢ center.commSemiring.toSemiring = (center R).toSemiring

Tactic:
rfl

Goal state after:
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 [isMulCommutative_iff, ← SetLike.mem_coe, NonUnitalSubsemiring.coe_iSup_of_directed dir,
    coe_iSup_of_directed dir] using NonUnitalSubsemiring.isMulCommutative_iSup dir

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
r : R
⊢ (↑↑(φ₁.comp ↑φ₂)).toFun ((algebraMap R A) r) = φ₁ (φ₂ ((algebraMap R A) r))

Tactic:
rfl

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝² x✝¹ : A →ₐ[R] A
x✝ : Aˣ
⊢ ↑((x✝² * x✝¹) • x✝) = ↑(x✝² • x✝¹ • x✝)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : Aˣ
⊢ ↑(1 • x✝) = ↑x✝

Tactic:
rfl

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✝
⊢ ∀ (head : List R) (tail : List (List R)),
    (List.map List.prod (List.map (List.cons (-1)) tail)).sum = -(List.map List.prod tail).sum →
      (List.map List.prod (List.map (List.cons (-1)) (head :: tail))).sum = -(List.map List.prod (head :: tail)).sum

Tactic:
simp +contextual [List.map_cons, add_comm]

Goal state after: