mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b + n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ n + b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b + c * n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]

Tactic:
simp [ModEq]

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

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑(b - a) = 0

Tactic:
← add_right_cancel_iff (G := R) (a := a) (b := b - a),

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑(b - a) + ↑a = 0 + ↑a
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n : ℕ
⊢ ↑n = ↑(n % 2)

Tactic:
simp [natCast_eq_ite, Nat.even_iff]

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

Goal state before:
pp: x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ p = a * y

Tactic:
ha,

Goal state after:
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
h : p * a * y = p ^ 2
ha : x = p * a
⊢ p = a * y
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
l : Finset α
⊢ l.val.lists.Nodup

Tactic:
have h_nodup : l.val.Nodup := l.nodup

Goal state after:
α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.val.lists.Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
⊢ (foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L).length = n * L.length + r.length

Tactic:
length_foldr_permutationsAux2,

Goal state after:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
⊢ (map length L).sum + r.length = n * L.length + r.length
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
tsub_eq_zero_iff_le.mpr h

Goal state after:
case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
⊢ ∀ (is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
is

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
    (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
      ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
⊢ ∀ (is : List α),
    (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
        ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is

Tactic:
is

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
    (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
      ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (match decide (x = y) with
        | true => y :: takeWhile (fun x_1 ↦ decide (x = x_1)) l
        | false => []).length +
      1

Tactic:
simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false,
        not_false_iff, count_eq_zero_of_not_mem, Nat.zero_add, hx, decide_false, length_nil]

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

Goal state before:
pp: case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k + 1 = (hd :: tl).length

Tactic:
rw [length, Nat.succ_inj]

Goal state after:
case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k = tl.length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx

Tactic:
have key : l.length - 1 - k < l.length := by lia

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.reverse.prev l[k] ⋯ = l.next l[k] hx
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a = b

Tactic:
by
  rw [← sub_eq_zero]
  refine h _ ?_
  rw [smul_sub, h', sub_self]

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

Goal state before:
pp: case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
· simp [Nat.succ_le_succ_iff]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Chain r Cycle.nil

Tactic:
by trivial

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
⊢ (∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b) → Chain r ↑(a :: l)

Tactic:
intro hs

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
⊢ Chain r ↑(a :: l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b

Tactic:
intro hs

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
⊢ ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 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
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer G x

Tactic:
change (g₁⁻¹ * g₂) • x = x

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
ha,

Goal state after:
case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ ∉ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
rwa [ha, inv_mem_iff (x := b)]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
⊢ (H ⊓ K).index ≠ 0

Tactic:
by
  rw [← relIndex_top_right] at hH hK ⊢
  exact relIndex_inf_ne_zero hH hK

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a + ↑b) = ↑↑(a + b)

Tactic:
Fin.val_add,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a + ↑b) = ↑((↑a + ↑b) % (n✝ + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑(a + b) = ↑(Fin.cast h a + Fin.cast h b)

Tactic:
Fin.val_add,

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (↑a + ↑b) % (m + 1) = ↑(Fin.cast h a + Fin.cast h b)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (↑a + ↑b) % (m + 1) = ↑(Fin.cast h a + Fin.cast h b)

Tactic:
Fin.val_add,

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (↑a + ↑b) % (m + 1) = (↑(Fin.cast h a) + ↑(Fin.cast h b)) % (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
· rw [← val_intCast, val]; rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G✝ : Type u_1
G' : Type u_2
inst✝² : Group G✝
inst✝¹ : Group G'
H✝ K L : Subgroup G✝
f : G✝ →* G'
G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
h : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
rw [← AddSubgroup.finiteIndex_toSubgroup_iff] at h ⊢

Goal state after:
G✝ : Type u_1
G' : Type u_2
inst✝² : Group G✝
inst✝¹ : Group G'
H✝ K L : Subgroup G✝
f : G✝ →* G'
G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
h : (AddSubgroup.toSubgroup H).FiniteIndex
⊢ (AddSubgroup.toSubgroup H.normalCore).FiniteIndex
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1

pp: case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0

Tactic:
· rw [Nat.cast_sub, Nat.cast_one]
        rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk

Goal state after:
case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1

Tactic:
exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

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

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
rw [Nat.odd_iff, ← Nat.two_dvd_ne_zero, ← Nat.prime_two.coprime_iff_not_dvd] at hn
  rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]

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

Goal state before:
pp: n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ x.natAbs ≤ y.natAbs

Tactic:
rw [sub_eq_iff_eq_add] at he

Goal state after:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ x.natAbs ≤ y.natAbs
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n b : ℕ
l : List ℕ
⊢ n * ofDigits b l = ofDigits b (List.map (fun x ↦ n * x) l)

Tactic:
induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ multiplicity a b = 1

Tactic:
rw [multiplicity, emultiplicity_eq_top.mpr h]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 ⊤ = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case cons
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)

Tactic:
simp only [ofDigits, add_sub_add_left_eq_sub]
    exact dvd_mul_sub_mul h ih

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ↑(Nat.find h✝)
⊢ a ^ (n✝ + 1) ∣ b

pp: case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
· norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))

Goal state after:
case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by
  rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
  · rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab
  · contradiction
  · rw [hb.multiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

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

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (n.factorization p + 1) ∣ n
⊢ False

Tactic:
rw [← factorization_le_iff_dvd (pow_ne_zero _ hp.ne_zero) hn] at h

Goal state after:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hx : x ^ p = 1
hp : Odd p
n : ℕ
⊢ ∃ m, x ^ n = x ^ (2 * m)

Tactic:
by
  obtain ⟨r, rfl⟩ := hp
  have key : x ^ (2 * (r + 1)) = x := by
    have h2 : 2 * (r + 1) = 2 * r + 1 + 1 := by omega
    rw [h2, pow_succ, hx, one_mul]
  exact ⟨(r + 1) * n, by rw [← mul_assoc, pow_mul, key]⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac * orderOf x ∣ n

Tactic:
ha,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac * orderOf x ∣ orderOf x * a
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ n !.factorization p ≤ n / (p - 1)

Tactic:
factorization_factorial hp (Nat.lt_add_one (log p n))

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ (n.choose k).factorization p = #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
rw [← factorization_choose' hp ((Nat.sub_add_cancel hkn).symm ▸ hnb), Nat.sub_add_cancel hkn]

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization

Tactic:
refine ⟨factorization_div, ?_⟩

Goal state after:
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
  exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ n = a ^ m * 1

Tactic:
ha,

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ n = a ^ n * 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ n.factorization p = #({i ∈ Ico 1 n | p ^ i ∣ n})

Tactic:
by
  simp [← Icc_factorization_eq_pow_dvd n pp]

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

Goal state before:
pp: h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
by
        simpa [emultiplicity_mul, h2, prime_two, bit, factorial]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ x ^ card G = 1

Tactic:
rw [← Nat.card_eq_fintype_card, pow_card_eq_one']

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n✝ n : ℕ
⊢ (X ^ (n✝ + 1)).divX.coeff n = (if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)).coeff n

Tactic:
simp [coeff_X_pow]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (p.comp (C a * X + C b)) = rootMultiplicity (a * c + b) p

Tactic:
apply le_antisymm (rootMultiplicity_comp_C_mul_X_add_C_le p a b c ha)

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ⋯
⊢ rootMultiplicity (a * c + b) p ≤ rootMultiplicity c (p.comp (C a * X + C b))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
⊢ (expand R p) (contract p f) = f

Tactic:
obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›
  · rw [expand_one, contract_one]
  · have := Fact.mk hchar; exact expand_contract p hf hprime.ne_zero

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

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) a) + map (frobenius R p) ((expand R p) b) = (a + b) ^ p

Tactic:
ha,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ a ^ p + map (frobenius R p) ((expand R p) b) = (a + b) ^ p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t

Tactic:
ha,

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count x (x ::ₘ t) = 1 + count x t
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
x : A
⊢ Transcendental R x ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
rw [Transcendental, IsAlgebraic, not_exists]
  congr! 1; tauto

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ←
    map_modByMonic f hx]
  exact
    ⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by
      rw [H, Polynomial.map_zero]⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ multiplicity (X - C a) p ∣ p

Tactic:
apply pow_multiplicity_dvd

Goal state after:
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.inf ht.1, Set.to_countable _⟩

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

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

Tactic:
by
  induction k with
  | zero =>
    rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
  | succ k ih =>
    rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
    simp [mul_assoc, mul_left_comm]

Goal state after: