mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∑ x_1 ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
      x.coeff x_1.snd.1 * y.coeff x_1.snd.2 * z.coeff x_1.fst.2 =
    ∑ x_1 ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2,
      x.coeff x_1.fst.1 * (y.coeff x_1.snd.1 * z.coeff x_1.snd.2)

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)

Goal state after:
case hi
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) ∈
      (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2

case hj
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1

case left_neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    (match
        match a with
        | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩ with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) =
      a

case right_neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.2,
    (match
        match a with
        | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩ with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) =
      a

case h
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∀ a ∈ (antidiagonal ⋯ ⋯ b).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
    x.coeff a.snd.1 * y.coeff a.snd.2 * z.coeff a.fst.2 =
      x.coeff
          (match a with
              | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).fst.1 *
        (y.coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.1 *
          z.coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.2)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : CommSemiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ r • x • y = x • r • y

Tactic:
rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.inl
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₂ : y ≤ x ∨ y ≈ x
h₁ : x ≤ y
⊢ ⟦x⟧ = ⟦y⟧

Tactic:
cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case h
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
⊢ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g) ⊆ antidiagonal ⋯ ⋯ (f g)

pp: case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (f g),
    x_1 ∉ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g) →
      (embDomain f x).coeff x_1.1 * (embDomain f y).coeff x_1.2 = 0

Tactic:
· rintro ⟨i, j⟩ hij
      simp only [mem_map, mem_antidiagonal,
        Function.Embedding.coe_prodMap, mem_support, Prod.exists] at hij
      obtain ⟨i, j, ⟨hx, hy, rfl⟩, rfl, rfl⟩ := hij
      simp [hx, hy, hf]

Goal state after:
case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (f g),
    x_1 ∉ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g) →
      (embDomain f x).coeff x_1.1 * (embDomain f y).coeff x_1.2 = 0
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv.symm ⟨B, hle⟩ = ⊥
⊢ A = B ∨ B = ⊤

Tactic:
replace h := congr(primeSpectrumEquiv A $h)

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv (A.primeSpectrumEquiv.symm ⟨B, hle⟩) = A.primeSpectrumEquiv ⊥
⊢ A = B ∨ B = ⊤
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv.symm ⟨B, hle⟩ = ⊤
⊢ A = B ∨ B = ⊤

Tactic:
replace h := congr(primeSpectrumEquiv A $h)

Goal state after:
case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv (A.primeSpectrumEquiv.symm ⟨B, hle⟩) = A.primeSpectrumEquiv ⊤
⊢ A = B ∨ B = ⊤
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - 1) ≤ max (A.valuation (1 + (↑a - 1)) * A.valuation (↑b - 1)) (A.valuation (↑a - 1))

Tactic:
add_sub_cancel,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - 1) ≤ max (A.valuation ↑a * A.valuation (↑b - 1)) (A.valuation (↑a - 1))
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
ha : A.valuation (↑a - 1) < 1
⊢ A.valuation (↑a⁻¹ - 1) * A.valuation (1 + (↑a - 1)) < 1

Tactic:
add_sub_cancel,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
ha : A.valuation (↑a - 1) < 1
⊢ A.valuation (↑a⁻¹ - 1) * A.valuation ↑a < 1
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Subgroup G
⊢ ∀ (x : G), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s

Tactic:
refine fun a ↦ ⟨fun h ↦ ?_, fun ha b ↦ s.mul_mem_cancel_left ha⟩

Goal state after:
G : Type u_1
inst✝ : Group G
s : Subgroup G
a : G
h : ∀ (b : G), a • b ∈ ↑s ↔ b ∈ ↑s
⊢ a ∈ s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s

Tactic:
have : q a • q '' s = q '' (a • s) :=
    (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm

Goal state after:
case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' s ↔ a • s = s
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
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
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse[k - (List.replicate n 0).length]?

Tactic:
List.length_replicate,

Goal state after:
case neg
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
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) = (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse[k - n]?
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ d' ((aeval x) ((monomial n✝) a✝)) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs ((monomial n✝) a✝))) +
      (aeval x) (derivative ((monomial n✝) a✝)) • d' x

Tactic:
| monomial =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p = X ^ n + p.eraseLead

Tactic:
nth_rewrite 1 [← p.eraseLead_add_C_mul_X_pow]
    rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n

Tactic:
rw [natDegree_mul' h, hp.natDegree_eq] at this

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : m + q.natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
a b : R
⊢ (-(C a * X - C b)).natDegree < 2

Tactic:
rw [natDegree_neg]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
a b : R
⊢ (C a * X - C b).natDegree < 2
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ DenomsClearable a b N (C r * X ^ n) i

Tactic:
refine ⟨r * a ^ n * b ^ (N - n), bi, bu, ?_⟩
  rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]
  rw [map_mul, map_mul, map_pow, map_pow, eval_X, mul_comm]
  rw [← tsub_add_cancel_of_le nN]
  conv_lhs => rw [← mul_one (i a), ← bu]
  simp [mul_assoc, mul_comm, mul_left_comm, pow_add, mul_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ (p.reverse * X ^ p.natTrailingDegree).natDegree = p.natDegree

Tactic:
natDegree_mul',

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.natDegree + (X ^ p.natTrailingDegree).natDegree = p.natDegree

R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ∀ (N : ℕ), n - 1 < N → ((ofFn n) v).coeff N = 0

Tactic:
exact fun _ h ↦ ofFn_coeff_eq_zero_of_ge _ <| Nat.le_of_pred_lt h

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

Goal state before:
pp: case isUnit_or_isUnit.inr.inr.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.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inl (h3 g_dvd_f (by rwa [← hk]))

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

Goal state before:
pp: case monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ ((monomial 1) 1 * (monomial n) a).smeval x = x * ((monomial n) a).smeval x

Tactic:
monomial_mul_monomial,

Goal state after:
case monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ ((monomial (1 + n)) (1 * a)).smeval x = x * ((monomial n) a).smeval x
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case monomial
R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n✝ n : ℕ
a : R
⊢ ((monomial n✝) r * (monomial n) a).smeval x = r • (x ^ n✝ * a • x ^ n)

Tactic:
monomial_mul_monomial,

Goal state after:
case monomial
R : Type u_1
inst✝⁵ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n✝ n : ℕ
a : R
⊢ ((monomial (n✝ + n)) (r * a)).smeval x = r • (x ^ n✝ * a • x ^ 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
⊢ ((u + if k = m then v else 0) + if k = n then w else 0) = u

Tactic:
if_neg hkm.ne,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (u + 0 + if k = n then w else 0) = u
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
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)

Tactic:
have := support_trinomial_subset k m n (u : ℤ) v w hk

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, m, n}
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k✝)
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 * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 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:
if_neg hkm.ne,

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 * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 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
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: 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
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((monomial k) ↑u * (monomial k) ↑w + (monomial k) ↑u * (monomial (n - m + k)) ↑v +
                      (monomial k) ↑u * (monomial n) ↑u +
                    ((monomial m) ↑v * (monomial k) ↑w + (monomial m) ↑v * (monomial (n - m + k)) ↑v +
                      (monomial m) ↑v * (monomial n) ↑u) +
                  ((monomial n) ↑w * (monomial k) ↑w + (monomial n) ↑w * (monomial (n - m + k)) ↑v +
                    (monomial n) ↑w * (monomial n) ↑u)).toFinsupp.coeff) }

Tactic:
monomial_mul_monomial,

Goal state after:
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
⊢ C ↑v * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            ((monomial (k + k)) (↑u * ↑w) + (monomial (k + (n - m + k))) (↑u * ↑v) + (monomial (k + n)) (↑u * ↑u) +
                    ((monomial (m + k)) (↑v * ↑w) + (monomial (m + (n - m + k))) (↑v * ↑v) +
                      (monomial (m + n)) (↑v * ↑u)) +
                  ((monomial (n + k)) (↑w * ↑w) + (monomial (n + (n - m + k))) (↑w * ↑v) +
                    (monomial (n + n)) (↑w * ↑u))).toFinsupp.coeff) }
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 : ℤˣ
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) }
h :
  m + n = m' + n ∧ n - m + k + n = n - m' + k + n ∨
    ↑u = ↑w ∧ m + n = n - m' + k + n ∧ n - m + k + n = m' + n ∨
      ↑u + ↑w = 0 ∧ m + n = n - m + k + n ∧ m' + n = n - m' + k + n
⊢ q = p ∨ q = p.mirror

Tactic:
simp only [add_left_inj, Units.val_inj] at h

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 : ℤˣ
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) }
h : m = m' ∧ n - m = n - m' ∨ u = w ∧ m = n - m' + k ∧ n - m + k = m' ∨ ↑u + ↑w = 0 ∧ m = n - m + k ∧ m' = n - m' + k
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
wlog h_lC : 0 < leadingCoeff P generalizing P with H

Goal state after:
case h.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
H : ∀ {P : R[X]}, P ≠ 0 → P.natDegree = d → 0 < P.leadingCoeff → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
h_lC : ¬0 < P.leadingCoeff
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (y ◃ y) ◃⁻¹ y ◃ y = y

Tactic:
← left_cancel (y ◃ y),

Goal state after:
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ (y ◃ y) ◃ (y ◃ y) ◃⁻¹ y ◃ y = (y ◃ y) ◃ y
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 q.i * F q.j = F q.k

Tactic:
by rw [← map_mul, q.i_mul_j]

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

Goal state before:
pp: case ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ IntCast.intCast (Int.ofNat n) = IntCast.intCast (Int.ofNat n)

Tactic:
rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]

Goal state after:
case ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

Tactic:
refine (quo_add_sum_rem_mul_pow_inverse_unique (n := fun _ => 1)
      hg hcop hgi (fun i hi _ => hr₁ i hi) (fun i hi _ => hr₂ i hi) ?_).imp_right
      fun h i hi => congrFun (h i hi) 0

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree
hf : ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
⊢ (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i) * ((algebraMap R[X] K) (g i))⁻¹ ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i) * ((algebraMap R[X] K) (g i))⁻¹ ^ (↑j + 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

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

Tactic:
by
  classical ext x; by_cases hx : x = a <;> aesop (add norm coeff_single_apply)

Goal state after: