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

Goal state before:
pp: case e_6.e_re
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ x✝.re + 0 + 0 + 0 = x✝.re

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case e_6.e_imI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 + x✝.imI • 1 + 0 + 0 = x✝.imI

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case e_6.e_imJ
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 + 0 + x✝.imJ • 1 + 0 = x✝.imJ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case e_6.e_imK
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ 0 + 0 + 0 + x✝.imK • 1 = x✝.imK

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : IsFormallyReal R
s : R
h₁ : IsSumSq s
h₂ : IsSumSq (-s)
⊢ s + -s = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
n : ℕ
hn : 1 + ↑n = 0
⊢ IsSumSq ↑n

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
a b : SkewMonoidAlgebra A G
⊢ equivMapDomain e (a + b) = equivMapDomain e a + equivMapDomain e b

Tactic:
by simp [equivMapDomain_eq_mapDomain, map_add]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ { coeff := Finsupp.erase a (coeff 0) } = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a a' : α
b : M
f : SkewMonoidAlgebra M α
⊢ ∀ (x y : SkewMonoidAlgebra M α),
    { coeff := Finsupp.erase a (x + y).coeff } =
      { coeff := Finsupp.erase a x.coeff } + { coeff := Finsupp.erase a y.coeff }

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a (f.coeff a)).coeff a✝ = f.coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (a b c : RingQuot r), a + b + c = a + (b + c)

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk.mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝² : Quot (Rel r)
a✝² : R
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝² } + { toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝² } + ({ toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ })
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (a b c : RingQuot r), a * b * c = a * (b * c)

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk.mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝² : Quot (Rel r)
a✝² : R
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝² } * { toQuot := Quot.mk (Rel r) a✝¹ } * { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝² } * ({ toQuot := Quot.mk (Rel r) a✝¹ } * { toQuot := Quot.mk (Rel r) a✝ })
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (a b c : RingQuot r), a * (b + c) = a * b + a * c

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk.mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝² : Quot (Rel r)
a✝² : R
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ { toQuot := Quot.mk (Rel r) a✝² } * ({ toQuot := Quot.mk (Rel r) a✝¹ } + { toQuot := Quot.mk (Rel r) a✝ }) =
    { toQuot := Quot.mk (Rel r) a✝² } * { toQuot := Quot.mk (Rel r) a✝¹ } +
      { toQuot := Quot.mk (Rel r) a✝² } * { toQuot := Quot.mk (Rel r) a✝ }
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (a b c : RingQuot r), (a + b) * c = a * c + b * c

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩

Goal state after:
case mk.mk.mk
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
toQuot✝² : Quot (Rel r)
a✝² : R
toQuot✝¹ : Quot (Rel r)
a✝¹ : R
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ({ toQuot := Quot.mk (Rel r) a✝² } + { toQuot := Quot.mk (Rel r) a✝¹ }) * { toQuot := Quot.mk (Rel r) a✝ } =
    { toQuot := Quot.mk (Rel r) a✝² } * { toQuot := Quot.mk (Rel r) a✝ } +
      { toQuot := Quot.mk (Rel r) a✝¹ } * { toQuot := Quot.mk (Rel r) a✝ }
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ∃ a, (fun x ↦ { toQuot := Quot.mk (Rel r) x }) a = { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_2
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ (mkRingHom r) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (((ringQuotToIdealQuotient r).comp (idealQuotientToRingQuot r)).comp (Ideal.Quotient.mk (Ideal.ofRel r))) x =
    ((RingHom.id (B ⧸ Ideal.ofRel r)).comp (Ideal.Quotient.mk (Ideal.ofRel r))) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (((idealQuotientToRingQuot r).comp (ringQuotToIdealQuotient r)).comp (mkRingHom r)) x =
    ((RingHom.id (RingQuot r)).comp (mkRingHom r)) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
h : 4 * P = 4 • P
⊢ P = (1 / 4 * 4) • P

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : Algebra ℝ R
inst✝ : IsOrderedModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
P : R := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
idem : P * P = 4 * P
idem' : P = (1 / 4) • (P * P)
sa : star P = P
⊢ 0 ≤ 1 / 4

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: ⊢ (√2 * √2)⁻¹ = 2⁻¹

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
⊢ p.support.card = 0 ↔ p = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
p : SkewPolynomial R
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
⊢ ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩).comp ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩) =
    AlgHom.id S (RingQuot (rel on ⇑f.symm))

Tactic:
ext b

Goal state after:
R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
b : B
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩)).comp
        (mkAlgHom S (rel on ⇑f.symm)))
      b =
    ((AlgHom.id S (RingQuot (rel on ⇑f.symm))).comp (mkAlgHom S (rel on ⇑f.symm))) b
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
b : B
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩)).comp
        (mkAlgHom S (rel on ⇑f.symm)))
      b =
    ((AlgHom.id S (RingQuot (rel on ⇑f.symm))).comp (mkAlgHom S (rel on ⇑f.symm))) b

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a : R
⊢ (⇑φ)^[0] a = ofAdd 0 • a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃ₐ[S] B
rel : A → A → Prop
a : A
⊢ ((((liftAlgHom S) ⟨(mkAlgHom S rel).comp ↑f.symm, ⋯⟩).comp
            ((liftAlgHom S) ⟨(mkAlgHom S (rel on ⇑f.symm)).comp ↑f, ⋯⟩)).comp
        (mkAlgHom S rel))
      a =
    ((AlgHom.id S (RingQuot rel)).comp (mkAlgHom S rel)) a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁶ : Semiring R
S : Type uS
inst✝⁵ : CommSemiring S
T : Type uT
A : Type uA
inst✝⁴ : Semiring A
inst✝³ : Algebra S A
r : R → R → Prop
inst✝² : Semiring T
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A ≃+* B
rel : A → A → Prop
n : ℕ
⊢ f ((algebraMap ℕ A) n) = (algebraMap ℕ B) n

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (p.sum fun a₂ b₂ ↦ (monomial (1 + a₂)) (0 * (⇑φ)^[1] b₂)) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ ∀ (a : ℕ), (((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a + a₂)) (0 * (⇑φ)^[a] b₂)) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    (((monomial 1) 1).sum fun a₂ b₂_1 ↦ (monomial (a + a₂)) ((b₁ + b₂) * (⇑φ)^[a] b₂_1)) =
      (((monomial 1) 1).sum fun a₂ b₂ ↦ (monomial (a + a₂)) (b₁ * (⇑φ)^[a] b₂)) +
        ((monomial 1) 1).sum fun a₂ b₂_1 ↦ (monomial (a + a₂)) (b₂ * (⇑φ)^[a] b₂_1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
x✝ : α
⊢ (starCenterToCentroid.toFun ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
by
    simp [starCenterToCentroid_apply, ← map_mul_right]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ∀ (a : ℕ), (monomial a) ((⇑φ)^[n] 0) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ∀ (a : ℕ) (b₁ b₂ : R), (monomial a) ((⇑φ)^[n] (b₁ + b₂)) = (monomial a) ((⇑φ)^[n] b₁) + (monomial a) ((⇑φ)^[n] b₂)

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ (p.sum fun a b ↦ ((monomial a) (φ b)).sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ (n + 1) =
    (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
r : R
⊢ (monomial n) r * X ^ 0 = (monomial (n + 0)) r

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬X.coeff 1 = coeff 0 1

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : a = 0
⊢ Finset.map toAdd.toEmbedding ((SkewMonoidAlgebra.support p).erase (ofAdd n)) =
    (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p)).erase n

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
inst✝ : DecidableEq R
h✝ : ¬a = 0
⊢ Finset.map toAdd.toEmbedding (insert (ofAdd n) (SkewMonoidAlgebra.support p)) =
    insert n (Finset.map toAdd.toEmbedding (SkewMonoidAlgebra.support p))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ (p.update n 0).support = p.support.erase n

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a b : G →₀ k
⊢ { coeff := a + b } = { coeff := a }.add { coeff := b }

Tactic:
add

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a b : G →₀ k
⊢ { coeff := a + b } = { coeff := a + b }
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
s : S
a : G
b : k
⊢ (s • single a b).coeff = (single a (s • b)).coeff

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
⊢ (coeff 1) 1 = 1

Tactic:
simp

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

Goal state before:
pp: case ofNat
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = single 1 ↑(Int.ofNat a✝)

Tactic:
simp

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

Goal state before:
pp: case negSucc
k : Type u_1
G : Type u_2
inst✝¹ : AddGroupWithOne k
inst✝ : One G
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) = single 1 ↑(Int.negSucc a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
a✝ : R
⊢ (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits 1));
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
      a✝ =
    1 a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
g h : ↥(unitary R)
a✝ : R
⊢ (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits (g * h)));
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
      a✝ =
    ((let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits g));
        { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }) *
        let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits h));
        { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
      a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u : ↥(unitary R)
x : R
⊢ ((conjStarAlgAut S R) (star u)) x = star ↑u * x * ↑u

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
u₁ u₂ : ↥(unitary R)
x : R
⊢ ((conjStarAlgAut S R) (u₁ * u₂)) x = ((conjStarAlgAut S R) u₁) (((conjStarAlgAut S R) u₂) x)

Tactic:
simp

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (1 * 1 • b₂)) = single g a

Tactic:
simp

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (0 * 1 • b₂)) = 0

Tactic:
simp

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 1) = single g a

Tactic:
simp

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 0) = 0

Tactic:
simp

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝² : Semiring S
inst✝¹ : AddCommMonoid k
inst✝ : Module S k
⊢ ∀ (c : S) (x : SkewMonoidAlgebra k G), coeffAddEquiv (c • x) = c • coeffAddEquiv x

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop a = untrop a

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop b = untrop b

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : a ≤ b
⊢ untrop b = untrop b

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop a = untrop a

Tactic:
simp

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
⊢ untrop (if 0 + 1 = 0 then 0 else 1) = untrop ((if 0 = 0 then 0 else 1) + 1)

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n✝ : ℕ
⊢ untrop (if n✝ + 1 + 1 = 0 then 0 else 1) = untrop ((if n✝ + 1 = 0 then 0 else 1) + 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : AddMonoid R
x✝ : Tropical R
⊢ untrop (x✝ ^ 0) = untrop 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case nil
R : Type u_1
inst✝ : AddMonoid R
⊢ trop [].sum = (map trop []).prod

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case nil
R : Type u_1
inst✝ : AddMonoid R
⊢ untrop [].prod = (map untrop []).sum

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case nil
R : Type u_1
inst✝ : LinearOrder R
⊢ trop [].minimum = (map (trop ∘ WithTop.some) []).sum

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = (map trop 0).sum

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), a * x = z ↔ a = y
a₁ : G
b₁ : k
⊢ (if a₁ * x = z then b₁ * a₁ • 0 else 0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = (map untrop 0).inf

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f : SkewMonoidAlgebra k G
r : k
x y z : G
H : ∀ (a : G), x * a = y ↔ a = z
⊢ (f.sum fun a b ↦ if x * a = y then 0 * x • b else 0) = 0

Tactic:
simp

Goal state after: