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

Goal state before:
pp: case neg.h₀
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✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
⊢ j ≠ i → (C (x j) * X ^ k j).coeff (k i) = 0

Tactic:
hji

Goal state after:
case neg.h₀
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✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ (C (x j) * X ^ k j).coeff (k i) = 0
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]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬(q.degree = ⊥ ∨ p.degree = ⊥)

Tactic:
not_or,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q.degree = ⊥ ∧ ¬p.degree = ⊥
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 1
⊢ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1

Tactic:
· obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h
    exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k) → #f.support = 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ degreeLT R (n + 1) = degreeLE R ↑n

Tactic:
ext x
  by_cases x_zero : x = 0
  · simp_rw [x_zero, Submodule.zero_mem]
  · rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
| p

Tactic:
← eraseLead_add_C_mul_X_pow p

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
| p.eraseLead + C p.leadingCoeff * X ^ p.natDegree
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.natDegree = p.natDegree

Tactic:
by
  simp [natDegree]

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

Goal state before:
pp: case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (∅.prod f).coeff k ∈ I ^ (∅.sum n - k)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card αˣ + 1

Tactic:
Nat.card_units,

Goal state after:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card α - 1 + 1
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Nat.card αˣ = card α - 1

Tactic:
Nat.card_units,

Goal state after:
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Nat.card α - 1 = card α - 1
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
⊢ Function.Injective ⇑starAlgHom

Tactic:
have := AlgHomClass.unitization_injective s h1 ((StarSubalgebra.subtype _).comp starAlgHom)
        fun _ ↦ by simp [starAlgHom]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
this : Function.Injective ⇑((StarAlgebra.adjoin R ↑s).subtype.comp starAlgHom)
⊢ Function.Injective ⇑starAlgHom
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ l ∈ s.lists ↔ s = ⟦l⟧

Tactic:
induction s using Quotient.inductionOn
  simpa using perm_comm

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

Goal state before:
pp: case cons.mp.inr
α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ [y] ++ l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1,
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ ∃ l₁_1 l₂_1,
    l₂_1 ≠ [] ∧ y :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
exact ⟨y :: l₁, l₂, l0, by simp⟩

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x

Tactic:
rcases le_total n m with h | h
  · refine left_of_add ?_ hn
    rwa [tsub_add_cancel_of_le h]
  · rw [tsub_eq_zero_iff_le.mpr h]
    apply isPeriodicPt_zero

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
revert hm hn

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
⊢ IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (m.gcd n) x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.e_a.e_b
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = (permutationsAux2 t is [] x✝ fun x ↦ x ++ ts).snd

Tactic:
simp +singlePass only [← permutationsAux2_comp_append]

Goal state after:
case cons.e_a.e_b
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ fun x ↦ id (x ++ (is ++ ts))).snd =
    (permutationsAux2 t [] [] x✝ fun x ↦ x ++ is ++ ts).snd
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n

Tactic:
classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

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 • a = a ↔ minimalPeriod (fun x ↦ m • x) a ∣ n

Tactic:
← isPeriodicPt_iff_minimalPeriod_dvd,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ IsPeriodicPt (fun x ↦ m • x) n a
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (-↑(n + 1)) • a = a ↔ ↑(period g a) ∣ -↑(n + 1)

Tactic:
rw [zpow_neg, zpow_natCast, inv_smul_eq_iff, eq_comm, Int.dvd_neg, Int.natCast_dvd_natCast,
      pow_smul_eq_iff_period_dvd]

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) % period m a) • a = m ^ n • a

Tactic:
Nat.add_mod_right,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (n % period m a) • a = m ^ n • a
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) - 1 + (head :: tail).length) % (head :: tail).length

pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

pp: case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length

Tactic:
Nat.add_mod_right,

Goal state after:
case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) - 1) % (head :: tail).length

case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + (tl.length + 1)) % (tl.length + 1) = n

Tactic:
Nat.add_mod_right,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ n % (tl.length + 1) = n
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)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
a b : ↑(orbitRel.Quotient.orbit ω)
h : ⟦↑a⟧ = ⟦↑b⟧
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
simp only [Quotient.eq] at h ⊢

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
a b : ↑(orbitRel.Quotient.orbit ω)
h : (orbitRel (↥H) X) ↑a ↑b
⊢ (Setoid.comap Subtype.val (orbitRel (↥H) X)) ⟨↑a, ⋯⟩ ⟨↑b, ⋯⟩
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)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : (Setoid.comap Subtype.val (orbitRel (↥H) X)) a b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
by
      rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
      simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]
      exact h

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

Goal state before:
pp: p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q

Tactic:
eq_of_mem_replicate hq

Goal state after:
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q

Tactic:
rwa [eq_of_mem_replicate hq]

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

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

Tactic:
constructor
  · contrapose!
    rintro hn
    obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
    exact ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
  · rintro (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
this : ∀ (b : G), b ∈ H
⊢ H.index ∣ 2

Tactic:
by simp [(eq_top_iff' _).mpr this]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ Injective ⇑(castHom ⋯ R)

Tactic:
rw [injective_iff_map_eq_zero]
  intro x
  obtain ⟨k, rfl⟩ := ZMod.intCast_surjective x
  rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]
  exact id

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ ((fun g ↦ f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) g ↔ f g = f ((fun x_1 ↦ x * x_1) y)

Tactic:
simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]

Goal state after:
case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ f g * f y⁻¹ = f x ↔ f g = f x * f y
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]

Goal state after:
case succ
n m : ℕ
⊢ n ∣ m + 1 → n ≤ m + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
· apply ZMod.val_mul_of_lt h

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

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs = ↑(a.natAbs.gcd 0)

Tactic:
Nat.gcd_zero_right

Goal state after:
a : ℤ
⊢ ↑a.natAbs = ↑a.natAbs
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n

Tactic:
by
  rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]
  constructor <;> intro h
  · rw [h]
  · apply add_right_cancel h

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
x✝ : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ ∑ i ∈ range n, x ^ i = 0

Tactic:
simp only [h, hn, neg_one_geom_sum, if_true]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.divisors, f x = f p * f 1

Tactic:
rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]

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

Goal state before:
pp: a b n : ℕ
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
by
      rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]

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

Goal state before:
pp: n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom

Tactic:
mul_assoc

Goal state after:
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
len : (D :: L).length = (d :: l).length
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : ofDigits b (D :: L) = ofDigits b (d :: l)
⊢ D :: L = d :: l

Tactic:
simp only [List.length_cons, add_left_inj] at len

Goal state after:
case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : ofDigits b (D :: L) = ofDigits b (d :: l)
len : L.length = l.length
⊢ D :: L = d :: l
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
obtain ⟨c, hc⟩ := pow_multiplicity_dvd a b
  refine ⟨c, hc, ?_⟩
  rintro ⟨k, hk⟩
  rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc
  have h₁ : a ^ (multiplicity a b + 1) ∣ b := ⟨k, hc⟩
  exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

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

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
hT : T.prod g ≠ 0
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization

Tactic:
simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 = minimalPeriod (fun x_1 ↦ x * x_1)^[n] 1

Tactic:
mul_left_iterate

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 = minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ single p k ≤ n.factorization ↔ k ≤ n.factorization p

Tactic:
single_le_iff

Goal state after:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ k ≤ n.factorization p ↔ k ≤ n.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 = minimalPeriod (fun x_1 ↦ x * x_1)^[n] 1

Tactic:
mul_left_iterate

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 = minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ (orderOf x).pred * x * y)

Tactic:
mul_assoc

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ (orderOf x).pred * (x * y))
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)

Tactic:
rw [mem_Ico] at hm

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
⊢ Group H

Tactic:
letI : Finite Hᵐᵒᵖ := Finite.of_equiv H MulOpposite.opEquiv

Goal state after:
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
this : Finite Hᵐᵒᵖ := Finite.of_equiv H MulOpposite.opEquiv
⊢ Group H
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 1 < ↑1

Tactic:
Prime.emultiplicity_one

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1

case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ padicValNat p n = 1

Tactic:
← factorization_def n (Finset.mem_filter.mp hp1).2

Goal state after:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ n.factorization p = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: N n : ℕ
⊢ #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n

Tactic:
induction N with
  | zero => simp [Finset.filter_false_of_mem]
  | succ N ih =>
    rw [Finset.range_add_one, Finset.filter_insert]
    by_cases h : n ∣ N.succ
    · simp [h, succ_div_of_dvd, ih]
    · simp [h, succ_div_of_not_dvd, ih]

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

Goal state before:
pp: case inl
a b m n : ℕ
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
hm : m ≠ 0
⊢ m'.Coprime n'

Tactic:
exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).coeff o = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)
    · exact natDegree_pow_le_of_le m ‹_›
    · exact Iff.mp ne_comm h

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

pp: case inr
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
· rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
⊢ ((expand R p) f).natDegree = f.natDegree * p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
⊢ IsUnit f ∨ IsUnit g

Tactic:
wlog! H : f.degree ≤ g.degree generalizing f g
    · rw [mul_comm] at h
      exact (this g f h H.le).symm
    left
    rw [h, degree_mul, Nat.WithBot.add_eq_one_iff] at hp
    rcases hp with ⟨hf, hg⟩ | ⟨hf, hg⟩; swap
    · simp [← not_lt, hf, hg] at H
    replace hf := f.eq_C_of_degree_eq_zero hf
    rw [hf]
    apply IsUnit.map C
    rw [h, hf, coeff_C_mul, coeff_C_mul] at hc
    apply hc <;> simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ((⇑derivative)^[k] p).natDegree ≤ p.natDegree - k

Tactic:
induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
      rw [Function.iterate_succ_apply', Nat.sub_succ']
      exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
rw [modByMonic_eq_of_not_monic _ hq, divByMonic_eq_of_not_monic _ hq, mul_zero, sub_zero]

Goal state after: