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

Goal state before:
pp: case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p

Tactic:
rw [hd, sup_idem]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i) = supDegree D (f i) ∧ leadingCoeff D (f i) = leadingCoeff D (f i)

Tactic:
exact ⟨rfl, rfl⟩

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

Goal state before:
pp: S : Type v
inst✝ : Ring S
c : S
⊢ (X - C c).nextCoeff = -c

Tactic:
rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]

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

Goal state before:
pp: case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)
⊢ eval₂ f (eval₂ f t (p.comp^[k] q)) p = eval₂ f ((fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)) p

Tactic:
IH

Goal state after:
case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)
⊢ eval₂ f ((fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)) p = eval₂ f ((fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex (update x i a) < toLex x ↔ a < x i

Tactic:
by
  refine ⟨?_, fun h => toLex_strictMono <| update_lt_self_iff.2 h⟩
  rintro ⟨j, hj, h⟩
  dsimp at h
  obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false
  rwa [update_self] at h

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

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ ∀ i_1 ∈ f.support.erase i, p ∣ (RingHom.id S) (f.coeff i_1) * z ^ i_1

Tactic:
intro j hj

Goal state after:
case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ (RingHom.id S) (f.coeff i) * z ^ i + ∑ x ∈ f.support.erase i, (RingHom.id S) (f.coeff x) * z ^ x
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
j : ℕ
hj : j ∈ f.support.erase i
⊢ p ∣ (RingHom.id S) (f.coeff j) * z ^ j
Module: Mathlib.Algebra.Polynomial.AlgebraMap

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

Tactic:
IH

Goal state after:
case step
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
⊢ P.coeff l • Q = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = C a * X s ^ 1

Tactic:
pow_one

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
⊢ C a * X s = C a * X s
Module: Mathlib.Data.Finsupp.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a ↦ toLex (single a 1)

Tactic:
intro a b h
  simp only [LT.lt, Finsupp.lex_def]
  simp only [ofLex_toLex, Nat.lt_eq]
  use a
  constructor
  · intro d hd
    simp only [Finsupp.single_eq_of_ne hd.ne, Finsupp.single_eq_of_ne (hd.trans h).ne]
  · simp [h.ne']

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = coeff m (X i ^ 1)

Tactic:
pow_one

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = coeff m (X i)
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
⊢ coeffsIn σ M = Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

Tactic:
refine le_antisymm ?_ <| Submodule.span_le.2 ?_
  · rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩
  · rintro _ ⟨m, hm, s, n, rfl⟩ i
    simp
    split <;> simp [hm]

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∀ x_1 ∈ x.support, (Finsupp.single (f x_1) (x x_1)) i = 0

Tactic:
intro j hj

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
j : σ
hj : j ∈ x.support
⊢ (Finsupp.single (f j) (x j)) i = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: n : Fin 2 →₀ ℕ
⊢ (ofSupportFinite ![n 0, n 1] ⋯) 0 = n 0 ∧ (ofSupportFinite ![n 0, n 1] ⋯) 1 = n 1

Tactic:
exact ⟨rfl, rfl⟩

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

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

Tactic:
rcases Nat.le.dest ho with ⟨o', rfl⟩

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ 0 = (p + q.eraseLead).coeff q.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f
⊢ f.eraseLead = 0

Tactic:
obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
a : R
hnext : (C a).nextCoeff = 0
⊢ (C a).eraseLead = 0

case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : (C a * X + C b).nextCoeff = 0
⊢ (C a * X + C b).eraseLead = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
induction f using MvPolynomial.induction_on' with

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑(aeval f) ↔ Injective ⇑(algebraMap R S₁)

Tactic:
rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) ↔ Injective (⇑(algebraMap R S₁) ∘ ⇑(isEmptyAlgEquiv R σ))
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
by
  by_cases hf : f = 0
  · rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
  apply le_antisymm
  · refine tsub_le_iff_right.mp ?_
    apply le_natDegree_of_ne_zero
    rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
    exact trailingCoeff_nonzero_iff_nonzero.mpr hf
  · rw [← le_tsub_iff_left f.reverse_natDegree_le]
    apply natTrailingDegree_le_of_ne_zero
    have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
    rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key

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

Goal state before:
pp: case nil
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hl : ∀ p ∈ [], p.degree ≤ n
⊢ [].sum.degree ≤ n

Tactic:
| nil =>

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

Goal state before:
pp: case nil
S : Type u_1
inst✝ : Semiring S
n : ℕ
hl : ∀ p ∈ [], p.natDegree ≤ n
⊢ [].prod.coeff ([].length * n) = (List.map (fun p ↦ p.coeff n) []).prod

Tactic:
| nil =>

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

Goal state before:
pp: 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
i : Fin n
hi : i.castSucc = Fin.last n
⊢ False

Tactic:
exact i.castSucc_lt_last.ne hi

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

Goal state before:
pp: case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂

Tactic:
have hda := hnd

Goal state after:
case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : (a * b).natDegree = 2
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map (fun x ↦ X - C x) s).prod.natDegree = s.card

Tactic:
natDegree_multiset_prod_of_monic,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) s)).sum = s.card

case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x.degree < ↑(n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
mem_degreeLE,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x.degree < ↑(n + 1) ↔ x.degree ≤ ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : X ^ (n + 1) ∈ degreeLE R ↑n
⊢ False

Tactic:
mem_degreeLE,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : (X ^ (n + 1)).degree ≤ ↑n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) i) ((fun n ↦ I.leadingCoeffNth n) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) j) ((fun n ↦ I.leadingCoeffNth n) z)

Tactic:
exact
    ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
      I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ coeff 1 0 ∉ P

Tactic:
coeff_one_zero,

Goal state after:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ 1 ∉ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case e'_1
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime (C r)

Tactic:
congr!
    simp only [renameEquiv_apply, algHom_C, algebraMap_eq]

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ r = 0

Tactic:
rw [← C_inj, h]
        simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: 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
inst✝ : FiniteType R S
⊢ adjoin S ↑{X} = ⊤

Tactic:
rw [Finset.coe_singleton]

Goal state after:
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
inst✝ : FiniteType R S
⊢ S[ X] = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ n f, Surjective ⇑f

pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ n f, Surjective ⇑f) → FiniteType R S

Tactic:
· rw [iff_quotient_mvPolynomial']
    rintro ⟨ι, hfintype, f, hsur⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩

Goal state after:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ n f, Surjective ⇑f) → FiniteType R S
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
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
⊢ p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff

Tactic:
rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False

Tactic:
· exact hneq h

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
⊢ ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)

Tactic:
intro j hj

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ IsCoprime (I i) (I j)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (Quotient.mk (I i)) (f x * e x) = 0

Tactic:
intro j hj

Goal state after:
case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ (Quotient.mk (I i)) (f j * e j) = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p

Tactic:
by
  by_contra! h
  revert h_two h_three hp
  decide +revert

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

Goal state before:
pp: p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ p ^ 1 = p

Tactic:
pow_one

Goal state after:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ p = p
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a ^ 1

Tactic:
pow_one

Goal state after:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a
Module: Mathlib.Data.Nat.Prime.Basic

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

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
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
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
rwa [_root_.pow_succ, _root_.pow_succ]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case hf
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ Surjective ⇑(Quotient.mk I)

Tactic:
exact Quotient.mk_surjective

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

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

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
t : α
⊢ map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).snd

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
t : α
ts l' l : List α
⊢ l' ∈ (permutationsAux2 t ts [] [] fun x ↦ l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ [] = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
| nil =>

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier

Tactic:
Subalgebra.mem_carrier,

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ Algebra.adjoin R (s ∪ star s)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r [] =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) [] ++ r

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ [] → l.length = n
⊢ (map length []).sum = n * [].length

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ map (map f) [].permutations' = (map f []).permutations'

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
ts is' : List α
⊢ ([] ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) ([].permutationsAux is') ++ ts.permutationsAux ([].reverse ++ is')

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
f : α → α
⊢ periodicPts f ⊆ range f

Tactic:
by
  intro x h
  rw [mem_periodicPts] at h
  rcases h with ⟨n, _, h⟩
  use f^[n - 1] x
  nth_rw 1 [← iterate_one f]
  rw [← iterate_add_apply, Nat.add_sub_cancel' (by lia)]
  exact h

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m :
  l ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) (is :: is.permutationsAux [])
⊢ l ~ t :: ts ++ is

Tactic:
mem_foldr_permutationsAux2

Goal state after:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m :
  l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations

Tactic:
mem_foldr_permutationsAux2

Goal state after:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts