mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ofLex (seed.baseEmbedding.toFun ⟨f'.sum fun d x ↦ ↑x, ⋯⟩) =
    ofLex (toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))))

Tactic:
rw [ofLex_toLex, LinearPMap.toFun_eq_coe]

Goal state after:
case refine_2
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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩) = (truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LE α
⊢ ∀ (a₁ b₁ a₂ b₂ : α),
    a₁ ≈ a₂ →
      b₁ ≈ b₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) a₁ b₁ = Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) a₂ b₂

Tactic:
refine fun x₁ x₂ y₁ y₂ hx hy ↦ propext ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂

case refine_2
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
⊢ (single a) r * (single b) s = (single (a + b)) (r * s)

Tactic:
by
  ext x
  by_cases h : x = a + b
  · rw [h, coeff_mul_single_add]
    simp
  · rw [coeff_single_of_ne h, coeff_mul, sum_eq_zero]
    simp_rw [mem_antidiagonal]
    rintro ⟨y, z⟩ ⟨hy, hz, rfl⟩
    rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h
    exact (h rfl).elim

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case h
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - k • x ∈ ball K c
heq : ↑(k⁻¹ • y) - x = k⁻¹ • (↑y - k • x)
⊢ ↑(k⁻¹ • y) - x ∈ ball K c

Tactic:
exact heq ▸ Submodule.smul_mem _ _ hy

Goal state after:
Module: Mathlib.Algebra.Order.Star.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : NonUnitalSemiring α
inst✝⁶ : NonUnitalSemiring β
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : StarRing α
inst✝² : StarRing β
inst✝¹ : StarOrderedRing α
inst✝ : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ closure (Set.range fun s ↦ star s * s) = closure (Set.range fun p ↦ (star p.1 * p.1, star p.2 * p.2))

Tactic:
Prod.mul_def,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : NonUnitalSemiring α
inst✝⁶ : NonUnitalSemiring β
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : StarRing α
inst✝² : StarRing β
inst✝¹ : StarOrderedRing α
inst✝ : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ closure (Set.range fun s ↦ ((star s).1 * s.1, (star s).2 * s.2)) =
    closure (Set.range fun p ↦ (star p.1 * p.1, star p.2 * p.2))
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
⊢ A ≤ B

Tactic:
x

Goal state after:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
⊢ x ∈ A → x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
⊢ A ≤ B

Tactic:
x

Goal state after:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
⊢ x ∈ A → x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
⊢ B.nonunits ≤ A.nonunits

Tactic:
x

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
⊢ x ∈ B.nonunits → x ∈ A.nonunits
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) < 1

Tactic:
lhs
      rw [← mul_one (A.valuation _), ← A.valuation.map_one_add_of_lt ha]

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 (1 + (↑a - 1))
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
⊢ A ≤ B

Tactic:
x

Goal state after:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
⊢ x ∈ A → x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
⊢ B.principalUnitGroup ≤ A.principalUnitGroup

Tactic:
x

Goal state after:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
⊢ x ∈ B.principalUnitGroup → x ∈ A.principalUnitGroup
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
x : FiniteElement K
⊢ ∃ n, x ≤ ↑n

Tactic:
by
    obtain ⟨n, hn⟩ := x.2
    refine ⟨n, (le_abs_self x).trans ?_⟩
    simpa using! hn

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
⊢ (aevalAeval x y) (C X) = x

Tactic:
aevalAeval_C,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
⊢ (aeval x) X = x
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)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
⊢ 0 < ↑(sSupFun hc) (y - x)

Tactic:
obtain hyx := (y - x).prop

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)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ (sSupFun hc).domain
⊢ 0 < ↑(sSupFun hc) (y - x)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: 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)
⊢ spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤
    spanCoeffs(q) ^ deg(r) * (1 ⊔ (span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)))

Tactic:
by gcongr

Goal state after:
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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).1.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).1

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ C a * X ^ (n - n) * X ^ n = C a * X ^ n

Tactic:
tsub_self,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ C a * X ^ 0 * X ^ n = C a * X ^ n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ ((monomial n) a).mirror = (monomial n) a

Tactic:
· rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

Tactic:
rw [Finset.mem_range_succ_iff] at *

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

Tactic:
rw [Finset.mem_range_succ_iff] at *

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n
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
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
⊢ h ∣ -k.mirror

Tactic:
dvd_neg

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
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
⊢ h ∣ k.mirror
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
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
⊢ g ∣ -k

Tactic:
dvd_neg

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
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
⊢ g ∣ k
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun₀ | 0 => n | 1 => p.natDegree - n) ∈ (p.homogenize p.natDegree).support

Tactic:
simpa [coeff_homogenize, mem_support_iff.mp hn]
      using Nat.add_sub_of_le <| le_natDegree_of_mem_supp n hn

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

Goal state before:
pp: 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
⊢ (C r * p).smeval x = r • p.smeval x

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, smeval_add, ph, qh, smul_add]
  | monomial n b => simp only [C_mul_monomial, smeval_monomial, mul_smul]

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
⊢ (X * (monomial n) a).smeval x = x * ((monomial n) a).smeval x

Tactic:
← monomial_one_one_eq_X,

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) 1 * (monomial n) a).smeval x = x * ((monomial n) a).smeval x
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: ⊢ X + 1 = X + ↑1

Tactic:
Nat.cast_one

Goal state after:
⊢ X + 1 = X + 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]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
⊢ (aeval r) ((⇑derivative)^[k] p) = 0

Tactic:
have h (x) : (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1) := by
    rw [← pow_add, add_tsub_cancel_of_le]
    rw [Nat.lt_iff_add_one_le] at hk
    exact (le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)

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)
⊢ (aeval r) ((⇑derivative)^[k] p) = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
rw [trinomial_trailing_coeff' hkm hmn]

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'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p' +
        q ! • (X - C r) ^ (q - q) * (⇑derivative)^[0] p') =
    q ! • eval r p'

Tactic:
tsub_self,

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 r
      (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p' +
        q ! • (X - C r) ^ 0 * (⇑derivative)^[0] p') =
    q ! • eval r p'
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 : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
· have h₂ : nextCoeff P ≠ 0 := by intro; simp_all
    obtain ⟨_, hl⟩ := coeffList_eq_cons_leadingCoeff (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂)
    simp [signVariations, List.destutter, leadingCoeff_eraseLead_eq_nextCoeff h₂, hl, h, h₂,
      coeffList_eraseLead hpz]

Goal state after:
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
⊢ n + (n - m + k) < n + n

Tactic:
by gcongr

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)
⊢ (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)

Tactic:
← zero_add ((q - 1)! • p'.eval r)

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)
⊢ (aeval r) (sumIDeriv p) = 0 + (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)
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 ∈ range (q - 1), (aeval r) ((⇑derivative)^[x] p) + (aeval r) ((⇑derivative)^[q - 1] p) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) =
    0 + (q - 1)! • eval r p' + q ! • ∑ x ∈ Ico q (p.natDegree + 1), (aeval r) (c x)

Tactic:
congr 2
    · apply sum_eq_zero
      exact fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)
    · rw [← aeval_iterate_derivative_self _ _ _ hp]
    · rw [smul_sum, sum_congr rfl]
      intro k hk
      exact hc k (mem_Ico.mp hk).1 r

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
⊢ ((LinearMap.toMatrix (basis a b) (basis a b)) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z)).det = norm z

Tactic:
convert! this

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
z : QuadraticAlgebra R a b
this : !![z.re, a * z.im; z.im, z.re + b * z.im].det = norm z
⊢ (LinearMap.toMatrix (basis a b) (basis a b)) (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) =
    !![z.re, a * z.im; z.im, z.re + b * z.im]
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), x * r = 0 → x = 0

Tactic:
x

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
⊢ x * r = 0 → x = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℕ
⊢ trace ↑n = 2 * ↑n

Tactic:
simp [trace_def, re_natCast, im_natCast]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z ^ 2 - trace z • z + (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 0

Tactic:
rw [Algebra.smul_def, algebraMap_trace_eq_add_star, algebraMap_norm_eq_mul_star]; ring

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝ : Quandle Q
n : ℕ
⊢ ∀ {x y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)

Tactic:
intro x y z
    simp only [dihedralAct]
    ring_nf

Goal state after: