mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ Epi (lim.map f)

Tactic:
have : lim.map f = (Pi.isoLimit _).inv ≫ Limits.Pi.map (f.app ⟨·⟩) ≫ (Pi.isoLimit _).hom := by
      apply limit.hom_ext
      intro ⟨n⟩
      simp

Goal state after:
n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
this : lim.map f = (Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom
⊢ Epi (lim.map f)
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
w✝¹ : X
a✝¹ : g w✝¹ ∈ univ
w✝ : X
hy : f w✝ = f w✝¹
a✝ : g w✝ ∈ univ
⊢ g w✝¹ = g w✝

Tactic:
rw [f_inj hy]

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Tactic:
apply Comp.applicative_id_comp

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

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ Upto.GT p ⟨a, ha⟩ ⟨b, property✝⟩ ↔ InvImage (fun x1 x2 ↦ x1 < x2) (fun y ↦ x - ↑y) ⟨a, ha⟩ ⟨b, property✝⟩

Tactic:
dsimp [InvImage, Upto.GT]

Goal state after:
p : ℕ → Prop
x : ℕ
h : p x
a : ℕ
ha : ∀ (j : ℕ), j < a → ¬p j
b : ℕ
property✝ : ∀ (j : ℕ), j < b → ¬p j
⊢ a > b ↔ x - a < x - b
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ traverse (bitraverse (pure ∘ f✝) (pure ∘ f'✝)) x✝ = pure (bimap f✝ f'✝ x✝)

Tactic:
simp only [bitraverse_eq_bimap_id', traverse_eq_map_id', Function.comp_apply]; rfl

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝

Tactic:
rw [succ_add_eq_add_succ] at _this hk

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + (↑z).succ)
hk : Nat.find h' = n + (↑z).succ
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ take (Nat.succ 0) h v i = snoc (take 0 ⋯ v) (v ⟨0, h⟩) i

Tactic:
have h' : i = 0 := by ext; simp

Goal state after:
case zero
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
h' : i = 0
⊢ take (Nat.succ 0) h v i = snoc (take 0 ⋯ v) (v ⟨0, h⟩) i
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ∃ x, ¬x = b → ⟨a, x⟩ ∈ l

Tactic:
use b

Goal state after:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ¬b = b → ⟨a, b⟩ ∈ l
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by_cases ht : t.Nonempty

Goal state after:
case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by_cases ht : t.Nonempty

Goal state after:
case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a ∈ (head✝ :: tail✝).keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [not_or] at h

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ ¬a ∈ tail✝.keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.mk.left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ ¬fst✝ ∈ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).keys.erase fst✝

Tactic:
apply l_ih.not_mem_erase

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

Goal state before:
pp: 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

Tactic:
| _ 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.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
⊢ Injective embSigma

Tactic:
intro f g h
  ext i
  have := congr_fun (congrArg (⇑) h) ⟨k, i⟩
  simpa using this

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ (f a✝).slice i hid + (∑ x ∈ s✝, f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Tactic:
slice_add,

Goal state after:
case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ (f a✝ + ∑ x ∈ s✝, f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
Nat.add_comm

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ fib (-↑n + 1) * fib (-↑n - 1) - fib (-↑n) ^ 2 = (-1) ^ (-↑n).natAbs

Tactic:
obtain ⟨i, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
    simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]
    grind

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
by
  intro hk
  rw [← length_reverse] at hk
  rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
    reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]

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

Goal state before:
pp: α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
⊢ (x :: (l ++ [y])).reverse = x :: (l ++ [y]) → (x :: (l ++ [y])).Palindrome

Tactic:
hr

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipLeft bs = (as.zipLeft' bs).fst

Tactic:
rw [zipLeft, zipLeft']
  cases as with
  | nil => rfl
  | cons _ atl =>
    cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b

Tactic:
rw [List.forall_mem_iff_forall_getElem]

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (i : ℕ) (hi : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length ≤ b
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = true
h : m ∈ splitBy.loop r l b (a :: g) []
⊢ IsChain (fun x y ↦ r x y = true) m

pp: case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
· apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
      grind

Goal state after:
case h_2
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α},
    (∀ (b : α), b ∈ g.head? → r b a = true) →
      IsChain (fun y x ↦ r x y = true) g → m ∈ splitBy.loop r l a g [] → IsChain (fun x y ↦ r x y = true) m
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
h : m ∈ splitBy.loop r l b [] [g.reverse ++ [a]]
⊢ IsChain (fun x y ↦ r x y = true) m
Module: Mathlib.Data.List.PeriodicityLemma

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

Tactic:
by
  by_cases p_zero : p = 0
  · rw [p_zero, mod_zero]
  · cases lt_or_ge i p with
    | inl small =>
        have eq : i % p = i := mod_eq_of_lt small
        rw [eq]
    | inr large =>
        have len' : i - p < w.length := by lia
        have IH : w[(i - p) % p]? = w[i - p]? := per.getElem?_mod p (i - p) w len'
        rw [hasPeriod_iff_getElem?] at per
        have minus : i - p < w.length - p := by lia
        have per' := per (i - p) minus
        simp only [large, Nat.sub_add_cancel] at per'
        have mod : i % p = (i - p) % p := mod_eq_sub_mod large
        aesop

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

Goal state before:
pp: case pos
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
calc
        (take n w ++ w)[j]? = (take n w)[j]? := getElem?_append_left (by simp_all)
        _ = w[j]? := getElem?_take_of_lt j_lt_n
        _ = w[j % p]? := Eq.symm (mod_w j (by lia))

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit ↑(m + 1)!
⊢ IsUnit ↑m !

Tactic:
Nat.factorial_succ,

Goal state after:
case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + 1 + k)!
this : IsUnit ↑((m + 1) * m !)
⊢ IsUnit ↑m !
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
co : {x | x ∈ l}.Pairwise (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : {x | x ∈ m'}.Pairwise (Coprime on s)},
    ↑(Eq.ndrec (motive := fun m ↦
          m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun nod x co ↦ chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
      ↑(chineseRemainderOfList a s l lco)
⊢ ↑(Eq.ndrec (motive := fun x ↦
        x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
        (fun nod x co ↦ chineseRemainderOfList a s l ⋯) ⋯ nod' hs' co') =
    ↑(chineseRemainderOfList a s l' ⋯)

Tactic:
exact this.trans <| chineseRemainderOfList_perm a s pp hs lco

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
⊢ ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x

Tactic:
intro ⟨x₁, x₂⟩

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
⊢ (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1) → (k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ (k % p, k / p) = (x₁, x₂))
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ n • a.factorization ≤ b.factorization ↔ a.factorization ≤ b.factorization ⌊/⌋ n

Tactic:
le_floorDiv_iff_smul_le (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)

Goal state after:
case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ n • a.factorization ≤ b.factorization ↔ n • a.factorization ≤ b.factorization
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝¹ : k ≤ log 2 n
left✝ : 0 < k
hn₁ : n = n.minFac ^ k
i : ℕ
hi : i ∈ Icc 1 (n - 1)
⊢ n.minFac ∣ (n.minFac ^ k).choose i

Tactic:
exact Prime.dvd_choose_pow (minFac_prime_iff.mpr h.ne_one) (by grind) (by grind)

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ∃ x, ∃ (_ : 1 ≤ x ∧ x ≤ n - 1), ¬n.minFac ^ 2 ∣ n.choose x

Tactic:
refine ⟨n.minFac ^ (k - 1), ⟨one_le_pow _ _ (minFac_pos n), ?_⟩, ?_⟩

Goal state after:
case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) ≤ n - 1

case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ ¬n.minFac ^ 2 ∣ n.choose (n.minFac ^ (k - 1))
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | rs
  · rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact ι x
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)
  · rcases id l with _ | ⟨ls, ll, lx, lr⟩
    · exact node (rs + 1) nil x r
    · refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r
      rcases id ll with _ | lls
      · exact nil
      --should not happen
      rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
      · exact nil
      --should not happen
      exact
        if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x r)
        else
          node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
            (node (size lrr + rs + 1) lrr x r)

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

Goal state before:
pp: case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact node 3 (ι x) rx rr
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ (↑↑a).toZNum = pos a

Tactic:
PosNum.of_to_nat

Goal state after:
a : PosNum
⊢ (Num.pos a).toZNum = pos a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ -(↑↑a).toZNum = neg a

Tactic:
PosNum.of_to_nat

Goal state after:
a : PosNum
⊢ -(Num.pos a).toZNum = neg a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
⊢ ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
have : ∀ {r₂}, Num.ofZNum' (Num.sub' r (Num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d := by
    intro r₂
    apply Num.mem_ofZNum'.trans
    rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]
    simp

Goal state after:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
⊢ ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d