mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
simp only [fix_def' (⇑f) h₀, not_exists, false_iff, notMem_none]
    simp only [dom_iff_mem, not_exists] at h₀
    intro; apply h₀

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

Goal state before:
pp: case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))

Tactic:
rw [lookmap, go, go]
    cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => simp

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

Goal state before:
pp: case some
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
· simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
by
    by_cases h : a = a'
    · subst h
      simp only [lookupAll_cons_eq, List.map]
      exact (lookupAll_sublist a l).cons_cons _
    · simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
      exact (lookupAll_sublist a l).cons _

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ traverse h (map g x) = traverse (h ∘ g) x

Tactic:
by
  induction x using Quotient.inductionOn
  simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]
  rw [← Traversable.traverse_map h g, List.map_eq_map]

Goal state after:
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
⊢ (m * n).divisors = m.divisors * n.divisors

Tactic:
by
  ext k
  simp_rw [mem_mul, mem_divisors, Nat.dvd_mul, mul_ne_zero_iff, ← exists_and_left,
    ← exists_and_right]
  simp only [and_assoc, and_comm, and_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ sizeOf (a :: l) ≤ sizeOf (a :: r)

Tactic:
cons.sizeOf_spec,

Goal state after:
α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ 1 + sizeOf a + sizeOf l ≤ sizeOf (a :: r)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
p : l₁ ~ l₂
l : List (Sigma β)
⊢ l₁.kunion l ~ l₂.kunion l

Tactic:
induction p generalizing l with

Goal state after:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
⊢ p f

Tactic:
induction hs : univ.sigma f using Finset.strongInductionOn generalizing f with | _ s ihs
   =>  _ 

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
s : Finset ((i : ι) × α i)
ihs : ∀ t ⊂ s, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
f : (i : ι) → Finset (α i)
hs : univ.sigma f = s
⊢ p f
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) s
⊢ s.sum.support = (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn with | _ a
  obtain ⟨l, hl, hd⟩ := hs
  suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! List.support_sum_eq a this
    simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
  simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl
  exact hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
by simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]; rfl

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

Goal state before:
pp: m n : ℕ
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)

Tactic:
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd

Goal state after:
case hp
m n : ℕ
⊢ ∀ (i n : ℕ), (↑i).bodd = ((n + i).bodd ^^ n.bodd)

case hn
m n : ℕ
⊢ ∀ (i m : ℕ), -[i+1].bodd = (m.bodd ^^ (m + i + 1).bodd)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

pp: case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Tactic:
· simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h

Goal state after:
case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

pp: case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Tactic:
· simp_rw [forall_exists_index, ← natCast_modEq_iff]; intro y ⟨h, c⟩; subst c; exact_mod_cast h

Goal state after:
case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p ((dropWhile p (hd :: tl)).get ⟨0, hl⟩) = true

Tactic:
simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : 0 < (dropWhile p l).length
⊢ ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Tactic:
induction l with
  | nil => cases hl
  | cons hd tl IH =>
    simp only [dropWhile]
    by_cases hp : p hd
    · simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]
    · simp [hp]

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

Goal state before:
pp: case false
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : false = p head
phh' : ¬p head = true
⊢ (!p head) = true

Tactic:
simpa using phh

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

Goal state before:
pp: case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true

Tactic:
simpa using phh

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l <+: l

Tactic:
rw [← reverse_suffix, rdropWhile, reverse_reverse]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l.reverse <:+ l.reverse
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true

Tactic:
decide_eq_true_eq

Goal state after:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true

Tactic:
decide_eq_true_eq

Goal state after:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)

Tactic:
obtain ⟨m, hgf'⟩ := H

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
Module: Mathlib.Data.List.Sections

Goal state before:
pp: case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
f : List α
h : f ∈ (head✝ :: tail✝).sections
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)

Tactic:
simp only [sections, mem_flatMap, mem_map] at h

Goal state after:
case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
f : List α
h : ∃ a, a ∈ tail✝.sections ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ ∀ (s : List α), s.length < (head :: tail).length → Acc (Shortlex r) s

Tactic:
intro l ll

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ Acc (Shortlex r) l
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i % p]? = w[i]?

Tactic:
p_zero,

Goal state after:
case pos
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : p = 0
⊢ w[i % 0]? = w[i]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil.cons
α : Type u_1
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
c : α
m : List α
ha : ∀ (x : α), x ∈ (c :: m).head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r (c :: m) a g [] = (g.reverse ++ [a]) :: splitBy r (c :: m)

Tactic:
| cons c m =>

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l

Tactic:
rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ ∀ (x : α), x ∈ l.flatten.head? → r (a.getLast ⋯) x = false
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: case mp
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

pp: case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n

Tactic:
· intro h
    exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩

Goal state after:
case mpr
m n : ℕ
hm : m ≠ 1
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !) → m.minFac ≤ n
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n = m
⊢ n.dist m = 0

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
h : n = m
⊢ n - m + (m - n) = 0
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ n.dist m = m - n

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
h : n ≤ m
⊢ n - m + (m - n) = m - n
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ n.dist m = n - m

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
h : m ≤ n
⊢ n - m + (m - n) = n - m
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ m ≤ n.dist m + n

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
⊢ m ≤ n - m + (m - n) + n
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ m ≤ n + n.dist m

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
⊢ m ≤ n + (n - m + (m - n))
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n ≤ n.dist m + m

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
⊢ n ≤ n - m + (m - n) + m
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n ≤ m + n.dist m

Tactic:
unfold Nat.dist

Goal state after:
n m : ℕ
⊢ n ≤ m + (n - m + (m - n))
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n : ℕ
⊢ n.dist 0 = n

Tactic:
unfold Nat.dist

Goal state after:
n : ℕ
⊢ n - 0 + (0 - n) = n
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n : ℕ
⊢ dist 0 n = n

Tactic:
unfold Nat.dist

Goal state after:
n : ℕ
⊢ 0 - n + (n - 0) = n
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n k m : ℕ
⊢ (n + k).dist (m + k) = n.dist m

Tactic:
unfold Nat.dist

Goal state after:
n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m - n)
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: k n m : ℕ
⊢ (k + n).dist (k + m) = n.dist m

Tactic:
unfold Nat.dist

Goal state after:
k n m : ℕ
⊢ k + n - (k + m) + (k + m - (k + n)) = n - m + (m - n)
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m k l : ℕ
h : n + m = k + l
⊢ n.dist k = l.dist m

Tactic:
unfold Nat.dist

Goal state after:
n m k l : ℕ
h : n + m = k + l
⊢ n - k + (k - n) = l - m + (m - l)
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m k : ℕ
⊢ n.dist k ≤ n.dist m + m.dist k

Tactic:
unfold Nat.dist

Goal state after:
n m k : ℕ
⊢ n - k + (k - n) ≤ n - m + (m - n) + (m - k + (k - m))
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
⊢ i.succ.dist j.succ = i.dist j

Tactic:
unfold Nat.dist

Goal state after:
i j : ℕ
⊢ i.succ - j.succ + (j.succ - i.succ) = i - j + (j - i)
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
h : i ≠ j
⊢ 0 < i.dist j

Tactic:
unfold Nat.dist

Goal state after:
i j : ℕ
h : i ≠ j
⊢ 0 < i - j + (j - i)
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.ceilRoot (a ^ n) = a

Tactic:
by
  simp [ceilRoot_def, pos_iff_ne_zero.2, hn]; split_ifs <;> simp [*]

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

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ p ^ multiplicity p n ∈ Icc 1 (n - 1)

Tactic:
by grind [le_of_dvd hn (pow_multiplicity_dvd p n)]

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).getD n 0 = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

Tactic:
Finset.orderEmbOfFin_apply,

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).getD n 0 = (hf.toFinset.sort fun a b ↦ a ≤ b)[⟨n, hn⟩]
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n : PosNum
⊢ ↑n.minFac = (↑n).minFac

Tactic:
by
  obtain - | n := n
  · simp [minFac]
  · rw [minFac, Nat.minFac_eq, if_neg]
    swap
    · simp [← two_mul]
    rw [minFacAux_to_nat]
    · rfl
    simp only [cast_one, cast_bit1]
    rw [Nat.sqrt_lt]
    calc
      (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
      _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
      _ < _ := by simp [mul_lt_mul]
  · rw [minFac, Nat.minFac_eq, if_pos]
    · rfl
    simp [← two_mul]

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n

Tactic:
refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)

Goal state after:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ ⋯.toFinset ⊆ range n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ZNum.ofInt' (-[0+1] + 1) = ZNum.ofInt' -[0+1] + 1

Tactic:
change ZNum.ofInt' 0 = ZNum.ofInt' (-[0+1]) + 1

Goal state after:
⊢ ZNum.ofInt' 0 = ZNum.ofInt' -[0+1] + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
⊢ m ∈ ofZNum' (ZNum.neg p)

Tactic:
cases m <;> cases h

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
⊢ Valid' o₁ (l.node3L x rl rx rr) o₂

Tactic:
suffices BalancedSz (size l) (size rl) ∧ BalancedSz (size l + size rl + 1) (size rr) by
      exact hl.node3L hr.left hr.right this.1 this.2

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

pp: case pos.inl.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
· rw [rl0] at this ⊢
        rw [le_antisymm (balancedSz_zero.1 this.symm) rr0]
        decide

Goal state after:
case pos.inl.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size = 0
⊢ 2 * r.size ≤ 9 * 0 + 5

Tactic:
exact le_trans (Nat.mul_le_mul_left _ (H₁ l0)) (by decide)

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balance' x r) o₂

Tactic:
refine hl.balance' hr ?_

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: d : ℕ
u : PrimeMultiset
⊢ (d • u).prod = u.prod ^ d

Tactic:
induction d with

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

Goal state before:
pp: n m : ℕ+
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
let u := factorMultiset n
  let v := factorMultiset m
  have : n = u.prod := (prod_factorMultiset n).symm; rw [this]
  have : m = v.prod := (prod_factorMultiset m).symm; rw [this]
  rw [← PrimeMultiset.prod_add]
  repeat' rw [PrimeMultiset.factorMultiset_prod]

Goal state after: