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

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : i = deg(p) - deg(q)
⊢ p.leadingCoeff ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : ¬i = deg(p) - deg(q)
⊢ 0 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
exacts [H₀ _, zero_mem _]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ↑b ≠ 0

Tactic:
rw [Int.cast_ne_zero]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
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 (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
rw [if_neg (hkm.trans hmn).ne', if_neg hmn.ne'] at hz

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
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 (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (x * 0 + y * 0 + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case e'_2.e'_5
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)
x : ℕ
⊢ x ∈ range q →
    eval r
        ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • (X - C r) ^ (q - (q - (x + 1))) *
          (⇑derivative)^[x + 1] p') =
      0

Tactic:
hx

Goal state after:
case e'_2.e'_5
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)
x : ℕ
hx : x ∈ range q
⊢ eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • (X - C r) ^ (q - (q - (x + 1))) *
        (⇑derivative)^[x + 1] p') =
    0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (-P).signVariations = P.signVariations

Tactic:
rw [signVariations, signVariations, coeffList_neg]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) (List.map (fun x ↦ -x) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  g i * (q₁ - q₂) * ∏ x ∈ s, g x + g i * (∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x - ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
← eq_sub_iff_add_eq',

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  g i * (∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x - ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x) =
    (r₂ i - r₁ i) * ∏ x ∈ s, g x - g i * (q₁ - q₂) * ∏ x ∈ s, g x
hgid : g i ∣ r₂ i - r₁ i
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
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
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
by
        have := coeffList_eraseLead (mul_ne_zero (X_sub_C_ne_zero η) h₃)
        #adaptation_note
        /--
        Moving from `nightly-2025-10-13` to `nightly-2025-10-19`
        we now need to provide an intermediate step.
        -/
        have : ((X - C η) * P).natDegree - ((X - C η) * P).eraseLead.degree.succ = n + 1 := by grind
        grind [leadingCoeff_mul, leadingCoeff_X_sub_C]

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

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
⊢ x ∉ Ico 0 q ∩ Ico q (p.natDegree + 1)

Tactic:
hx

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : x ∈ Ico 0 q ∩ Ico q (p.natDegree + 1)
⊢ False
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ (algebraMap R (QuadraticAlgebra R ?m.26 ?m.27)) x = (algebraMap R (QuadraticAlgebra R ?m.26 ?m.27)) 0

pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ R

pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ R

Tactic:
map_zero

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ (algebraMap R (QuadraticAlgebra R ?m.26 ?m.27)) x = 0

R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ R

R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ R
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ (algebraMap R (QuadraticAlgebra R a b)) 0 = 0

Tactic:
map_zero

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
H : ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
x : R
hxr : x * r = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocSemiring R
h : a₁✝.toDistrib = a₂✝.toDistrib
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalNonAssocRing R
h : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonUnitalSemiring = a₂✝.toNonUnitalSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : Semiring R
h : a₁✝.toNonAssocSemiring = a₂✝.toNonAssocSemiring
x y : R
⊢ x * y = x * y
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
x : R
⊢ IsSumNonzeroSq x → x ≠ 0

Tactic:
hx

Goal state after:
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 : R
hx : IsSumNonzeroSq x
⊢ x ≠ 0
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
x : R
⊢ IsSumNonzeroSq x → x ≠ 0

Tactic:
hx

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x : R
hx : IsSumNonzeroSq x
⊢ x ≠ 0
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
x : R
⊢ x ^ 2 = 0 → x = 0

Tactic:
hx

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
x : R
hx : x ^ 2 = 0
⊢ x = 0
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonAssocRing = toNonAssocRing
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x + y = x + y

case h_mul
R : Type u
a₁✝ a₂✝ : Ring R
h : a₁✝.toSemiring = a₂✝.toSemiring
x y : R
⊢ x * y = x * y
Module: Mathlib.Algebra.Ring.WithZero

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

Tactic:
cases b <;> cases c <;> try 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.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:
by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp only [mul_quot, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_4
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
a x : B
hx✝ : x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
⊢ (mkRingHom r) x = 0 → (mkRingHom r) (a • x) = 0

Tactic:
hx

Goal state after:
case refine_4
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
a x : B
hx✝ : x ∈ Submodule.span B {x | ∃ a b, r a b ∧ x + b = a}
hx : (mkRingHom r) x = 0
⊢ (mkRingHom r) (a • x) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
a✝ : x✝ ∈ s
⊢ x✝ ∉ p.support → f x✝ (p.coeff x✝) = 0

Tactic:
hx

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
x✝ : ℕ
a✝ : x✝ ∈ s
hx : x✝ ∉ p.support
⊢ f x✝ (p.coeff x✝) = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p q : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (SkewMonoidAlgebra.sum (p + q) fun n r ↦ f (toAdd n) r) =
    (SkewMonoidAlgebra.sum p fun n r ↦ f (toAdd n) r) + SkewMonoidAlgebra.sum q fun n r ↦ f (toAdd n) r

Tactic:
exact SkewMonoidAlgebra.sum_add_index (fun n _ ↦ hf (toAdd n)) (fun n _ ↦ h_add (toAdd n))

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n i : ℕ
a : R
h : i ≠ n
⊢ (p.update n a).coeff i = p.coeff i

Tactic:
rw [p.coeff_update_apply, if_neg h]

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

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := e.star
this : Mul R := e.mul
x✝ : R
⊢ e (star x✝) = star (e x✝)

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := e.star
this : Mul R := e.mul
x✝ y✝ : R
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := e.star
this : AddMonoid R := e.addMonoid
x✝ : R
⊢ e (star x✝) = star (e x✝)

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : AddMonoid S
inst✝ : StarAddMonoid S
this✝ : Star R := e.star
this : AddMonoid R := e.addMonoid
x✝ y✝ : R
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
x✝ : R
⊢ e (star x✝) = star (e x✝)

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
x✝ y✝ : R
⊢ e (x✝ + y✝) = e x✝ + e y✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case mul
R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : StarRing S
this✝ : Star R := e.star
this : NonUnitalNonAssocSemiring R := e.nonUnitalNonAssocSemiring
x✝ y✝ : R
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case star
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := e.star
this : SMul 𝕜 R := Equiv.smul 𝕜 e
x✝ : R
⊢ e (star x✝) = star (e x✝)

Tactic:
exact e.apply_symm_apply _

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

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
e : R ≃ S
𝕜 : Type u_3
inst✝³ : Star 𝕜
inst✝² : Star S
inst✝¹ : SMul 𝕜 S
inst✝ : StarModule 𝕜 S
this✝ : Star R := e.star
this : SMul 𝕜 R := Equiv.smul 𝕜 e
r✝ : 𝕜
x✝ : R
⊢ e (r✝ • x✝) = r✝ • e x✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
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✝ : NonUnitalNonAssocSemiring S
b : S
s : SkewMonoidAlgebra k G
f : G → k → S
⊢ b * s.sum f = s.sum fun a c ↦ b * f a c

Tactic:
by
  simp only [sum, Finsupp.sum, Finset.mul_sum]

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 g : SkewMonoidAlgebra k G
x : G
⊢ (Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite

Tactic:
apply Set.Finite.subset (Finset.finite_toSet ((f.support).product (g.support)))

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
⊢ (Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2) ⊆ ↑(f.support.product g.support)
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 g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2 =
    ∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
apply Finset.sum_congr_of_eq_on_inter <;> aesop

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
x✝ : Tropical R
⊢ untrop (0 * x✝) = untrop 0

Tactic:
by simp [top_add]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i)

Tactic:
convert! Multiset.untrop_prod (s.val.map f)

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum