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

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f : Equidecomp X G
x : X
h : x ∈ f.source
⊢ ↑f.symm (↑f.toPartialEquiv x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f : Equidecomp X G
x : X
h : x ∈ f.target
⊢ ↑f.toPartialEquiv (↑f.symm x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
⊢ IsIntegrallyClosed S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝¹ x✝ : ℍ[R,c₁,c₃]
⊢ { re := (x✝¹ + x✝).re, imI := (x✝¹ + x✝).imJ, imJ := (x✝¹ + x✝).imI, imK := -(x✝¹ + x✝).imK } =
    { re := x✝¹.re, imI := x✝¹.imJ, imJ := x✝¹.imI, imK := -x✝¹.imK } +
      { re := x✝.re, imI := x✝.imJ, imJ := x✝.imI, imK := -x✝.imK }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x✝ : R
⊢ { re := ((algebraMap R ℍ[R,c₁,c₃]) x✝).re, imI := ((algebraMap R ℍ[R,c₁,c₃]) x✝).imJ,
      imJ := ((algebraMap R ℍ[R,c₁,c₃]) x✝).imI, imK := -((algebraMap R ℍ[R,c₁,c₃]) x✝).imK } =
    (algebraMap R ℍ[R,c₃,c₁]) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a * ↑r = r • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ x • ↑y = ↑(x * y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x : ℍ[R,c₁,c₂,c₃]
⊢ star (star x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a✝ b✝ : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a * b) = star b * star a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a✝ b✝ : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ star (a + b) = star a + star b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = ↑(2 * a.re + c₂ * a.imI)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = ↑(2 * a.re + c₂ * a.imI)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ↑r * x = x * ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ Commute (star a) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ star ↑x = ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a.im = -a.im + ↑c₂ * ↑a.imI

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
R : Type u_3
c₁ c₂ c₃ : R
inst✝³ : CommRing R
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : SMulCommClass S R R
s : S
a : ℍ[R,c₁,c₂,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
R : Type u_3
c₁ c₃ : R
inst✝² : CommRing R
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
s : S
a : ℍ[R,c₁,c₃]
⊢ (star (s • a)).re = (s • star a).re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
a : ℍ[R,c₁,c₂,c₃]
x : R
h : a = ↑x
⊢ a = ↑a.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₃ : R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ c₂ : R
a : ℍ[R,c₁,c₂,c₃]
⊢ star a = a ↔ a = ↑a.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₃ : R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ : R
a : ℍ[R,c₁,c₃]
⊢ star a = -a ↔ a.re = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x✝ : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
x : Option α
⊢ (a • b) • x = a • b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x✝ : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
x : Option α
⊢ MulOpposite.op a • x = a • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : SMul M α
inst✝¹ : SMul N α
a : M
b✝ : α
x : Option α
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : Option α), m₁✝ • a = m₂✝ • a
b : α
⊢ m₁✝ • b = m₂✝ • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
a₁ a₂ : M
b : Option α
⊢ (a₁ * a₂) • b = a₁ • a₂ • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
b : Option α
⊢ 1 • b = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a * a = ↑(star a * a).re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ (a • b) • x = a • b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a * star a = ↑(a * star a).re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y✝ : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
x y : ℍ[R,c₁,c₂,c₃]
⊢ (op ∘ star) (x * y) = (op ∘ star) x * (op ∘ star) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r✝ x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
r : R
⊢ (op ∘ star) ((algebraMap R ℍ[R,c₁,c₂,c₃]) r) = (algebraMap R ℍ[R,c₁,c₂,c₃]ᵐᵒᵖ) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ + 0 * -1 * a.imJ * b.imK - -1 * -1 * a.imK * b.imK =
    a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x✝ : (i : ι) × α i
inst✝ : ∀ (i : ι), SMulCommClass M N (α i)
a : M
b : N
x : (i : ι) × α i
⊢ a • b • x = b • a • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imI + a.imI * b.re + 0 * a.imI * b.imI - -1 * a.imJ * b.imK + -1 * a.imK * b.imJ =
    a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b : α i
x✝ : (i : ι) × α i
inst✝¹ : (i : ι) → SMul Mᵐᵒᵖ (α i)
inst✝ : ∀ (i : ι), IsCentralScalar M (α i)
a : M
x : (i : ι) × α i
⊢ MulOpposite.op a • x = a • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imJ + -1 * a.imI * b.imK + a.imJ * b.re + 0 * a.imJ * b.imI - -1 * a.imK * b.imI =
    a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
x : (i : ι) × α i
⊢ (a * b) • x = a • b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
x : (i : ι) × α i
⊢ 1 • x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ a.re * b.imK + a.imI * b.imJ + 0 * a.imI * b.imK - a.imJ * b.imI + a.imK * b.re =
    a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a).re = a.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a + star a = ↑(2 * a.re)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a + star a = 2 * ↑a.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a + a = ↑(2 * a.re)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a + a = 2 * ↑a.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a = ↑(2 * a.re) - a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a.im = -a.im

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y : R
a b : ℍ[R]
⊢ (0 * star 0).re = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x y : R
a b : ℍ[R]
⊢ (1 * star 1).re = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
⊢ ↑(x * y * star (x * y)).re = ↑((x * star x).re * (y * star y).re)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
x : α ⊕ β
⊢ (a • x).swap = a • x.swap

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
x : R
⊢ normSq ↑x = x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq (star a) = normSq a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ normSq ↑n = ↑n ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
z : ℤ
⊢ normSq ↑z = ↑z ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
⊢ (a • b) • x = a • b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq (-a) = normSq a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a * star a = ↑(normSq a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
a : M
b : N
x : α ⊕ β
⊢ a • b • x = b • a • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a * a = ↑(normSq a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hfmodP2 : map (Ideal.Quotient.mk (ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0
g h : R[X]
h_eq : f = g * h
⊢ IsUnit g ∨ IsUnit h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a.im ^ 2 = -↑(normSq a.im)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ ↑(normSq (a + b)) = ↑(normSq a) + a * star b + b * star a + ↑(normSq b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x✝ : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
x : α ⊕ β
⊢ MulOpposite.op a • x = a • x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ Irreducible (map (algebraMap R (FractionRing (R ⧸ P))) X)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
r : R
q : ℍ[R]
⊢ normSq (r • q) = r ^ 2 * normSq q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a✝ : M
b : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M α
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
a : α
⊢ m₁✝ • a = m₂✝ • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq (a + b) = normSq a + (a * star b).re + ((b * star a).re + normSq b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : SMul M α
inst✝³ : SMul M β
inst✝² : SMul N α
inst✝¹ : SMul N β
a : M
b✝ : α
c : β
x : α ⊕ β
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α ⊕ β), m₁✝ • a = m₂✝ • a
b : β
⊢ m₁✝ • b = m₂✝ • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + (a * star b).re + ((b * star a).re + normSq b) = normSq a + normSq b + ((a * star b).re + (b * star a).re)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
x : α ⊕ β
⊢ (a * b) • x = a • b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
x : α ⊕ β
⊢ 1 • x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + ((a * star b).re + (b * star a).re) = normSq a + normSq b + 2 * (a * star b).re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ normSq a = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ 0 ≤ normSq a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ a b : ℍ[R]
hab : a * b = 0
⊢ normSq a * normSq b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a ^ 2 = ↑(normSq a) ↔ a = ↑a.re

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑(a • s • t) = ↑(s • a • t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
⊢ ↑(s • t • u) = ↑(t • s • u)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
s : Finset γ
⊢ (a • b) • s = a • b • s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : Finset α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : SMul α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
a : α
s : Finset β
⊢ ↑(op a • s) = ↑(a • s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(normSq a) ↔ a.re = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : DecidableEq α
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Finset β
⊢ image (fun b ↦ 1 • b) s = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ 0⁻¹ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SMul α β
inst✝¹ : IsLeftCancelSMul α β
inst✝ : DecidableEq β
s : Set α
t : Finset β
⊢ (s.PairwiseDisjoint fun x ↦ x • t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑x✝ = ↑x✝.num / ↑x✝.den

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
⊢ a • s = univ ↔ s = univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑(s • univ) = ↑univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ * x✝

Tactic:
by

Goal state after: