mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ restrictScalars S (sInf s) = sInf (restrictScalars S '' s)

Tactic:
ext

Goal state after:
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)
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
⊢ restrictScalars S (iInf s) = ⨅ i, restrictScalars S (s i)

Tactic:
ext

Goal state after:
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)
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₂'
⊢ e.conj (e.symm.conj f) = f

Tactic:
ext

Goal state after:
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✝
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₁'
⊢ e.symm.conj (e.conj f) = f

Tactic:
ext

Goal state after:
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✝
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₂'
⊢ e.conj LinearMap.id = LinearMap.id

Tactic:
ext

Goal state after:
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✝
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₂
⊢ f.domRestrict f.ker = 0

Tactic:
ext

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₂
f : M →ₛₗ[τ₁₂] M₂
x✝ : ↥f.ker
⊢ (f.domRestrict f.ker) x✝ = 0 x✝
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
⊢ (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 := ⋯ }) =
    1

Tactic:
ext

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
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✝
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✝¹ x✝ : Aˣ
⊢ (let __spread.0 := (x✝¹ * x✝).mulLeft;
    let __spread.1 := LinearMap.mulLeft R ↑(x✝¹ * x✝);
    { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
      right_inv := ⋯ }) =
    (let __spread.0 := x✝¹.mulLeft;
      let __spread.1 := LinearMap.mulLeft R ↑x✝¹;
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ }) *
      let __spread.0 := x✝.mulLeft;
      let __spread.1 := LinearMap.mulLeft R ↑x✝;
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ }

Tactic:
ext

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
R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
x✝² x✝¹ : Aˣ
x✝ : A
⊢ (let __spread.0 := (x✝² * x✝¹).mulLeft;
      let __spread.1 := LinearMap.mulLeft R ↑(x✝² * x✝¹);
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ })
      x✝ =
    ((let __spread.0 := x✝².mulLeft;
        let __spread.1 := LinearMap.mulLeft R ↑x✝²;
        { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
          right_inv := ⋯ }) *
        let __spread.0 := x✝¹.mulLeft;
        let __spread.1 := LinearMap.mulLeft R ↑x✝¹;
        { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
          right_inv := ⋯ })
      x✝
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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ (f.submoduleMap p).ker = comap p.subtype f.ker

Tactic:
ext

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

Tactic:
ext

Goal state after:
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
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✝ : IsScalarTower R A A
a b : Aˣ
⊢ mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b = mulRightLinearEquiv R (a * b)

Tactic:
ext

Goal state after:
R : Type u_9
A : Type u_10
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a b : Aˣ
x✝ : A
⊢ (mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b) x✝ = (mulRightLinearEquiv R (a * b)) x✝
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₂
⊢ comap f (⨅ i, p i) = ⨅ i, comap f (p i)

Tactic:
ext

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ (c • 0).down = down 0
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift.{?u.13, v} M
⊢ c • (f + g) = c • f + c • g

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift.{?u.13, v} M
⊢ (c • (f + g)).down = (c • f + c • g).down
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
x✝ : R
⊢ x✝ • 1 = 1

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
x✝ : R
⊢ (x✝ • 1).down = down 1
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
x✝² : R
x✝¹ x✝ : ULift.{?u.15, v} M
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
x✝² : R
x✝¹ x✝ : ULift.{?u.15, v} M
⊢ (x✝² • (x✝¹ * x✝)).down = (x✝² • x✝¹ * x✝² • x✝).down
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₂
⊢ comap (-f) p = comap f p

Tactic:
ext

Goal state after:
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
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) → e.symm x ∈ p

case mpr
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₂
⊢ e.symm x ∈ p → ∃ y ∈ p, ↑e y = x
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:
obtain ⟨x, hx⟩ := hf y
  use ⟨x, Submodule.mem_comap.mpr (hx ▸ y.2)⟩
  apply Subtype.val_injective
  simp [hx]

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

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

case snd
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝).2 = (↑x✝).2
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:
ext

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

case snd
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑(Int.negSucc x✝), ↑(Int.negSucc x✝)).2 = (-↑(x✝ + 1)).2
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✝) = -x✝¹ * x✝ + -↑n * x✝¹ * x✝

Tactic:
add_right_inj,

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 : ℕ
⊢ -(x✝¹ * x✝) + -(x✝¹ * x✝ * ↑n) = -(x✝¹ * x✝) + x✝¹ * (x✝ * -↑n)

Tactic:
add_right_inj,

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

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * (x✝ * ↑n)) = x✝¹ * (x✝ * -↑n)
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✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
ext

Goal state after:
case fst
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² * (x✝¹ + x✝)).1 = (x✝² * x✝¹ + x✝² * x✝).1

case snd
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² * (x✝¹ + x✝)).2 = (x✝² * x✝¹ + x✝² * x✝).2
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✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
ext

Goal state after:
case fst
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ ((x✝² + x✝¹) * x✝).1 = (x✝² * x✝ + x✝¹ * x✝).1

case snd
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ ((x✝² + x✝¹) * x✝).2 = (x✝² * x✝ + x✝¹ * x✝).2
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mp
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
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor

Goal state after:
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
⊢ map (fst M N) u ≤ s

case mp.right
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
⊢ map (snd M N) u ≤ t
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
⊢ srange f = map f ⊤

Tactic:
ext

Goal state after:
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 ⊤
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
⊢ M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure ↑M

Tactic:
ext

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
⊢ x✝ ∈ M.nonUnitalSubsemiringClosure ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

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

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
x✝ : S
⊢ x✝ ∈ f.range ↔ x✝ ∈ NonUnitalSubring.map f ⊤
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
⊢ f.rangeS = Subsemiring.map f ⊤

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.rangeS ↔ x✝ ∈ Subsemiring.map f ⊤
Module: Mathlib.Algebra.Algebra.Basic

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

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
r✝ : ℕ
⊢ (algebraMap ℕ R) r✝ = (algebraMap ℕ R) r✝
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
⊢ ⇑(algebraMap R A) ∘ Nat.cast = Nat.cast

Tactic:
ext

Goal state after:
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✝
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
⊢ ⇑(algebraMap R A) ∘ Int.cast = Int.cast

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure = Subsemiring.closure ↑M

Tactic:
ext

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ x✝ ∈ M.subsemiringClosure ↔ x✝ ∈ Subsemiring.closure ↑M
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 : ℕ
⊢ ⇑(φ ^ Nat.zero) = (⇑φ)^[Nat.zero]

Tactic:
ext

Goal state after:
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✝
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✝ : ℕ
ih : ⇑(φ ^ x✝) = (⇑φ)^[x✝]
⊢ ⇑(φ ^ x✝.succ) = (⇑φ)^[x✝.succ]

Tactic:
ext

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : A →ₐ[R] A
n x✝¹ : ℕ
ih : ⇑(φ ^ x✝¹) = (⇑φ)^[x✝¹]
x✝ : A
⊢ (φ ^ x✝¹.succ) x✝ = (⇑φ)^[x✝¹.succ] x✝
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
φ : A →ₐ[R] B
⊢ φ.comp (ofId R A) = ofId R B

Tactic:
ext

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

Goal state after:
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✝)
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:
ext

Goal state after:
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✝
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 →ₐ[R] A
⊢ x✝ • 1 = 1

Tactic:
ext

Goal state after:
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 →ₐ[R] A
⊢ ↑(x✝ • 1) = ↑1