mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (c :: s ++ [a]).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
cons_append

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (c :: (s ++ [a])).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
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
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * x✝³⁻¹ * (x✝³ * x✝¹) ∈ H

Tactic:
mul_assoc,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * (x✝³⁻¹ * (x✝³ * x✝¹)) ∈ H
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 * ((unop ↑b)⁻¹ * c⁻¹ * x✝¹) ∈ H

Tactic:
mul_assoc,

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✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (unop x✝³)⁻¹ * x✝²⁻¹ * (x✝¹ * unop x✝³) ∈ H

Tactic:
mul_assoc,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (unop x✝³)⁻¹ * (x✝²⁻¹ * (x✝¹ * unop x✝³)) ∈ H
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
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * (x✝¹ * unop x✝³) * (unop x✝³)⁻¹ ∈ H

Tactic:
mul_assoc,

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * (x✝¹ * unop x✝³ * (unop x✝³)⁻¹) ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (Quotient.out q)⁻¹ * g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q ∈ H

Tactic:
mul_assoc,

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (Quotient.out q)⁻¹ * (g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q) ∈ H
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ Prime p

Tactic:
have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
        List.mem_cons.1 (by rwa [primeFactorsList] at h)

Goal state after:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
⊢ Prime p
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ g⁻¹ ∈ H

Tactic:
← mul_one g⁻¹,

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ g⁻¹ * 1 ∈ H
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a * a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
mul_assoc,

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a * (a ^ n * c) = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a * a ^ n * c).primeFactorsList

Tactic:
mul_assoc,

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a * (a ^ n * c)).primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b * c ∉ H

Tactic:
mul_assoc,

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * (b * c) ∉ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast

Tactic:
by
  rcases n with - | n
  · simp; rfl
  change Fin (n + 1) at a b
  change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _
  simp only [Fin.val_add_eq_ite, Int.natCast_succ]
  norm_cast
  split_ifs with h
  · rw [Nat.cast_sub h]
    congr
  · rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ Nat.card M ≤ Nat.card ↑↑f.range

Tactic:
SetLike.coe_sort_coe,

Goal state after:
G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ Nat.card M ≤ Nat.card ↥f.range
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ val 1 = 1 % n

Tactic:
by
  rw [← Nat.cast_one, val_natCast]

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

Goal state before:
pp: case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
ZMod.natCast_zmod_val,

Goal state after:
case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ ↑m * (↑m)⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
⊢ IsUnit ↑m ↔ m.Coprime n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩
  have H' := val_coe_unit_coprime H.unit
  rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'
  rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']
  exact Nat.gcd_rec n m

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

Goal state before:
pp: case refine_1
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑x.cast.val = ↑x.val

Tactic:
ZMod.natCast_zmod_val,

Goal state after:
case refine_1
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = ↑x.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑x.cast.val = ↑x.val

Tactic:
ZMod.natCast_zmod_val,

Goal state after:
case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = ↑x.val
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.descFactorial k < n ^ k

Tactic:
exact descFactorial_lt_pow hn hk

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

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n

Tactic:
mul_assoc,

Goal state after:
n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n + 1) * (2 * n).choose n)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p✝ n : ℕ
hn : n ≠ 0
p : ℕ
⊢ (p + 2) ^ padicValNat (p + 2) n < (p + 2) ^ n

Tactic:
apply Nat.lt_of_le_of_lt ?_ <| Nat.lt_pow_self <| by lia

Goal state after:
p✝ n : ℕ
hn : n ≠ 0
p : ℕ
⊢ (p + 2) ^ padicValNat (p + 2) n ≤ n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)).sum

Tactic:
induction L with
  | nil => simp
  | cons hd tl hl =>
    simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using!
      Or.inl hl

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ 0 < n / b.succ.succ

Tactic:
exact Nat.div_pos hnb (zero_lt_succ (succ b))

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b n : ℕ
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
by
  rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  rcases le_or_gt b 1 with hb | hb
  · interval_cases b <;> simp +arith [digits_zero_succ', hn]
  simpa [length_digits, hb, hn] using log_mono_right (le_succ _)

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

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
mul_assoc,

Goal state after:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ b.digits (b * (b ^ k * m)) = List.replicate (k + 1) 0 ++ b.digits m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
hm : emultiplicity a b = ⊤
⊢ ⊤ = ↑(multiplicity a b)

pp: case coe
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
a✝ : ℕ
hm : emultiplicity a b = ↑a✝
⊢ ↑a✝ = ↑(multiplicity a b)

Tactic:
· simp [h] at hm

Goal state after:
case coe
α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
a✝ : ℕ
hm : emultiplicity a b = ↑a✝
⊢ ↑a✝ = ↑(multiplicity a b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False

Tactic:
· simp at hm

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Finset (List ℕ)

Tactic:
have : Fintype {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} :=
    Fintype.ofInjective (Set.MapsTo.restrict _ _ _ (mapsTo_ofDigits hb l))
      <| (Set.MapsTo.restrict_inj (mapsTo_ofDigits hb l)).mpr <| injOn_ofDigits hb l
  exact {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ emultiplicity p b = ⊤

Tactic:
emultiplicity_eq_top

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n / p ^ n.factorization p).factorization p

Tactic:
Nat.factorization_div (Nat.ordProj_dvd n p)

Goal state after:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p
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 (1 * y)

Tactic:
← pow_orderOf_eq_one x,

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 * y)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b

Tactic:
simpa [pb] using h b

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * (x * y) * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * (x * y * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)

Tactic:
by
  simpa using h.add_pow_prime_pow_eq hp 1

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
obtain _ | hprime := hR

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 = x ^ 1 + y ^ 1

case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
obtain _ | hprime := hR

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n

case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ g ^ H.index ∈ H

Tactic:
by rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']

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

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
d : G
⊢ (single g 1 * x %ᵒᶠ g).coeff (g + d) = 0

Tactic:
rw [coeff_modOf_self_add]

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

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g d : G
⊢ (x * single g 1 %ᵒᶠ g).coeff (g + d) = 0

Tactic:
rw [coeff_modOf_self_add]

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

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

Tactic:
ext
  simpa only [coeff_divX, coeff_zero] using! coeff_one

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

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (divX_hom (C c * X ^ n)).natDegree = n - 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
G : Type u_6
inst✝¹ : Group G
inst✝ : Finite G
S : Set G
hS1 : S.Nonempty
hS2 : S * S = S
a : G
ha : a ∈ S
⊢ a⁻¹ ∈ submonoidOfIdempotent S hS1 hS2

Tactic:
rw [← one_mul a⁻¹, ← pow_one a, ← pow_orderOf_eq_one a, ← pow_sub a (orderOf_pos a)]

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Finite G
S : Set G
hS1 : S.Nonempty
hS2 : S * S = S
a : G
ha : a ∈ S
⊢ a ^ (orderOf a - succ 0) ∈ submonoidOfIdempotent S hS1 hS2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ ∃ i ≤ n, c = p ^ i

Tactic:
by rwa [Nat.dvd_prime_pow hp.1] at hcpn

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

Goal state before:
pp: case refine_2.inl.inr
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

pp: case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

pp: case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
· refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq

Goal state after:
case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ (p + q).natDegree = 0 ∨ M (p + q)

case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f g : R[X]
⊢ (f + g).coeff n = f.coeff n + g.coeff n

Tactic:
apply coeff_add

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (∑ x ∈ f.support, if p * x = n then f.coeff x else 0) = f.coeff (n / p)

Tactic:
rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
    · intro b _ hb2
      rw [if_neg]
      intro hb3
      apply hb2
      rw [← hb3, Nat.mul_div_cancel_left b hp]
    · intro hn
      rw [notMem_support_iff.1 hn]
      split_ifs <;> rfl

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ n * X * k

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ n * (X * k)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ p * r = p * C (p * r).leadingCoeff

Tactic:
have : r.natDegree = 0 := by simpa [hp.natDegree_mul' hr] using hdeg

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
⊢ p * r = p * C (p * r).leadingCoeff
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
h : (X - C c) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p.comp (C a * X + C b)
⊢ (X - C (a * c + b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p

Tactic:
rw [dvd_comp_C_mul_X_add_C_iff, pow_comp] at h

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
h : (X - C c).comp (C ⅟a * (X - C b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p
⊢ (X - C (a * c + b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative ↑n = 0

Tactic:
rw [← map_natCast C n]
  exact derivative_C

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ (monomial (n * p)) ((frobenius R p) a) = (monomial n) a ^ p

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = (monomial n) a ^ p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = (monomial n) a ^ p

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ C ((frobenius R p) a) * X ^ (n * p) = (C a * X ^ n) ^ p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial.zero
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
b : R
⊢ (monomial (0 + n - 1)) (a * (b * ↑0)) + (monomial (0 + n - 1)) (a * (b * ↑n)) =
    (monomial (0 - 1 + n)) (a * (b * ↑0)) + (monomial (0 + (n - 1))) (a * (b * ↑n))

Tactic:
simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]

Goal state after: