mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
v : ℕ
hv : v ≠ 1
hr : CharP R v
h : ↑1 = 0
⊢ v = 1

Tactic:
rwa [CharP.cast_eq_zero_iff _ v, Nat.dvd_one] at h

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
⊢ n.minFac = 2 ↔ 2 ∣ n

Tactic:
by
  constructor
  · intro h
    rw [← h]
    exact minFac_dvd n
  · intro h
    have ub := minFac_le_of_dvd (le_refl 2) h
    have lb := minFac_pos n
    refine ub.eq_or_lt.resolve_right fun h' => ?_
    suffices n.minFac = 1 by simp_all
    exact (le_antisymm (Nat.succ_le_of_lt lb) (Nat.lt_succ_iff.mp h')).symm

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsRegular (X ^ n)

Tactic:
suffices IsLeftRegular (X ^ n : R[X]) from
    ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩
  intro P Q (hPQ : X ^ n * P = X ^ n * Q)
  ext i
  rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsRegular (X ^ n)

Tactic:
by
  suffices IsLeftRegular (X ^ n : R[X]) from
    ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩
  intro P Q (hPQ : X ^ n * P = X ^ n * Q)
  ext i
  rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ (cons a s has).sup fun b ↦ (f b).degree

Tactic:
sup_cons

Goal state after:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ max (f a).degree (s.sup fun b ↦ (f b).degree)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
⊢ p.coeff (i, j).1 * 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
by simp [hp]

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
⊢ 0 = 0 - 0

Tactic:
tsub_self

Goal state after:
case inr
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
i : ι
a b : α
j : ι
h : j ≠ i
⊢ 0 = 0
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : (i : ι) → LT (β i)
r : ι → ι → Prop
inst✝ : Std.Irrefl r
x y : (i : ι) → β i
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) x y ↔ x default < y default

Tactic:
by
  simp [Pi.Lex, Unique.forall_iff, Unique.exists_iff, irrefl]

Goal state after:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : j ≠ i
⊢ 0 = 0 - 0

Tactic:
tsub_self

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : j ≠ i
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q.leadingCoeff • P = 0

Tactic:
simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f + -g).neLocus (g + -g) = (f - g).support

Tactic:
add_neg_cancel,

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f + -g).neLocus 0 = (f - g).support
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case C
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
a✝ : R
⊢ C a✝ ∈ S

Tactic:
exact S.algebraMap_mem _

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
d : σ →₀ ℕ
hd : d ≠ d₀
⊢ coeff d φ = coeff d ((monomial d₀) (coeff d₀ φ))

Tactic:
· rw [notMem_support_iff.mp fun hmem ↦ hd (h d hmem), coeff_monomial, if_neg fun e ↦ hd e.symm]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (p.coeff.sum fun n b ↦ (monomial (0 + n)) (a * b)) = a * coeff m p

pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ (p.coeff.sum fun n b ↦ (monomial (0 + n)) (0 * b)) = 0

Tactic:
· simp +contextual [sum_def, coeff_sum]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ (p.coeff.sum fun n b ↦ (monomial (0 + n)) (0 * b)) = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := ⋯
ψ : MvPolynomial σ R := ⋯
⊢ φ = MvPolynomial.C r * ψ

Tactic:
apply MvPolynomial.ext

Goal state after:
case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := ⋯
ψ : MvPolynomial σ R := ⋯
⊢ ∀ (m : σ →₀ ℕ), coeff m φ = coeff m (MvPolynomial.C r * ψ)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mp
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M

Tactic:
rintro hp j
    simpa using hp (j + i)

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ Multiset.toFinset 0 = ∅

Tactic:
Multiset.toFinset_zero

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∅ = ∅
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
inst✝ : CommSemiring R
⊢ Multiset.toFinset 0 = ∅

Tactic:
Multiset.toFinset_zero

Goal state after:
R : Type u
σ : Type u_1
r : R
inst✝ : CommSemiring R
⊢ ∅ = ∅
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf i ((monomial s) a) = s i

Tactic:
by
  classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = p.support.sup fun m ↦ (toMultiset m).card

Tactic:
rw [totalDegree]
  congr; funext m
  exact (Finsupp.card_toMultiset _).symm

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ (p.support.sup fun m ↦ (toMultiset m).card) ≤ q.totalDegree

Tactic:
hb₂,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ (toMultiset b).card ≤ q.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ p.support ∧ b ∉ q.support

Tactic:
exact ⟨hb₁, hb⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ (p.support.sup fun m ↦ (toMultiset m).card) ≤ (p + q).totalDegree

Tactic:
hb₂,

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ (toMultiset b).card ≤ (p + q).totalDegree
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degreesLE R σ 0 = 1

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (by simp)
  simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx
  have := (totalDegree_eq_zero_iff_eq_C (p := x)).mp
    (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))
  exact ⟨x.coeff 0, by simp [Algebra.smul_def, ← this]⟩

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hp, trailingCoeff_zero, zero_mul]

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

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = (revAt (n + n')) n + (revAt (o + o')) o

Tactic:
rw [revAt_le (le_add_right rfl.le)]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (revAt (o + o')) o
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (revAt (o + o')) o

Tactic:
rw [revAt_le (le_add_right rfl.le)]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)

Tactic:
rw [revAt_le (le_add_right rfl.le)]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + (o + (n' + o')))) (n + o) = n + n' - n + (o + o' - o)

Tactic:
← add_assoc,

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + o + (n' + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case add
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
f g : MvPolynomial σ R
hf : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) f) = eval₂ φ a f
hg : Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) g) = eval₂ φ a g
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) (f + g)) = eval₂ φ a (f + g)

Tactic:
simp only [eval₂_add, Polynomial.eval₂_add, hf, hg]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    Polynomial.C (C r * m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none

Tactic:
simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
      map_mul, mul_assoc]

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ Polynomial.C (C r) * (Polynomial.X ^ m none * m.some.prod fun a k ↦ Polynomial.C (X a) ^ k) =
    Polynomial.C (C r) * (Polynomial.C (m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key : p.natDegree = 0 ∨ q.natDegree = 0
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
⊢ (∃ x, ¬coeff x (((optionEquivLeft R σ) p).coeff i) = 0) →
    ∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i

Tactic:
rintro ⟨m, hm⟩

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
m : σ →₀ ℕ
hm : ¬coeff m (((optionEquivLeft R σ) p).coeff i) = 0
⊢ ∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.comp (-X) ≠ 0

Tactic:
by simp [hp]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree ≠ 0

Tactic:
by simp [hp]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0) → ∃ a, ¬coeff a f = 0 ∧ a 0 = i

Tactic:
rintro ⟨m, hm⟩

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ¬coeff (cons i m) f = 0
⊢ ∃ a, ¬coeff a f = 0 ∧ a 0 = i
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ (x + y) ^ i * y ^ (n - (1 + i) + (1 + i) - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ (x + y) ^ i * y ^ (n - (1 + i) + 1 + i - i) = (x + y) ^ i * y ^ (n - (1 + i) + 1)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
neg_sub,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = ∑ x ∈ range n, if i = x then ↑(n.choose (x + 1)) else 0

Tactic:
rw [Finset.sum_eq_single i, if_pos rfl]

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ∀ b ∈ range n, b ≠ i → (if i = b then ↑(n.choose (b + 1)) else 0) = 0

case h₁
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ i ∉ range n → (if i = i then ↑(n.choose (i + 1)) else 0) = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

Tactic:
induction n generalizing i with
  | zero => dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
  | succ n ih =>
    simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
      Nat.cast_add, coeff_X_add_one_pow]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
s : Set σ
p : MvPolynomial (↑s) R
⊢ Prime ((rename Subtype.val) p) ↔ Prime p

Tactic:
by
  classical
    symm
    let eqv :=
      (sumAlgEquiv R (↥sᶜ) s).symm.trans
        (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)
    have : rename Subtype.val = eqv.toAlgHom.comp (Algebra.algHom _ (MvPolynomial s R) _) := by
      apply algHom_ext
      simp [eqv, rename, X, monomial, Algebra.algHom, renameEquiv, Finsupp.mapDomain.addMonoidHom,
        sumAlgEquiv, C]
    apply_fun (· p) at this
    simpa [this, MulEquiv.prime_iff, Algebra.algHom] using (prime_C_iff _).symm

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A ↔ ∃ ι x f, Surjective ⇑f

Tactic:
constructor
  · rw [iff_quotient_freeAlgebra]
    rintro ⟨s, f, hsur⟩
    use { x : A // x ∈ s }, inferInstance, f
  · rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ((aeval f) (p' * p)) v + ((aeval f) (q * q')) v = v

Tactic:
mul_comm q q'

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ((aeval f) (p' * p)) v + ((aeval f) (q' * q)) v = v
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n

Tactic:
rw [← Int.ofNat_inj]

Goal state after:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b m n : ℤ
hmn : m.natAbs.Coprime n.natAbs
⊢ a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

Tactic:
by
  convert! ← modEq_and_modEq_iff_modEq_lcm using 1
  rw [lcm_eq_mul_iff.mpr (.inr <| .inr hmn), ← natAbs_mul, modEq_natAbs]

Goal state after:
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + (a + b) = b

Tactic:
← add_assoc,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + a + b = b
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
x y : R
h : x + y = 0
⊢ x = y

Tactic:
CharTwo.add_eq_zero

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
x y : R
h : x = y
⊢ x = y
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
hf : Pairwise (IsCoprime on f)
⊢ I ⊓ J = ⨅ i, f i

Tactic:
by simp [f, iInf, inf_comm]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
ha : x = p
this : 1 ∣ p
⊢ x = p ∧ y = p

Tactic:
subst ha

Goal state after:
case inl
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h✝ : x✝ * y✝ = x ^ 2
pdvdxy : x ∣ x✝ * y✝
h : x * y = x ^ 2
this : 1 ∣ x
⊢ x = x ∧ y = x
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inr
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x✝ * y✝ = a ^ 2
pdvdxy : a ∣ x✝ * y✝
h : x * y = a ^ 2
ha : x = a * a
this : a ∣ a
⊢ y = 1

Tactic:
subst ha

Goal state after:
case inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : a * a * y = a ^ 2
⊢ y = 1
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
have hpd : p ^ (k + l) * p ∣ m * n := by
      let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
      rwa [pow_succ'] at hpmn'
  have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
  have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
  have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
  have hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l :=
    (Prime.dvd_mul p_prime).1 hpd4
  suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ, _root_.pow_succ]
  exact hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
    fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n * (minimalPeriod f x / (minimalPeriod f x).gcd n)] x = x

Tactic:
← Nat.mul_div_assoc _ (gcd_dvd_left _ _),

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n * minimalPeriod f x / (minimalPeriod f x).gcd n] x = x