mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_notMem_periodicPts hx]

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ n < 0, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case add
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ + y✝, ⋯⟩

Tactic:
exact add _ _ h₁ h₂

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

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

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

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [] ≠ []
⊢ [].prev ([].head hl) ⋯ = [].getLast hl

Tactic:
contradiction

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
hi₁ : i = 1
⊢ l[i + idxOf a l]? = some [a, l.nextOr a d][i]

Tactic:
grind [next, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]

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

Goal state before:
pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)

Tactic:
refine ⟨hd, hd', ?_, by simp⟩

Goal state after:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ¬hd = hd'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
this : [] = b :: m
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
contradiction

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

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
this : a :: l = []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
contradiction

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

Goal state before:
pp: ⊢ ¬BddAbove {p | Prime p}

Tactic:
by
  rw [not_bddAbove_iff]
  intro n
  obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
  exact ⟨p, hp, hi⟩

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

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ g⁻¹ * ⋯.choose ∈ ⊥

Tactic:
← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x),

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ g⁻¹ * ⋯.choose ∈ stabilizer G (g⁻¹ • x)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p

Tactic:
contradiction

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

Goal state before:
pp: case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

Tactic:
contradiction

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ a * a ∈ H

Tactic:
mul_mem_iff_of_index_two h

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ a ∈ H ↔ a ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x + ↑y.cast).cast

Tactic:
ZMod.intCast_zmod_cast

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x + y).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x * y).cast = (x * ↑y.cast).cast

Tactic:
ZMod.intCast_zmod_cast

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x * y).cast = (x * y).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x - y).cast = (x - ↑y.cast).cast

Tactic:
ZMod.intCast_zmod_cast

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x - y).cast = (x - y).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x : ZMod n
⊢ (-x).cast = (-↑x.cast).cast

Tactic:
ZMod.intCast_zmod_cast

Goal state after:
n : ℕ
x : ZMod n
⊢ (-x).cast = (-x).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).val ≤ a.val + b.val

Tactic:
by
  cases n
  · simpa [ZMod.val] using! Int.natAbs_add_le _ _
  · simpa [ZMod.val_add] using! Nat.mod_le _ _

Goal state after:
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: n : ℕ
⊢ Subsingleton (ZMod n) ↔ n = 1

Tactic:
by
  constructor
  · obtain (_ | _ | n) := n
    · simpa [ZMod] using not_subsingleton _
    · simp [ZMod]
    · simpa [ZMod] using not_subsingleton _
  · rintro rfl
    infer_instance

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

Goal state before:
pp: case pos
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
simp [choose_eq_zero_of_lt lt]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
by
  by_cases lt : n + 1 < k
  · simp [choose_eq_zero_of_lt lt]
  · cases n with
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

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

Goal state before:
pp: case succ.e_tail.e_a
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) / (b + 2) = n✝ + 1

Tactic:
simp [add_mul_div_left, div_eq_of_lt hxb]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod n
k : ZMod n
⊢ f k.cast = k

Tactic:
by
  cases n
  · dsimp +instances [ZMod, ZMod.cast] at f k ⊢
    simp
  · dsimp [ZMod.cast]
    rw [map_natCast, natCast_zmod_val]

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

Goal state before:
pp: case cons.hxy
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
by_cases h' : L = []

Goal state after:
case pos
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case1
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
rcases ih with ⟨rfl, hdvd⟩

Goal state after:
case case1
p✝ p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case2
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd

Tactic:
rcases ih with ⟨rfl, hdvd⟩

Goal state after:
case case2
p✝ p e q : ℕ
hqp : ¬q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e, q).snd
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: 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 : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b
⊢ D = d

Tactic:
simpa [mod_eq_of_lt (w2 d List.mem_cons_self),
      mod_eq_of_lt (w1 D List.mem_cons_self)] using H

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

Goal state before:
pp: case cons
b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)

Tactic:
have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)

Goal state after:
case cons
b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
p n : ℕ
a✝ : (p.digits n).sum ≤ n
⊢ (p.digits (n + 1)).sum ≤ n + 1

Tactic:
induction p with
    | zero => rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    | succ p =>
      nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

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

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ∑ k ∈ range 1, ofDigits p (List.drop k tl) + (ofDigits p tl - tl.sum) + (p - 1) * ofDigits p [] =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
range_one,

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ∑ k ∈ {0}, ofDigits p (List.drop k tl) + (ofDigits p tl - tl.sum) + (p - 1) * ofDigits p [] =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
by
  obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
  · induction L with
    | nil => simp [ofDigits]
    | cons hd tl ih =>
      simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]
  · simp [ofDigits_one]
  · simp [lt_one_iff.mp h]
    cases L
    · rfl
    · simp [ofDigits]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ FiniteMultiplicity a b

Tactic:
by
  by_contra nh
  rw [← emultiplicity_eq_top, h] at nh
  trivial

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
contradiction

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

Goal state before:
pp: m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ p ^ k * m / p ^ (p ^ k * m).factorization p = m

Tactic:
by
  rw [ordCompl_self_pow_mul m k hp]
  exact (ordCompl_eq_self_iff_zero_or_not_dvd m hp).mpr (Or.inr hm)

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

Goal state before:
pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'

Goal state after:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.Algebra.CharP.Lemmas

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

Tactic:
rw [(h.pow_left _).mul_mul_mul_comm, mul_assoc (x * y)]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring 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:
by
  simp [eq_sub_iff_add_eq, ← add_pow_expChar_pow_of_commute _ _ (h.sub_left rfl)]

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

Goal state before:
pp: p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))

Tactic:
refine emultiplicity_le_emultiplicity_of_dvd_right ?_

Goal state after:
p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ p ∣ n

Tactic:
rw [Nat.dvd_iff_mod_eq_zero]

Goal state after:
case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ n % p = 0
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.degree = deg

Tactic:
by
  subst coeff_eq coeff_eq_deg deg_eq_deg
  rcases eq_or_ne m ⊥ with rfl | hh
  · exact bot_unique h_deg_le
  · obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh
    exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

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
⊢ (eval₂ C (C 1) f).natDegree = 0

Tactic:
eval₂_hom,

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ (C (eval 1 f)).natDegree = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : (p.comp (X + C x)).trailingCoeff * (q.comp (X + C x)).trailingCoeff ≠ 0
⊢ (p.comp (X + C x) * q.comp (X + C x)).natTrailingDegree =
    (p.comp (X + C x)).natTrailingDegree + (q.comp (X + C x)).natTrailingDegree

Tactic:
natTrailingDegree_mul' hpq

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
by_cases hpq : p %ₘ q = 0

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
⊢ (⇑derivative)^[x] p = 0

Tactic:
induction h : p.natDegree using Nat.strong_induction_on generalizing p x with | _ _ ih
  subst h
  obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'
  rw [Function.iterate_succ_apply]
  by_cases hp : p.natDegree = 0
  · rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]
  have := natDegree_derivative_lt hp
  exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree

Tactic:
rw [divByMonic_eq_zero_iff hg] at hfg

Goal state after:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ (aeval (S.val x)) p = 0

Tactic:
S.val_apply

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ (aeval ↑x) p = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : ¬q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

pp: case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
· simp [Polynomial.modByMonic_eq_of_not_monic _ h]

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
by_cases! h : ¬ q.Monic
  · simp [Polynomial.modByMonic_eq_of_not_monic _ h]
  apply Polynomial.modByMonic_eq_of_dvd_sub h
  have : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = (p₁ %ₘ q) * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q) := by ring
  rw [this]
  apply dvd_add
  all_goals
  · apply dvd_mul_of_dvd_right
    simp [Polynomial.modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ C ↑(n.descFactorial k) * X ^ (n - k) = ↑(n.descFactorial k) • X ^ (n - k)

Tactic:
smul_eq_C_mul

Goal state after:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ C ↑(n.descFactorial k) * X ^ (n - k) = C ↑(n.descFactorial k) * X ^ (n - k)
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi t ⊆ (univ.pi s)ᶜ
this : ∀ (i : ι), (s i ∩ t i).Nonempty
⊢ False

Tactic:
choose x hxs hxt using this

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
hsf : ∀ (i : ι), ∃ᶠ (x : α i) in f i, x ∈ s i
I : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi t ⊆ (univ.pi s)ᶜ
x : (i : ι) → α i
hxs : ∀ (i : ι), x i ∈ s i
hxt : ∀ (i : ι), x i ∈ t i
⊢ False
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i