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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
⊢ p.natDegree < q.natDegree

Tactic:
by
  by_cases hq : q = 0
  · exact (not_lt_bot <| hq ▸ hpq).elim
  rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : q.degree < p.degree
⊢ max p.degree q.degree ≤ p.degree

Tactic:
max_eq_left_of_lt hlt

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : q.degree < p.degree
⊢ p.degree ≤ p.degree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0

Tactic:
refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
    rw [Finsupp.notMem_support_iff.mp h, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = 0

Tactic:
rw [← notMem_support_iff]

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
⊢ (single a (f a)).sum g ≤ f.sum g

Tactic:
rcases eq_or_ne (f a) 0 with H | H

Goal state after:
case inl
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a = 0
⊢ (single a (f a)).sum g ≤ f.sum g

case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ (single a (f a)).sum g ≤ f.sum g
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : M → N
hg : g 0 = 0
h : 0 ≤ fun x ↦ g x
a : α
⊢ g (f a) ≤ f.sum fun x m ↦ g m

Tactic:
by
  simp only [← sum_single_index (h := fun (_ : α) m ↦ g m) (a := a) (b := f a) hg]
  apply single_le_sum _ (fun _ m ↦ h m)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Tactic:
let _ := invertibleOne (α := R)

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Tactic:
let _ := invertibleOne (α := R)

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) p

Tactic:
rw [← comp_eval₂Hom]

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (φ.comp (eval₂Hom f g)) p
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ Pi.Lex r (fun {i} x1 x2 ↦ x1 < x2) ⇑x ⇑y

Tactic:
by
  simp_rw [Pi.Lex, le_antisymm_iff]
  exact lex_lt_of_lt_of_preorder r hlt

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsRegular ((MvPolynomial.monomial m) a)

Tactic:
← isLeftRegular_iff_isRegular

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsLeftRegular ((MvPolynomial.monomial m) a)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsLeftRegular (X n)

Tactic:
intro P Q (hPQ : (X n) * P = (X n) * Q)

Goal state after:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
⊢ P = Q
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
⊢ (rename id) p = p

Tactic:
rename_id_apply

Goal state after:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
⊢ p = p
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
⊢ (rename id) p = p

Tactic:
rename_id_apply

Goal state after:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
⊢ p = p
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)

Tactic:
intro x hx y hy k

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ coeff k (x * y) ∈ M * N
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d ((rename f) φ) = 0

Tactic:
rw [← notMem_support_iff]

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ d ∉ ((rename f) φ).support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
⊢ degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d

Tactic:
by
  rw [degreeOf_eq_sup, Finset.sup_le_iff]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (eval₂Hom (φ.comp (algebraMap R S₁)) fun i ↦ φ (g i)) p

Tactic:
rw [← comp_eval₂Hom]

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (φ.comp (eval₂Hom (algebraMap R S₁) g)) p
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then ⊥ else 0) = 0

Tactic:
bot_eq_zero',

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then 0 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
a : R
⊢ (f * C a).natDegree ≤ f.natDegree

Tactic:
by
  simpa using natDegree_mul_le (q := C a)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
refine Finset.le_min fun n hn => ?_
  rw [mem_support_iff, coeff_mul] at hn
  obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
  refine
    (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_
  rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Tactic:
rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (C (f.coeff 0)).eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.natDegree < n

Tactic:
eraseLead_natDegree_le,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.natDegree - 1 < n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.Nf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

Tactic:
exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

Tactic:
exact add_comm _ _

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

Goal state before:
pp: case monomial.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ coeff m (∏ x, X x ^ j x.succ) = 0

Tactic:
have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction

Goal state after:
case monomial.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
hmj : m ≠ j.tail
⊢ coeff m (∏ x, X x ^ j x.succ) = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.sum.natDegree ≤ List.foldr max 0 (List.map natDegree l)

Tactic:
apply List.sum_le_foldr_max natDegree
  · simp
  · exact natDegree_add_le

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

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

Tactic:
· rintro ⟨m, h, rfl⟩
    exact ⟨tail m, by simpa using h⟩

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

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) 0).sum

Tactic:
simp only [Multiset.notMem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
      Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]

Goal state after:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) 0).sum

pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) (a ::ₘ t)).sum

Tactic:
· simp only [Multiset.notMem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
      Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]
    rw [← C_1]
    rw [nextCoeff_C_eq_zero]

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) (a ::ₘ t)).sum
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
⊢ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i.castSucc <
    Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
rw [Fin.strictMono_castSucc.injective.extend_apply]

Goal state after:
case succ.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
⊢ k i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j
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
⊢ f (n + 1) i = y * f n i

Tactic:
dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0

Tactic:
· rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin n
⊢ Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i.castSucc ≠ 0

Tactic:
rw [Fin.strictMono_castSucc.injective.extend_apply]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin n
⊢ x i ≠ 0
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ span R ↑t

Tactic:
rw [ht]
          exact hx

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
S : Subalgebra R A
⊢ P S

Tactic:
obtain ⟨t, rfl⟩ := S.fg_of_noetherian

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑t)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ f ∈ map C I

Tactic:
rw [← sum_monomial_eq f]

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ (f.sum fun n a ↦ (monomial n) a) ∈ map C I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this : C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit r

Tactic:
rw [← constantCoeff_C _ r]
        exact h.map _

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ adjoin S (Set.range MvPolynomial.X) = ⊤

Tactic:
exact MvPolynomial.adjoin_range_X

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

Goal state before:
pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
a✝ : m ∈ f.support
⊢ C (coeff m f) * (monomial m) 1 ∈ Ideal.map C I

Tactic:
suffices C (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Ideal.mul_mem_right _ _ this

Goal state after:
case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
a✝ : m ∈ f.support
⊢ C (coeff m f) ∈ Ideal.map C I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a : ℤ
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a

Tactic:
rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]

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

Goal state before:
pp: case mp
m n : ℕ
⊢ ¬m.Coprime n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

pp: case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n

Tactic:
· intro h
    exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩

Goal state after:
case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
a : R
I : Ideal R
⊢ a • ⊤ = R ∙ Submodule.Quotient.mk a

Tactic:
simp [← Ideal.Quotient.span_singleton_one, Algebra.smul_def, Submodule.smul_span]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.prev x ⋯ = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.next x hx = l'.next x ⋯

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.next l[k] hx = l'.next l[k] ⋯
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n

Tactic:
by
  simp [hn]

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors

Tactic:
by
  grind [dvd_gcd_iff]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

Tactic:
← inv_mem_iff (x := a),

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a⁻¹ ∉ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.index

Tactic:
by
  rw [← relIndex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ a.val < 0

Tactic:
cases NeZero.ne 0 rfl

Goal state after: