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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
H : Subsingleton R
hpq : m = 0 ∧ n = 0
⊢ m = 0

Tactic:
exact hpq.1

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.reverse.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree

Tactic:
natTrailingDegree_reverse,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ 0 + p.natTrailingDegree = p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * h * (g.mirror * h.mirror) = k * (g.mirror * h.mirror.mirror)

Tactic:
mirror_mirror,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * h * (g.mirror * h.mirror) = k * (g.mirror * h)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R b a
⊢ destutter' R b (a :: l) = b :: destutter' R a l

Tactic:
by
  rw [destutter', if_pos h]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))

Tactic:
have := hl a (by simp) b (by simp)
    simp_rw [map_cons, destutter_cons_cons, ← this]
    by_cases hr : R a b <;>
      simp [hr, ← destutter_cons', map_destutter fun c hc d hd ↦ hl _ (cons_subset_cons _
        (subset_cons_self _ _) hc) _ (cons_subset_cons _ (subset_cons_self _ _) hd),
        map_destutter fun c hc d hd ↦ hl _ (subset_cons_self _ _ hc) _ (subset_cons_self _ _ hd)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp1 : p ≠ 1 := by rintro rfl; rw [natDegree_one] at hp2; cases hp2

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ Irreducible p ↔ p.roots = 0
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (aeval x) p = p.smeval x

Tactic:
aeval_def,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ eval₂ (algebraMap R S) x p = p.smeval x
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ (⇑derivative)^[k] p = k ! • gp

Tactic:
by
  refine ⟨_, (natDegree_sum_le _ _).trans ?_, iterate_derivative_eq_factorial_smul_sum p k⟩
  rw [fold_max_le]
  refine ⟨Nat.zero_le _, fun i hi => ?_⟩
  dsimp only [Function.comp]
  exact (natDegree_C_mul_le _ _).trans <| (natDegree_X_pow_le _).trans <|
    (le_natDegree_of_mem_supp _ hi).trans <| natDegree_iterate_derivative _ _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ (aeval r) ((⇑derivative)^[k] p) = 0

Tactic:
aeval_def,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval₂ (algebraMap R A) r ((⇑derivative)^[k] p) = 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ (aeval r) ((⇑derivative)^[q] p) = q ! • eval r p'

Tactic:
aeval_def,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval₂ (algebraMap R A) r ((⇑derivative)^[q] p) = q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
replace hy := hp.2 m (mem_insert_of_mem (mem_insert_self m {n}))

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * ∏ x ∈ s, g x +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * ∏ x ∈ s, g x) +
        Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) j *
          ∏ k ∈ (Finset.cons i s hi).erase j, g k)

Tactic:
Function.update_of_ne (hjs hj).symm,

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j * ∏ k ∈ s.erase j, g k =
    r j * b j %ₘ g i * ∏ x ∈ s, g x +
      ((r j * b j /ₘ g i + r j * a j /ₘ g j) * (g i * ∏ x ∈ s, g x) +
        r j * a j %ₘ g j * ∏ k ∈ (Finset.cons i s hi).erase j, g k)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : c = 0
⊢ ((monomial d) c).signVariations = 0

Tactic:
simp [hcz]

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

Goal state before:
pp: p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial

Tactic:
by
  rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * (a j * g i + b j * g j)

Tactic:
hab j hj,

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * 1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ (aeval r) (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p))

Tactic:
aeval_def,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p))
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
trinomial_natDegree hkm' hmn' z.ne_zero

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : SignType.sign P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
rcases s_nC.trichotomy with rfl | rfl | rfl

Goal state after:
case succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

case succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

case succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Regular.Prod

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : Mul R
inst✝ : Mul S
a : R
b : S
⊢ IsRegular (a, b) ↔ IsRegular a ∧ IsRegular b

Tactic:
by
  simp [isRegular_iff, and_and_and_comm]

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
by
  constructor
  · apply (act' x).symm.injective
  rintro rfl
  rfl

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case h
R : Type u_1
inst✝ : Rack R
y z : Rᵐᵒᵖ
X✝ : R
⊢ op (unop (op X✝) ◃⁻¹ unop (op (unop y ◃⁻¹ unop z))) =
    op (unop (op (unop (op X✝) ◃⁻¹ unop y)) ◃⁻¹ unop (op (unop (op X✝) ◃⁻¹ unop z)))

Tactic:
induction y

Goal state after:
case h.h
R : Type u_1
inst✝ : Rack R
z : Rᵐᵒᵖ
X✝¹ X✝ : R
⊢ op (unop (op X✝¹) ◃⁻¹ unop (op (unop (op X✝) ◃⁻¹ unop z))) =
    op (unop (op (unop (op X✝¹) ◃⁻¹ unop (op X✝))) ◃⁻¹ unop (op (unop (op X✝¹) ◃⁻¹ unop z)))
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₃
⊢ q.i * c₂ • q.j - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)

Tactic:
mul_smul_comm,

Goal state after:
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₂ • (q.i * q.j) - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)
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₃
⊢ q.i * c₃ • 1 = c₃ • q.i

Tactic:
mul_smul_comm,

Goal state after:
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₃ • (q.i * 1) = c₃ • q.i
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₃
⊢ q.i * c₂ • q.j * q.j - (c₁ • q.j + c₂ • (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)

Tactic:
mul_smul_comm,

Goal state after:
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₂ • (q.i * q.j) * q.j - (c₁ • q.j + c₂ • (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)
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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    x.re • (1 * y.re • 1) + x.re • (1 * y.imI • q.i) + x.re • (1 * y.imJ • q.j) + x.re • (1 * y.imK • q.k) +
          (x.imI • (q.i * y.re • 1) + x.imI • (q.i * y.imI • q.i) + x.imI • (q.i * y.imJ • q.j) +
            x.imI • (q.i * y.imK • q.k)) +
        (x.imJ • (q.j * y.re • 1) + x.imJ • (q.j * y.imI • q.i) + x.imJ • (q.j * y.imJ • q.j) +
          x.imJ • (q.j * y.imK • q.k)) +
      (x.imK • (q.k * y.re • 1) + x.imK • (q.k * y.imI • q.i) + x.imK • (q.k * y.imJ • q.j) +
        x.imK • (q.k * y.imK • q.k))

Tactic:
mul_smul_comm,

Goal state after:
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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    x.re • y.re • (1 * 1) + x.re • y.imI • (1 * q.i) + x.re • y.imJ • (1 * q.j) + x.re • y.imK • (1 * q.k) +
          (x.imI • y.re • (q.i * 1) + x.imI • y.imI • (q.i * q.i) + x.imI • y.imJ • (q.i * q.j) +
            x.imI • y.imK • (q.i * q.k)) +
        (x.imJ • y.re • (q.j * 1) + x.imJ • y.imI • (q.j * q.i) + x.imJ • y.imJ • (q.j * q.j) +
          x.imJ • y.imK • (q.j * q.k)) +
      (x.imK • y.re • (q.k * 1) + x.imK • y.imI • (q.k * q.i) + x.imK • y.imJ • (q.k * q.j) +
        x.imK • y.imK • (q.k * q.k))
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
x y : A
w : s x y
⊢ (mkAlgHom S s) x = (mkAlgHom S s) y

Tactic:
simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial n) a * X = (monomial (n + 1)) a

Tactic:
X,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
⊢ (monomial n) a * (monomial 1) 1 = (monomial (n + 1)) a
Module: Mathlib.Algebra.SkewPolynomial.Basic

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

Tactic:
X,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
hn : X ^ n = (monomial n) 1
⊢ (monomial 1) 1 * (monomial n) 1 = (monomial (n + 1)) 1
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
X,

Goal state after:
R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ ((monomial 1) 1).support = ∅
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p q : SkewMonoidAlgebra k G
⊢ p = q ↔ ∀ (n : G), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f : G →₀ k⟩

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
q : SkewMonoidAlgebra k G
f : G →₀ k
⊢ { coeff := f } = q ↔ ∀ (n : G), { coeff := f }.coeff n = q.coeff n
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∃ y, ↑(toUnits v) * y • 1 = ↑(toUnits u)) ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
mul_smul_comm,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∃ y, y • (↑(toUnits v) * 1) = ↑(toUnits u)) ↔ ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : Nontrivial k
a b : G
h : (of k G) a = (of k G) b
⊢ a = b

Tactic:
simp_rw [of_apply, ← coeff_inj] at h
  simpa using (Finsupp.single_eq_single_iff _ _ _ _).mp h

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ ((X.restrict h).presheaf.germ V x ?hx ≫ (X.restrictStalkIso h x).hom) ≫ (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx

pp: case hx
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ x ∈ V

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ (X.restrict h).presheaf.germ V x ?hx ≫ (X.restrictStalkIso h x).hom ≫ (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx

case hx
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ x ∈ V
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ (eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x)) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
Category.assoc,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case inst
X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (f.stalkMap x).hom'

Tactic:
apply isLocalHomValStalkMap

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case inst
X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (g.stalkMap ((ConcreteCategory.hom f.base) x)).hom'

Tactic:
apply isLocalHomValStalkMap

Goal state after: