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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal (b +ᵥ a) ⋯, ((single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 = 0

Tactic:
rw [sum_congr _ fun _ _ => rfl, sum_empty]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ VAddAntidiagonal (b +ᵥ a) ⋯ = ∅
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr
S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
hn : n ≠ 0
⊢ 0 ≤ mk ↑n

Tactic:
rw [mk_intCast hn]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
⊢ ∑ x_1 ∈ antidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = 0

Tactic:
rw [sum_congr _ fun _ _ => rfl, sum_empty]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
⊢ antidiagonal ⋯ ⋯ (a + b) = ∅
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ ((single b) r * x).coeff a = r * x.coeff (a - b)

Tactic:
by
  simpa using coeff_single_mul_add (a := a - b) (b := b)

Goal state after:
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
r : R
x : R⟦Γ⟧
a : Γ
⊢ (x * (single 0) r).coeff a = x.coeff a * r

Tactic:
rw [← add_zero a, coeff_mul_single_add, add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
⊢ ∀ (c : R) {x : R}, x ∈ P.supportAddSubgroup.carrier → c • x ∈ P.supportAddSubgroup.carrier

Tactic:
simpa using smul_mem_support P

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
⊢ mk x ≤ mk y → ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

Tactic:
rintro ⟨(_ | n), hn⟩
    · simp_all [exists_zero_lt]
    · obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)
      refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
      simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)

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 : Γ
i j : Γ'
hij : ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (i, j)
⊢ (i, j) ∈ antidiagonal ⋯ ⋯ (f g)

Tactic:
obtain ⟨i, j, ⟨hx, hy, rfl⟩, rfl, rfl⟩ := hij

Goal state after:
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⟦Γ⟧
i j : Γ
hx : x.coeff i ≠ 0
hy : y.coeff j ≠ 0
⊢ (f.toEmbedding i, f.toEmbedding j) ∈ antidiagonal ⋯ ⋯ (f (i + j))
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ ¬∃ y, ↑y - k • x ∈ ball K c

Tactic:
contrapose h

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ∃ y, ↑y - k • x ∈ ball K c
⊢ ∃ y, ↑y - x ∈ ball K c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

Tactic:
use (0, 1); simp [h]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
⊢ IsUnit a

Tactic:
have ha : (a : K) ≠ 0 := by
      intro c
      rw [c, A.valuation.map_zero] at h
      exact zero_ne_one h

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ IsUnit a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  (OrderDual.ofDual.trans A.primeSpectrumEquiv) (OrderDual.toDual a) ≤
    (OrderDual.ofDual.trans A.primeSpectrumEquiv) (OrderDual.toDual b)
⊢ OrderDual.toDual a ≤ OrderDual.toDual b

Tactic:
by
        simp only [OrderDual.toDual_le_toDual]
        dsimp at h
        have := idealOfLE_le_of_le A _ _ ?_ ?_ h
        · rwa [idealOfLE_ofPrime, idealOfLE_ofPrime] at this
        all_goals exact le_ofPrime A (PrimeSpectrum.asIdeal _)

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

Goal state before:
pp: case refine_1
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
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
j : FiniteArchimedeanClass M
⊢ j < FiniteArchimedeanClass.mk (↑y - x) hxy0 → (ofLex (f.eval x)).coeff j = (ofLex (↑↑f y)).coeff j

Tactic:
hj

Goal state after:
case refine_1
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
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
j : FiniteArchimedeanClass M
hj : j < FiniteArchimedeanClass.mk (↑y - x) hxy0
⊢ (ofLex (f.eval x)).coeff j = (ofLex (↑↑f y)).coeff j
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this✝ : ↑z ≠ x
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) < ArchimedeanClass.mk (x - ↑z)

Tactic:
ArchimedeanClass.mk_sub_comm x z.val

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this✝ : ↑z ≠ x
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) < ArchimedeanClass.mk (↑z - x)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

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

Tactic:
simpa [le_antisymm_iff, principalUnitGroup_le_principalUnitGroup] using h.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (min a b).untop₀ = min a.untop₀ b.untop₀

Tactic:
by
  lift a to α using ha
  lift b to α using hb
  norm_cast

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
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
⊢ ↑b ∈ {r | x < f r}

Tactic:
by simpa using hb

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

Goal state before:
pp: case neg.inr
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
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ ¬∃ y, ↑y - x ∈ ball K d

Tactic:
contrapose h

Goal state after:
case neg.inr
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
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
h : ∃ y, ↑y - x ∈ ball K d
⊢ ∃ y, ↑y - x ∈ ball K c
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
h : x ≠ 0
⊢ (C x).coeffList = [x]

Tactic:
by
  simp [coeffList, List.range_succ, degree_eq_natDegree (C_ne_zero.mpr h)]

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

Goal state before:
pp: case pos.refine_1
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
i : ℕ
h✝ : deg(p) - deg(q) ≤ i
⊢ q.coeff (i - (deg(p) - deg(q))) ∈ span R coeffs(q)

Tactic:
exact subset_span ⟨_, rfl⟩

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

Goal state before:
pp: case pos.refine_2
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
i : ℕ
h✝ : deg(p) - deg(q) ≤ i
⊢ p.leadingCoeff ∈ span R coeffs(p)

Tactic:
exact subset_span ⟨_, rfl⟩

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

Goal state before:
pp: case monomial.monomial
R : Type u_2
inst✝ : CommRing R
n m : ℕ
a : R
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) ((monomial n) ((monomial m) a))) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs ((monomial n) ((monomial m) a))))

Tactic:
| monomial m a =>

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

Goal state before:
pp: case monomial.monomial
R : Type u_1
inst✝ : CommSemiring R
n m : ℕ
a : R
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) ((monomial m) a))) =
    (equivMvPolynomial R) (derivative ((monomial n) ((monomial m) a)))

Tactic:
| monomial m a =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
⊢ (p - q).natDegree < n

Tactic:
rw [← sub_sub_sub_cancel_right p q (X ^ n)]

Goal state after:
R : Type u_1
inst✝ : Ring R
p q : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
⊢ (p - X ^ n - (q - X ^ n)).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:
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.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
⊢ (-r).natDegree < m

Tactic:
natDegree_neg

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
⊢ r.natDegree < m
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v ≠ 0
⊢ n ≠ 0

Tactic:
contrapose h

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ (ofFn n) v = 0
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: 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
⊢ (X ^ 0 * p).smeval x = x ^ 0 * p.smeval x

Tactic:
by
    simp [npow_zero, one_mul]

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

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

Tactic:
← iterate_derivative_map

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

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

Tactic:
← iterate_derivative_map

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 ((⇑derivative)^[q] (map (algebraMap R A) p)) = q ! • eval r p'
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 : ℕ
h :
  ∀ (k : ℕ),
    ∃ gp,
      gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) gp

Tactic:
choose c h using h

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 : ℕ
c : ℕ → R[X]
h :
  ∀ (k : ℕ),
    (c k).natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) gp
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case refine_2
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
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
⊢ j ∈ s → ((r₁ j - r₂ j) * ∏ k ∈ s.erase j, g k).degree < (∏ i ∈ s, g i).degree

Tactic:
hj

Goal state after:
case refine_2
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
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (r₂ i - r₁ i - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
j : ι
hj : j ∈ s
⊢ ((r₁ j - r₂ j) * ∏ k ∈ s.erase j, g k).degree < (∏ i ∈ s, g i).degree
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ AddCommMonoid (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addCommMonoid _ rfl ?_ ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoid R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x
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
w : QuadraticAlgebra R a b
⊢ (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w =
    ((LinearMap.toMatrix (basis a b) (basis a b)).symm !![z.re, a * z.im; z.im, z.re + b * z.im]) w

Tactic:
apply basis .. |>.repr.injective

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
w : QuadraticAlgebra R a b
⊢ (basis a b).repr ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) w) =
    (basis a b).repr (((LinearMap.toMatrix (basis a b) (basis a b)).symm !![z.re, a * z.im; z.im, z.re + b * z.im]) w)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
i : ι
hi : i ∈ s
⊢ r i * ∏ k ∈ s.erase i, g k ^ n k = q' i * ∏ i ∈ s, g i ^ n i + ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
rw [← Finset.mul_prod_erase s _ hi, hr i hi, add_mul, Finset.sum_mul, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Quandle

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

Tactic:
apply (act' x).symm.injective

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

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

Tactic:
cases a

Goal state after:
case zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
b c : WithZero α
⊢ 0 * (b + c) = 0 * b + 0 * c

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