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

Goal state before:
pp: p : ℤ[X]
hp : #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)
⊢ p.IsUnitTrinomial

Tactic:
obtain ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩ := card_support_eq_three.mp hp.1

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp :
  #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3 ∧
    ∀ k_1 ∈ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support,
      IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL✝ : P.eraseLead.coeffList = c :: cs
h₁ : SignType.sign c ≠ 0
h_eL : P.eraseLead ≠ 0
ls : List R
hls : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls
⊢ c = P.eraseLead.leadingCoeff

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - ((monomial (P.natDegree + 1)) P.leadingCoeff - C η * (monomial P.natDegree) P.leadingCoeff) -
      (monomial P.natDegree) P.nextCoeff

Tactic:
C_mul_monomial,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ X * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      (monomial P.natDegree) (P.coeff d - η * P.coeff (d + 1)) =
    X * P - C η * P - ((monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) (η * P.leadingCoeff)) -
      (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑u ↑v ↑w
f : ℤ[X] → ℤ[X] :=
  fun p ↦
    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp.coeff) }
hm : m = n - m + k
hm' : m' = n - m' + k
⊢ q = p ∨ q = p.mirror

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : (p * p.mirror).leadingCoeff = (q * q.mirror).leadingCoeff
⊢ q = p ∨ q = p.mirror

Tactic:
rw [leadingCoeff_mul, leadingCoeff_mul, mirror_leadingCoeff, mirror_leadingCoeff, hp, hq,
    trinomial_leadingCoeff hkm hmn w.ne_zero, trinomial_leadingCoeff hkm' hmn' z.ne_zero,
    trinomial_trailingCoeff hkm hmn u.ne_zero, trinomial_trailingCoeff hkm' hmn' x.ne_zero]
    at hmul

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this✝³ : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
this✝² : P.natDegree + 2 = ((X - C η) * P).coeffList.length
this✝¹ : ((X - C η) * P).leadingCoeff = P.leadingCoeff
h₉ : ((X - C η) * P).nextCoeff = 0
this✝ : ((X - C η) * P).eraseLead = ((X - C η) * P.eraseLead).eraseLead
this :
  ((X - C η) * P).coeffList =
    ((X - C η) * P).leadingCoeff ::
      (List.replicate (((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ) 0 ++
        ((X - C η) * P).eraseLead.coeffList)
⊢ ((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isFalse
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : ¬decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue.isFalse
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : ¬1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ + y✝) = (equivProd a b) x✝ + (equivProd a b) y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (-x✝) = -(equivProd a b) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ y✝ : QuadraticAlgebra R a b
⊢ (equivProd a b) (x✝ - y✝) = (equivProd a b) x✝ - (equivProd a b) y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
n✝ : ℕ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
x✝ : QuadraticAlgebra R a b
n✝ : ℤ
⊢ (equivProd a b) (n✝ • x✝) = n✝ • (equivProd a b) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case re
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).re = (OfNat.ofNat n).re

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case im
R : Type u_1
a b : R
inst✝¹ : AddCommMonoidWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ (QuadraticAlgebra.C (OfNat.ofNat n)).im = (OfNat.ofNat n).im

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: case mp
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ (algebraMap R (QuadraticAlgebra R a b)) r ∣ z → r ∣ z.re ∧ r ∣ z.im

pp: case mpr
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ r ∣ z.re ∧ r ∣ z.im → (algebraMap R (QuadraticAlgebra R a b)) r ∣ z

Tactic:
· rintro ⟨x, rfl⟩
    simp

Goal state after:
case mpr
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
z : QuadraticAlgebra R a b
⊢ r ∣ z.re ∧ r ∣ z.im → (algebraMap R (QuadraticAlgebra R a b)) r ∣ z
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
⊢ ∀ (x y : QuadraticAlgebra R a b), 2 * (x + y).re + b * (x + y).im = 2 * x.re + b * x.im + (2 * y.re + b * y.im)

Tactic:
grind

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re ^ 2 = a * z.im * z.im - b * z.re * z.im
h : ¬z.im = 0
⊢ (-z.re / z.im) ^ 2 = a + b * (-z.re / z.im)

Tactic:
grind

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
h : ¬z.im = 0
⊢ z = 0

Tactic:
· exfalso
      rw [← pow_two, sub_eq_zero, ← eq_sub_iff_add_eq] at hz
      apply Hab.out (-z.re / z.im)
      grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
⊢ n✝ + 1 ≤ P.signVariations

Tactic:
obtain ⟨η, η_root, η_pos⟩ : ∃ x, x ∈ P.roots ∧ 0 < x := by grind [Multiset.countP_pos]

Goal state after:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
η : R
η_root : η ∈ P.roots
η_pos : 0 < η
⊢ n✝ + 1 ≤ P.signVariations
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ y = x ◃ y

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Rack R
x : R
⊢ x ◃ x = x ◃ x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case mk.mk
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
i✝¹ j✝¹ k✝¹ : A
i_mul_i✝¹ : i✝¹ * i✝¹ = c₁ • 1 + c₂ • i✝¹
j_mul_j✝¹ : j✝¹ * j✝¹ = c₃ • 1
i_mul_j✝¹ : i✝¹ * j✝¹ = k✝¹
j_mul_i✝¹ : j✝¹ * i✝¹ = c₂ • j✝¹ - k✝¹
i✝ j✝ k✝ : A
i_mul_i✝ : i✝ * i✝ = c₁ • 1 + c₂ • i✝
j_mul_j✝ : j✝ * j✝ = c₃ • 1
i_mul_j✝ : i✝ * j✝ = k✝
j_mul_i✝ : j✝ * i✝ = c₂ • j✝ - k✝
hi :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
        j_mul_i := j_mul_i✝¹ }.i =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.i
hj :
  { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
        j_mul_i := j_mul_i✝¹ }.j =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }.j
⊢ { i := i✝¹, j := j✝¹, k := k✝¹, i_mul_i := i_mul_i✝¹, j_mul_j := j_mul_j✝¹, i_mul_j := i_mul_j✝¹,
      j_mul_i := j_mul_i✝¹ } =
    { i := i✝, j := j✝, k := k✝, i_mul_i := i_mul_i✝, j_mul_j := j_mul_j✝, i_mul_j := i_mul_j✝, j_mul_i := j_mul_i✝ }

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case incl
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x : EnvelGroup R
x✝ : R
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦incl x✝⟧ =
    F ⟦incl x✝⟧

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommMonoid M
inst✝² : DecidableEq M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ ↑s ∧ (↑t).Nonempty ∨ 0 ∈ ↑t ∧ (↑s).Nonempty ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (c₂ • c₃) • 1 - c₃ • q.i = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧

Tactic:
by
        induction x with
        | unit => exact F.map_one.symm
        | incl => rfl
        | mul x y ih_x ih_y =>
          have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
          simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
          suffices ∀ x y, F (Mul.mul x y) = F (x) * F (y) by
            simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
            rw [← ih_x, ← ih_y, mapAux]
          exact F.map_mul
        | inv x ih_x =>
          have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl
          rw [hm, map_inv, map_inv, ih_x]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s : R
hs : 0 ≠ 0
⊢ IsSumNonzeroSq 0

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
this : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
grind

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

Goal state before:
pp: case sq
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha✝ : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
x a✝ : R
ha : a✝ ≠ 0
⊢ a✝ * a✝ ≠ 0

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
this : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq 0

Tactic:
grind

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : IsSemireal R
hn : ↑0 = 0
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : Ring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h₁ : inst₁.toSemiring = inst₂.toSemiring := by
    ext : 1 <;> assumption
  have h₂ : inst₁.toNonAssocRing = inst₂.toNonAssocRing := by
    ext : 1 <;> assumption
  /- We prove that the `SubNegMonoid`s are equal because they are one
  field away from `Sub` and `Neg`, enabling use of `injection`. -/
  have h₃ : (inst₁.toAddCommGroup).toAddGroup.toSubNegMonoid
            = (inst₂.toAddCommGroup).toAddGroup.toSubNegMonoid :=
    congrArg (@AddGroup.toSubNegMonoid R) <| by ext : 1; exact h_add
  -- Split into fields and prove they are equal using the above.
  cases inst₁; cases inst₂
  congr <;> solve | injection h₂ | injection h₃

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.IntPolynomial

Goal state before:
pp: K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = (algebraMap K L) (P.coeff n) * x ^ n

Tactic:
rfl

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

Goal state before:
pp: case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝ : α
⊢ ↑a✝ * (0 + 0) = ↑a✝ * 0 + ↑a✝ * 0

Tactic:
rfl

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

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (0 + ↑a✝) = ↑a✝¹ * 0 + ↑a✝¹ * ↑a✝

Tactic:
rfl

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

Goal state before:
pp: case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (↑a✝ + 0) = ↑a✝¹ * ↑a✝ + ↑a✝¹ * 0

Tactic:
rfl

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝

Tactic:
rfl

Goal state after:
case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝
Module: Mathlib.Algebra.Ring.WithZero

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²

Tactic:
rfl

Goal state after:
case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case zero
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
f : CentroidHom α
a b : α
__AddMonoidHom✝ : α →+ α := f.toEnd ^ 0
⊢ (↑(f.toEnd ^ 0)).toFun (a * b) = a * (↑(f.toEnd ^ 0)).toFun b

Tactic:
rfl

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

Goal state before:
pp: case zero
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
f : CentroidHom α
a b : α
__AddMonoidHom✝ : α →+ α := f.toEnd ^ 0
⊢ (↑(f.toEnd ^ 0)).toFun (a * b) = (↑(f.toEnd ^ 0)).toFun a * b

Tactic:
rfl

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R✝ : Type u_4
α : Type u_5
inst✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
x✝¹ x✝ : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
G' : Type u_4
G'' : Type u_5
f : G ≃ G'
g : G' ≃ G''
l : SkewMonoidAlgebra k G
x : G''
⊢ (equivMapDomain (f.trans g) l).coeff x = (equivMapDomain g (equivMapDomain f l)).coeff x

Tactic:
rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
l : SkewMonoidAlgebra k G
x : G
⊢ (equivMapDomain (Equiv.refl G) l).coeff x = l.coeff x

Tactic:
rfl

Goal state after: