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

Goal state before:
pp: case re
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)).re = (star b * star a).re

Tactic:
simp

Goal state after:
case re
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₃]
⊢ a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK +
      c₂ * (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ) =
    (b.re + c₂ * b.imI) * (a.re + c₂ * a.imI) + c₁ * b.imI * a.imI + c₃ * b.imJ * a.imJ + c₂ * c₃ * b.imJ * a.imK -
      c₁ * c₃ * b.imK * a.imK
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
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)).imI = (star b * star a).imI

Tactic:
simp

Goal state after:
case imI
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₃]
⊢ -(c₃ * a.imK * b.imJ) + (c₃ * a.imJ * b.imK - (a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI)) =
    -((b.re + c₂ * b.imI) * a.imI) + -(b.imI * (a.re + c₂ * a.imI)) + c₂ * b.imI * a.imI - c₃ * b.imJ * a.imK +
      c₃ * b.imK * a.imJ
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
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)).imJ = (star b * star a).imJ

Tactic:
simp

Goal state after:
case imJ
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₃]
⊢ c₁ * a.imK * b.imI - (a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI) =
    -((b.re + c₂ * b.imI) * a.imJ) + c₁ * b.imI * a.imK + -(b.imJ * (a.re + c₂ * a.imI)) + c₂ * b.imJ * a.imI -
      c₁ * b.imK * a.imI
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
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)).imK = (star b * star a).imK

Tactic:
simp

Goal state after:
case imK
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₃]
⊢ -(a.imK * b.re) + (a.imJ * b.imI - (a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK)) =
    -((b.re + c₂ * b.imI) * a.imK) + b.imI * a.imJ + c₂ * b.imI * a.imK - b.imJ * a.imI + -(b.imK * (a.re + c₂ * a.imI))
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).re = (a * (↑(2 * a.re + c₂ * a.imI) - a)).re

Tactic:
simp

Goal state after:
case re
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.re = a.re * (2 * a.re + c₂ * a.imI - a.re)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imI = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imI

Tactic:
simp

Goal state after:
case imI
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imI + -(a.imI * a.re) = -(a.re * a.imI) + a.imI * (2 * a.re + c₂ * a.imI - a.re)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imJ
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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imJ = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imJ

Tactic:
simp

Goal state after:
case imJ
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) =
    -(a.re * a.imJ) + -(c₁ * a.imI * a.imK) + a.imJ * (2 * a.re + c₂ * a.imI - a.re)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imK
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
⊢ ((↑(2 * a.re + c₂ * a.imI) - a) * a).imK = (a * (↑(2 * a.re + c₂ * a.imI) - a)).imK

Tactic:
simp

Goal state after:
case imK
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
⊢ (2 * a.re + c₂ * a.imI - a.re) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) =
    -(a.re * a.imK) + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + a.imK * (2 * a.re + c₂ * a.imI - a.re)
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

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

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
case imI
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imI + -(a.imI * a.re) + -(c₂ * a.imI * a.imI) + c₃ * a.imJ * a.imK + -(c₃ * a.imK * a.imJ) = 0
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
case imJ
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imJ + -(c₁ * a.imI * a.imK) + -(a.imJ * a.re) + -(c₂ * a.imJ * a.imI) + c₁ * a.imK * a.imI = 0
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
case imK
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (a.re + c₂ * a.imI) * a.imK + -(a.imI * a.imJ) + -(c₂ * a.imI * a.imK) + a.imJ * a.imI + -(a.imK * a.re) = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
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
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ 0 + 0 + 0 + r * s %ₘ q = r * s %ₘ q

Tactic:
simp

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

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

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
rw [← coe_natCast, normSq_coe]

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 simp only [normSq_def, star_neg, neg_mul_neg]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ 0 ^ 2 = -↑(normSq 0) ↔ star 0 = -0

Tactic:
simp

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
a : R
⊢ a ∈ ker (algebraMap R (R ⧸ P)) ↔ a ∈ P

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) 1 x = x

Tactic:
simp

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

Goal state before:
pp: case zero
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h y : M
f : M → G
⊢ (shiftₗ M G h ^ 0) f y = f (y + 0 • h)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).1 = x✝.1

Tactic:
simp

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

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).2 = x✝.2

Tactic:
simp

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

Goal state before:
pp: case zero
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m : ℕ
⊢ x ^ (m * 0) = (x ^ m) ^ 0

Tactic:
rw [npow_zero, mul_zero, npow_zero]

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 0) x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ f (y + n • h) = ((fwdDiffₗ M G h + 1) ^ n) f y

Tactic:
rw [← shiftₗ_pow_apply h f, shiftₗ]

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

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 0).1 = 1.1

Tactic:
simp

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

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 0).2 = 1.2

Tactic:
simp

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

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).1 = x✝.1

Tactic:
simp

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

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝ : M × N
⊢ (x✝ ^ 1).2 = x✝.2

Tactic:
simp

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

Goal state before:
pp: case zero
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h x : M
⊢ Δ_[h]^[0] (⇑φ) x = (φ h - 1) ^ 0 * φ x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ Nat.card ↑s⁻¹ = Nat.card ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ Nat.card ↑(a • s) = Nat.card ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = (Finsupp.single i 1).prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h.h_zero
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = a.prod fun a b ↦ f a ^ (-b)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∀ (a : ι), f a ^ 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) = ∏ i, f i ^ a i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : IsCoatom M
⊢ IsCoatom (comap φ M)

Tactic:
refine And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM
  · rwa [← (comap_injective hφ).ne_iff, comap_top] at hM
  · intro K hK
    specialize hM (K.map φ)
    rw [← comap_lt_comap_of_surjective hφ, ← (comap_injective hφ).eq_iff] at hM
    rw [comap_map_eq_self ((M.ker_le_comap φ).trans hK.le), comap_top] at hM
    exact hM hK

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = (Finsupp.single i 1).prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case h.h_zero
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: R : Type u_4
inst✝ : Ring R
k : ℤ
⊢ (fun x ↦ x • 1) k = ↑k

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℕ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2) = ∏ i, f i ^ a i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ a ∈ (castAddHom A).range ↔ a ∈ zmultiples 1

Tactic:
AddMonoidHom.mem_range,

Goal state after:
A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ (∃ x, (castAddHom A) x = a) ↔ a ∈ zmultiples 1
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
x✝ : G
⊢ τ 0 f x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, τ a (f i)) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, τ a (f i)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ ∀ s ∈ toSubmonoid '' f, s.MulSaturated

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
hs : s.saturation.toSubmonoid ≤ s
⊢ s.saturation.MulSaturated

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #∅ ≤ #(∅ * ∅)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
inst✝ : IsLeftCancelMulZero α
⊢ #{0} ≤ #({0} * {0})

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : 1 < f (v k)
hk₁ : f (v k) < f (v i)
⊢ v k ∈ closure (v '' t)

Tactic:
by_contra hk₂

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : 1 < f (v k)
hk₁ : f (v k) < f (v i)
hk₂ : v k ∉ closure (v '' t)
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ 0⁻¹ ↔ a✝ ∈ 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ IsMulIndecomposable.baseOf v f ⊆ univ

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom ∘ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f

Tactic:
simp

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

Goal state before:
pp: case inl
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁶ : GroupWithZero M₀
inst✝⁵ : MulZeroOneClass N₀
inst✝⁴ : Nontrivial N₀
inst✝³ : NoZeroDivisors N₀
inst✝² : MulZeroOneClass G₀
inst✝¹ : DecidablePred fun x ↦ x = 0
inst✝ : DecidablePred fun x ↦ x = 0
f : M₀ →*₀ N₀
⊢ 1 (f 0) = 1 0

Tactic:
simp

Goal state after: