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

Goal state before:
pp: R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)

Tactic:
refine s.induction ?_ ?_
  · rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
    split_ifs; exacts [bot_le, hzero.le]
  · intro i s his ih
    rw [Finset.prod_insert his, Finset.sum_insert his]
    exact (supDegree_mul_le hadd).trans (by gcongr)

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ (n + 1)).degree ≤ ↑(n + 1) * a

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, pow_succ]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ ↑n * a
⊢ (p ^ n * p).degree ≤ ↑n * a + a
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).coeff = ⇑f ∘ p.coeff

Tactic:
ext n; exact coeff_map ..

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - C a ≠ 0

Tactic:
rw [sub_eq_add_neg, ← map_neg C a]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + C (-a) ≠ 0
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a

Tactic:
rcases H with ⟨n, hn⟩

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ ∃ n a, f = (monomial n) a
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ (y + 1 - 1)

Tactic:
Nat.add_sub_cancel

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ y = ↑((d + 1).choose (y + 1)) * ↑(y + 1) * y✝ ^ y
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p

Tactic:
by
  apply MvPolynomial.induction_on p <;>
    simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ ∃ j ∈ p.support, j + s = m

Tactic:
by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∑ i ∈ s, f i).degrees ≤ s.sup fun i ↦ (f i).degrees

Tactic:
by
  simp_rw [degrees_def]; exact supDegree_sum_le

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₁
f : R →+* S₁
hf : Injective ⇑f
⊢ Injective ⇑(map f)

Tactic:
intro p q h
  simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢
  intro m
  exact hf (h m)

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d (p + q) ≠ 0

Tactic:
coeff_add

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d p + coeff d q ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ (rename Subtype.val) q = (rename Subtype.val) ((rename ⇑e.symm) ((rename ⇑e) q))

Tactic:
rename_rename e

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ (rename Subtype.val) q = (rename Subtype.val) ((rename (⇑e.symm ∘ ⇑e)) q)
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
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Tactic:
Submodule.mul_le

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
⊢ ∀ m ∈ coeffsIn σ M, ∀ n ∈ coeffsIn σ N, m * n ∈ coeffsIn σ (M * N)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
inst✝ : CommSemiring R
⊢ (C r).vars = ∅

Tactic:
by
  classical rw [vars_def, degrees_C, Multiset.toFinset_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ((monomial (Finsupp.single n 1)) 1).vars = {n}

Tactic:
vars_monomial (one_ne_zero' R),

Goal state after:
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (Finsupp.single n 1).support = {n}
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ d ∉ (p - ((monomial d) c - (monomial d') c)).support

Tactic:
classical
  rw [notMem_support_iff, coeff_sub, coeff_sub, coeff_monomial, coeff_monomial,
    if_pos rfl, if_neg hdd'.symm, sub_zero, hc, sub_self]

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

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
⊢ cons 0 (single i y) = single i.succ y

Tactic:
ext j
  cases j using Fin.cases <;> simp [single_apply]

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

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
h : y ≠ 0
⊢ cons y s ≠ 0

Tactic:
by
  contrapose h with c
  rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))

Tactic:
coeff_C

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = if 0 = m then coeff 0 p else 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧ degreesLE R σ s * degreesLE R σ t ≤ degreesLE R σ (s + t)

Tactic:
Submodule.mul_le

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧
    ∀ m ∈ degreesLE R σ s, ∀ n ∈ degreesLE R σ t, m * n ∈ degreesLE R σ (s + t)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ leadingCoeff (⇑toLex) p = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
by
  rw [leadingCoeff]
  apply congr_arg p.coeff
  apply toLex.injective
  rw [Function.rightInverse_invFun toLex.surjective, toLex_ofLex]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
⊢ p.natDegree ≤ n + 1 - 1

Tactic:
refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff (n + 1) = 0
h : p.natDegree = n.succ
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (p * C a).natDegree = p.natDegree

Tactic:
by
  refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_
  refine mem_support_iff.mpr ?_
  rwa [coeff_mul_C]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
rw [degree_mul' (by simpa)]; simp [left_ne_zero_of_mul h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ nextCoeffUp 0 = 0

Tactic:
simp [nextCoeffUp]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
⊢ (p + q).eraseLead = p.eraseLead + q

Tactic:
ext n
  by_cases nd : n = p.natDegree
  · rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_degree_lt pq).symm]
    simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm
  · rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
    rintro rfl
    exact nd (natDegree_add_eq_left_of_degree_lt pq)

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

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * (C g.leadingCoeff * X ^ (g.natDegree + f.natDegree))) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)

Tactic:
reflect_C_mul,

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ C f.leadingCoeff * (C g.leadingCoeff * reflect (N + O) (X ^ (g.natDegree + f.natDegree))) =
    C f.leadingCoeff * reflect N (X ^ f.natDegree) * (C g.leadingCoeff * reflect O (X ^ g.natDegree))
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Tactic:
rintro ⟨a, ha, b, rfl⟩
    simp [ha]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsLeftCancelMulZero R
h : p.natDegree = 1
r₁ : R
⊢ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p

Tactic:
rwa [natDegree_eq_one] at h

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
⊢ ((optionEquivLeft R σ) p).support = Finset.image (fun m ↦ m none) p.support

Tactic:
ext i
  simp only [Polynomial.mem_support_iff, ne_eq, MvPolynomial.ext_iff, coeff_zero, not_forall,
    Finset.mem_image, mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none]
  constructor
  · rintro ⟨m, hm⟩
    exact ⟨optionElim i m, by simpa using! hm, optionElim_apply_none _ _⟩
  · rintro ⟨m, h, rfl⟩
    exact ⟨some m, h⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree

Tactic:
have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ (φ 0).natDegree = fu (natDegree 0)

Tactic:
by simp [fu0]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ reflect N (C (-1) * f) = -reflect N f

Tactic:
reflect_C_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ C (-1) * reflect N f = -reflect N f
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
by rw [one_pow, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ∑ i ∈ range n, (-1) ^ i = if Even n then 0 else 1

Tactic:
by
  induction n with
  | zero => simp
  | succ k hk =>
    simp only [geom_sum_succ', Nat.even_add_one, hk]
    split_ifs with h
    · rw [h.neg_one_pow, add_zero]
    · rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

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

Goal state before:
pp: case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
⊢ (C x).coeff n ∈ I

Tactic:
coeff_C

Goal state after:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
⊢ (if n = 0 then x else 0) ∈ I
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
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
x : A
t : Finset A
a✝ : x ∉ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R ↑(insert x t))

Tactic:
Finset.coe_insert

Goal state after:
case refine_2
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
x : A
t : Finset A
a✝ : x ∉ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R (insert x ↑t))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝ : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
⊢ Function.Injective ⇑f

Tactic:
refine LinearMap.ker_eq_bot.1 <| LinearMap.ker_eq_bot'.2 fun n hn ↦ ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝ : AddCommGroup M := addCommMonoidToAddCommGroup R
this : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
⊢ n = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr.convert_5
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ q ∈ Ideal.span ↑s

Tactic:
exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T ≤ toSubmodule (S ⊔ T)

Tactic:
Submodule.mul_le

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ m ∈ toSubmodule S, ∀ n ∈ toSubmodule T, m * n ∈ toSubmodule (S ⊔ T)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
⊢ coeff n (C x) ∈ I

Tactic:
coeff_C

Goal state after:
case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
⊢ (if 0 = n then x else 0) ∈ I
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.zero
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
S : Type u_2
inst✝³ : Semiring S
inst✝² : CharZero S
inst✝¹ : ExpChar R 1
inst✝ : ExpChar S 1
hp : Nat.Prime 1
hchar✝ : CharP R 1
⊢ ExpChar (R × S) 1

pp: case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p

Tactic:
· exact (Nat.not_prime_one hp).elim

Goal state after:
case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Injective ⇑(quotientMap I f H)

Tactic:
by
  refine (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_
  obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
  rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha
  exact Quotient.eq_zero_iff_mem.mpr (h ha)

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

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (n % period m a) • a = m ^ n • a

Tactic:
conv_rhs => rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

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

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s.length = t.length

Tactic:
simpa using congr_arg length h

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
h : x ∈ [y, z]
⊢ [y, z].prev x h = y

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = y

Tactic:
· simp [prev, hz]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = y
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

Tactic:
exact gp.2

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

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ s.Nodup

Tactic:
induction s using Quot.inductionOn with | _ l
  obtain - | ⟨hd, tl⟩ := l
  · simp
  · have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
    simp [this]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ (⨅ i, f i).index ≤ ∏ i, (f i).index

Tactic:
simp_rw [← relIndex_top_right, relIndex_iInf_le]

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = cast 0 ↔ a = 0

Tactic:
exact Injective.eq_iff' (cast_injective_of_le h) rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors = ∅ ↔ n = 0

Tactic:
by
  contrapose!
  exact nonempty_divisors

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_1
m n : ℕ
hn : n ≠ 0
h : m ∈ n.properDivisors
⊢ n = m * (n / m)

pp: case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Tactic:
· exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm

Goal state after:
case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
← Nat.not_even_iff_odd

Goal state after:
case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ ↑(↑m)⁻¹.val * ↑m = 1

Tactic:
rw [mul_comm, mul_val_inv hmn]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ p.divisors.erase p = {1}

Tactic:
pp.divisors,

Goal state after:
p : ℕ
pp : Prime p
⊢ {1, p}.erase p = {1}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ z.divisors = ∅ ↔ z = 0

Tactic:
by
  contrapose!
  exact nonempty_divisors

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

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
← Nat.two_dvd_ne_zero,

Goal state after:
n : ℕ
hn : ¬2 ∣ n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z a✝ : ℤ
⊢ a✝ ∈ image Prod.fst z.divisorsAntidiag ↔ a✝ ∈ z.divisors

Tactic:
simp [Eq.comm, dvd_def]

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

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ ¬a + a = 0

Tactic:
add_self_eq_zero_iff_eq_zero hn

Goal state after:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ ¬a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ZMod 2
⊢ -a = a

Tactic:
by
  fin_cases a <;> apply Fin.ext <;> simp; rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1 + k - k) ^ k

Tactic:
Nat.add_sub_cancel

Goal state after:
case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1) ^ k