mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.inl
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x < 1
this : Units.mk0 (1 + x) h_2 ∈ B.unitGroup
⊢ x ∈ B

Tactic:
simpa using
        B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
          (B.neg_mem _ B.one_mem)

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ (max ↑a ↑b).untop₀ = max a b

pp: case neg
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ (max ↑a ↑b).untop₀ = max a b

Tactic:
· simp [max_eq_right h, max_eq_right (coe_le_coe.mpr h)]

Goal state after:
case neg
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ (max ↑a ↑b).untop₀ = max a b
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ s

Tactic:
rw [← hb]; exact smul_mem_smul_set ha

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
x y : R
⊢ mk (FiniteElement.mk (f (x * y)) ⋯) = mk (FiniteElement.mk (f x) ⋯) * mk (FiniteElement.mk (f y) ⋯)

Tactic:
map_mul

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
x y : R
⊢ mk (FiniteElement.mk (f x * f y) ⋯) = mk (FiniteElement.mk (f x) ⋯) * mk (FiniteElement.mk (f y) ⋯)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
⊢ FiniteResidueField.mk (FiniteElement.mk x hx - FiniteElement.mk (f r) ⋯) = 0 ↔ stdPart x = r

Tactic:
map_sub,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
⊢ FiniteResidueField.mk (FiniteElement.mk x hx) - FiniteResidueField.mk (FiniteElement.mk (f r) ⋯) = 0 ↔ stdPart x = r
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.eraseLead.coeff dk

Tactic:
rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
⊢ ∀ (c : Set (Partial seed)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → BddAbove c

Tactic:
intro c

Goal state after:
K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → BddAbove c
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : n < 1
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

pp: case inr.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ f.coeff 1 = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff 1

pp: case inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

Tactic:
· obtain rfl : n = 0 := Nat.lt_one_iff.mp hn
    simp

Goal state after:
case inr.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ f.coeff 1 = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff 1

case inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ 0 = 2 * 0

Tactic:
mul_zero

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ 0 = p.mirror * 0

Tactic:
mul_zero

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n i : ℕ
v : Fin n → R
hi : n ≤ i
⊢ ((ofFn n) v).coeff i = 0

Tactic:
simp [ofFn, Nat.not_lt_of_ge hi]

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

Goal state before:
pp: case isUnit_or_isUnit.inl
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
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inr (h3 h_dvd_f (by rwa [← hk]))

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p q : R[X]
x : S
⊢ (p - q).smeval x = p.smeval x - q.smeval x

Tactic:
rw [sub_eq_add_neg, smeval_add, smeval_neg, sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv p = ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p

Tactic:
dsimp [sumIDeriv]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ((derivativeFinsupp p).sum fun i ↦ id) = ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ sumIDeriv p = ∑ i ∈ range n, (⇑derivative)^[i] p

Tactic:
dsimp [sumIDeriv]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ((derivativeFinsupp p).sum fun i ↦ id) = ∑ i ∈ range n, (⇑derivative)^[i] p
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ sumIDeriv p = ∑ i ∈ range (n + 1), (⇑derivative)^[i] p

Tactic:
dsimp [sumIDeriv]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ((derivativeFinsupp p).sum fun i ↦ id) = ∑ i ∈ range (n + 1), (⇑derivative)^[i] p
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑i ≤ ↑n

Tactic:
mem_insert,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i ∈ {m, n}
⊢ ↑i ≤ ↑n
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i ∈ {m, n}
⊢ ↑i ≤ ↑n

Tactic:
mem_insert,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i ∈ {n}
⊢ ↑i ≤ ↑n
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑k ≤ ↑i

Tactic:
mem_insert,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i ∈ {m, n}
⊢ ↑k ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i ∈ {m, n}
⊢ ↑k ≤ ↑i

Tactic:
mem_insert,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i ∈ {n}
⊢ ↑k ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ ∈ {k, m, n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
mem_insert,

Goal state after:
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ = k ∨ k✝ ∈ {m, n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ = k ∨ k✝ ∈ {m, n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
mem_insert,

Goal state after:
k✝ k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hk : k✝ ∈ (trinomial k m n ↑u ↑v ↑w).support
this : k✝ = k ∨ k✝ = m ∨ k✝ ∈ {n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
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
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (SignType.sign P.leadingCoeff ::
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      1

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
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff

Tactic:
· grind [Nat.sub_add_cancel, List.length_pos_of_ne_nil, List.destutter'_ne_nil]

Goal state after:
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
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff
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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
have hQ : ((X - C η) * P).nextCoeff = coeff P d - η * coeff P (d + 1) := by
    grind [nextCoeff_of_natDegree_pos, coeff_X_sub_C_mul]

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)
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
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 = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)

Goal state after:
case inr.inl
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : ↑y = -↑v
hpq : -p * (-p).mirror = -p * (-p).mirror
hq : -p = trinomial k m' n (↑x) (-↑v) ↑z
⊢ -p = p ∨ -p = -p ∨ -p = p.mirror ∨ -p = -p.mirror

case inr.inr
p : ℤ[X]
h : IsRelPrime p p.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
h1 : ↑y = -↑v
hpq : -p * (-p).mirror = (-p).mirror * (-p).mirror.mirror
hq : (-p).mirror = trinomial k m' n (↑x) (-↑v) ↑z
⊢ (-p).mirror = p ∨ (-p).mirror = -p ∨ (-p).mirror = p.mirror ∨ (-p).mirror = -p.mirror
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
rw [self_distrib]
  rw [left_cancel]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  ((algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1)) *
      ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
    ((algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)) *
      ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
rw [hff, hff, (FaithfulSMul.algebraMap_injective R[X] K).eq_iff] at hf

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hff :
  ∀ {q : R[X]} {r : (i : ι) → Fin (n i) → R[X]},
    ((algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)) *
        ∏ i ∈ s, (algebraMap R[X] K) (g i) ^ n i =
      (algebraMap R[X] K) (q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k)
hf :
  q₁ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₁ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k =
    q₂ * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r₂ i j.rev * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: 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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₂ • q.j - q.k) = c₂ • F q.j - F q.k

Tactic:
map_sub,

Goal state after:
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
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
⊢ F (c₂ • q.j) - F q.k = c₂ • F q.j - F q.k
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case hi
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
q : Basis A c₁ c₂ c₃
⊢ ((Basis.self R).compHom q.liftHom).i = q.i

Tactic:
simp [Basis.lift]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case hj
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
q : Basis A c₁ c₂ c₃
⊢ ((Basis.self R).compHom q.liftHom).j = q.j

Tactic:
simp [Basis.lift]

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ T (S (a * b)) = S (T (a * b))

Tactic:
map_mul_right,

Goal state after:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ T (S a * b) = S (T (a * b))
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✝² : Semiring k
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
e : G ≃ H
⊢ ∀ (c : k) (x : SkewMonoidAlgebra A G), equivMapDomain e (c • x) = c • equivMapDomain e x

Tactic:
intro c

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝² : Semiring k
inst✝¹ : AddCommMonoid A
inst✝ : Module k A
e : G ≃ H
c : k
⊢ ∀ (x : SkewMonoidAlgebra A G), equivMapDomain e (c • x) = c • equivMapDomain e x
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Tactic:
· intro h
    induction h with
    | of => exact Relation.EqvGen.rel _ _ (Rel.of ‹_›)
    | refl => exact (RingQuot.ringCon r).refl _
    | symm => exact (RingQuot.ringCon r).symm ‹_›
    | trans => exact (RingQuot.ringCon r).trans ‹_› ‹_›
    | add => exact (RingQuot.ringCon r).add ‹_› ‹_›
    | mul => exact (RingQuot.ringCon r).mul ‹_› ‹_›

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_1
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
y a b : B
h : r a b
su : a - b = y
⊢ (mkRingHom r) (a - b) = 0

Tactic:
map_sub,

Goal state after:
case refine_1
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
y a b : B
h : r a b
su : a - b = y
⊢ (mkRingHom r) a - (mkRingHom r) b = 0
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:
← mul_smul

Goal state after:
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
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
m : ℤ
a : ℝ
x : R
⊢ ↑m • a • x = (↑m * a) • x

Tactic:
← mul_smul

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
m : ℤ
a : ℝ
x : R
⊢ (↑m * a) • x = (↑m * a) • x
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ 0 = q * 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ 0 = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.coeff + g.coeff⟩ by rw [ofCoeff_add, eta]]

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { coeff := f.coeff + g.coeff }.sum h = f.sum h + g.sum h
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.coeff + g.coeff⟩ by rw [ofCoeff_add, eta]]

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { coeff := f.coeff + g.coeff }.sum h = f.sum h + g.sum h