mathlib-initiative/mathlib-tactics huggingface dataset:
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
p p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ∧ x ∈ p' → x ∈ {0}) ↔ ∀ x ∈ p, x ∈ p' → x = 0

Tactic:
simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s : Set (Submodule R M)
x✝ : M
⊢ x✝ ∈ restrictScalars S (sInf s) ↔ x✝ ∈ sInf (restrictScalars S '' s)

Tactic:
simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
ι : Sort u_4
s : ι → Submodule R M
x✝ : M
⊢ x✝ ∈ restrictScalars S (iInf s) ↔ x✝ ∈ ⨅ i, restrictScalars S (s i)

Tactic:
simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s t : Submodule R M
x : M
⊢ x ∈ restrictScalars S (s ⊓ t) ↔ x ∈ restrictScalars S s ⊓ restrictScalars S t

Tactic:
simp

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

Goal state before:
pp: R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst✝⁷ : CommSemiring R₁'
inst✝⁶ : CommSemiring 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₂'
f : Module.End R₂' M₂'
x✝ : M₂'
⊢ (e.conj (e.symm.conj f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst✝⁷ : CommSemiring R₁'
inst✝⁶ : CommSemiring 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₂'
f : Module.End R₁' M₁'
x✝ : M₁'
⊢ (e.symm.conj (e.conj f)) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst✝⁷ : CommSemiring R₁'
inst✝⁶ : CommSemiring 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₂'
x✝ : M₂'
⊢ (e.conj LinearMap.id) x✝ = LinearMap.id x✝

Tactic:
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₂
x : M
⊢ x ∈ ker 0

Tactic:
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₂
x✝ : ↥f.ker
⊢ (f.domRestrict f.ker) x✝ = 0 x✝

Tactic:
simp

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
R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
x✝ : A
⊢ (let __spread.0 := mulLeft 1;
      let __spread.1 := LinearMap.mulLeft R ↑1;
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ })
      x✝ =
    1 x✝

Tactic:
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✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x✝ : M
⊢ x✝ ∈ (-f).ker ↔ x✝ ∈ f.ker

Tactic:
simp

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:
simp

Goal state after:
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:
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₂
ι : Sort u_9
f : M →ₛₗ[σ₁₂] M₂
p : ι → Submodule R₂ M₂
x✝ : M
⊢ x✝ ∈ comap f (⨅ i, p i) ↔ x✝ ∈ ⨅ i, comap f (p i)

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

Tactic:
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:
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:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
f : M →ₗ[R] M₂
p : Submodule R M₂
x✝ : M
⊢ x✝ ∈ comap (-f) p ↔ x✝ ∈ comap f p

Tactic:
simp

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
⊢ comap (a • f) p = comap f p

Tactic:
ext b

Goal state after:
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
b : V
⊢ b ∈ comap (a • f) p ↔ b ∈ comap f p
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:
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:
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:
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:
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:
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:
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:
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✝² : NonUnitalNonAssocCommSemiring R
inst✝¹ : SetLike S R
inst✝ : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), ↑(x + y) = ↑x + ↑y

Tactic:
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:
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:
simp

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:
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✝² : 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:
simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
        LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, SetLike.eta]

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Tactic:
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:
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:
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:
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:
simp

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
⊢ (0, 1) * (1, 0) = 0

Tactic:
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:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x✝ : S
⊢ x✝ ∈ srange f ↔ x✝ ∈ map f ⊤

Tactic:
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:
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:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ NonUnitalSubring.map f ⊤

Tactic:
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:
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:
simp

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

Goal state before:
pp: case zero
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) ^ 0 = (x - (algebraMap R A) r) ^ 0 * x

Tactic:
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:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.rangeS ↔ x✝ ∈ Subsemiring.map f ⊤

Tactic:
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:
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:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
r✝ : ℕ
⊢ (algebraMap ℕ R) r✝ = (algebraMap ℕ R) r✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : ℕ
⊢ (⇑(algebraMap R A) ∘ Nat.cast) x✝ = ↑x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x✝ : ℤ
⊢ (⇑(algebraMap R A) ∘ Int.cast) x✝ = ↑x✝

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
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:
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:
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:
simp

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
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ f 1 = 1

Tactic:
hf

Goal state after:
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
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ 1 = 1
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n : ℕ
x✝ : A
⊢ (φ ^ Nat.zero) x✝ = (⇑φ)^[Nat.zero] x✝

Tactic:
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:
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:
simp

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

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M →ₗ[R] N
x : M
r : R
⊢ f.toFun ((algebraMap R S) r • x) = (RingHom.id S) ((algebraMap R S) r) • f.toFun x

Tactic:
simp

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

Goal state before:
pp: R : Type ?u.4
S : Type ?u.6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
M : Type ?u.13
N : Type ?u.15
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
h : Surjective ⇑(algebraMap R S)
f : M ≃ₗ[R] N
x : M
r : R
⊢ (↑f).toFun ((algebraMap R S) r • x) = (RingHom.id S) ((algebraMap R S) r) • (↑f).toFun x

Tactic:
simp

Goal state after: