mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : 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)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f - g) i = (⇑f - ⇑g) i

Tactic:
exact tsub_apply f g i

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = 0 ↔ a = 0

Tactic:
← map_zero C,

Goal state after:
R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = C 0 ↔ a = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ s ≤ m

Tactic:
obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
j : σ →₀ ℕ
h : j + s ∈ (p * (monomial s) r).support
⊢ s ≤ j + s
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
rw [coeffs, Finset.image_subset_iff]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ ∀ x ∈ support 1, coeff x 1 ∈ {1}
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: 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
x : S
⊢ C x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
by simpa using monomial_mem_coeffsIn (i := 0)

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

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Tactic:
· intro p n hp
    simp only [hp, rename_X, constantCoeff_X, map_mul]

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

Goal state before:
pp: case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p - q = p + -q

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: case e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ q.vars = (-q).vars

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: case e'_2
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ p - q = p + -q

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ q.vars = (-q).vars

Tactic:
simp [sub_eq_add_neg]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
by
  rw [← vars_neg q] at hpq
  convert! vars_add_of_disjoint hpq using 2 <;> simp [sub_eq_add_neg]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ ∀ m ∈ (f - g).support, m x < k

Tactic:
grind [degreeOf_lt_iff]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
⊢ (∑ i ∈ t, φ i).vars = t.biUnion fun i ↦ (φ i).vars

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree = ↑(n * q.natDegree)

Tactic:
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑n * ↑q.natDegree = ↑(n * q.natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < p.trailingDegree

Tactic:
rw [hp, trailingDegree_zero]

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < ⊤
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
⊢ reflect N (C c * X ^ n) = C c * X ^ (revAt N) n

Tactic:
ext
  grind

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        Finset.sup'_eq_sup hs]
      refine le_antisymm ?_ ?_
      · rw [Finset.sup'_le_iff]
        intro b hb
        by_cases hb' : f b = 0
        · simpa [hb'] using! hs
        rw [degree_eq_natDegree hb', Nat.cast_withBot]
        exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
      · rw [Finset.sup'_le_iff]
        intro b hb
        simp only [Finset.le_sup'_iff, Function.comp_apply]
        by_cases hb' : f b = 0
        · refine ⟨x, hx, ?_⟩
          contrapose! hx'
          simpa [← Nat.cast_withBot, hb', degree_eq_bot] using! hx'
        exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩

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

Goal state before:
pp: case pos.h
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)

Tactic:
· exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : ((X + C a) * g).natDegree = (X + C a).natDegree + g.natDegree
⊢ False

Tactic:
rw [hfg, natDegree_one, natDegree_X_add_C] at h

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = 1 + g.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

pp: case neg
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
· simp only [f0, zero_mul, reverse_zero]

Goal state after:
case neg
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ (f * g).reverse = f.reverse * g.reverse
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: R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (finprod f).Monic

Tactic:
rw [finprod_def]

Goal state after:
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset h, f i else 1).Monic
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
⊢ (∃ a, k a = i) → (∑ x_1, if i = k x_1 then x x_1 else 0) ≠ 0

Tactic:
rintro ⟨j, _, rfl⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ (∑ x_1, if k j = k x_1 then x x_1 else 0) ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
and_iff_right hp1

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Tactic:
simpa using coeff_zero_multiset_prod (s.1.map f)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
and_iff_right hp1

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
⊢ ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree

Tactic:
by
  obtain ⟨a, has, hmax⟩ := s_fin.exists_maximalFor degree s hs
  refine ⟨a, has, fun p hp => ?_⟩
  obtain ⟨p', hp', hpp'⟩ := exists_degree_le_of_mem_span hs hp
  exact hpp'.trans <| not_lt.1 <| not_lt_iff_le_imp_ge.2 <| hmax hp'

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

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
this : ↑(l z) ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_linearCombination R] at this

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
this : ∃ l_1 ∈ Finsupp.supported R R p, (Finsupp.linearCombination R _root_.id) l_1 = ↑(l z)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: 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
k : ℕ
h : N < k
x✝ : R
hx : x✝ ∈ I.leadingCoeffNth k
hxm : x✝ ∉ M
⊢ I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth

Tactic:
exact ⟨k, rfl⟩

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

Goal state before:
pp: 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
⊢ p.degree = q.degree + (X ^ (k - q.natDegree)).degree

pp: 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
⊢ q.leadingCoeff * (X ^ (k - q.natDegree)).leadingCoeff ≠ 0

Tactic:
Polynomial.degree_X_pow

Goal state after:
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
⊢ p.degree = q.degree + ↑(k - q.natDegree)

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
⊢ q.leadingCoeff * (X ^ (k - q.natDegree)).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

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

Tactic:
sup_idem

Goal state after:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S = toSubmodule S
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ I = ⊥

Tactic:
rw [← map_eq_bot_iff_of_injective h.1]

Goal state after:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ map (mk I) I = ⊥
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).snd = map (fun x ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r

Tactic:
by
  rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f^[m] n x

Tactic:
by
  rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
  exact hf.isFixedPt.iterate m

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x

Tactic:
unfold IsPeriodicPt IsFixedPt

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ f^[m] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x

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
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x

Tactic:
rw [IsPeriodicPt, IsFixedPt, iterate_mul]

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : x ∈ ys.dropLast → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'

Tactic:
| cons y ys IH =>

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
ys : List α
IH : x ∈ ys.dropLast → ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)

Tactic:
rw [iterate_zero_apply]
      nth_rw 3 [← @iterate_minimalPeriod α f x]
      nth_rw 2 [← hM]
      exact H _ (Nat.lt_succ_self _)

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys

Tactic:
| cons y ys IH =>

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
⊢ k = k.succ

Tactic:
have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ k = k.succ
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x✝ : ↥(stabilizer G a)
⊢ ↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh)) x✝) = ↑((stabilizerEquivStabilizer hk) x✝)

Tactic:
simp [stabilizerEquivStabilizer_apply, H]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x

Tactic:
rw [eq_zero_of_pow_eq_zero hx]

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s

Tactic:
induction s
  · trivial
  · rw [chain_coe_cons] at p ⊢
    exact p.imp H

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (unop ↑b)⁻¹ * c⁻¹ * x✝¹ * unop ↑b ∈ H

Tactic:
mem_normalizer_iff'.mp b.prop,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ unop ↑b * ((unop ↑b)⁻¹ * c⁻¹ * x✝¹) ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
⊢ RightInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
by
    simp only [Function.RightInverse, LeftInverse]
    intro q
    induction q using Quotient.inductionOn'
    rfl

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b

Tactic:
simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ← primeFactors_gcd,
    ha, hb]

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⁻¹ * a ∈ H

Tactic:
inv_mul_cancel

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
⊢ 1 ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (map f H).relIndex f.range * f.range.index

Tactic:
relIndex_mul_index (H.map_le_range f)

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (map f H).index