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

Goal state before:
pp: case nil
α : Type u
β : Type v
⊢ [].zipRight' [] = (map (fun b ↦ (none, b)) [], [])

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight' (head✝ :: tail✝) = (map (fun b ↦ (none, b)) (head✝ :: tail✝), [])

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left f [] [] = map (fun a ↦ f a none) []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left f (head✝ :: tail✝) [] = map (fun a ↦ f a none) (head✝ :: tail✝)

Tactic:
rfl

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

Goal state before:
pp: n m : ℕ
h : n < m
⊢ [n] ++ Ico n.succ m = n :: Ico (n + 1) m

Tactic:
rfl

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

Goal state before:
pp: case pos
n m : ℕ
h : n < m
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
rw [eq_cons h]
    unfold List.Ico
    exact isChain_range' _ (_ + 1) 1

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

Goal state before:
pp: case nil
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right f [] [] = map (f none) []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head✝ : β
tail✝ : List β
⊢ map₂Right f [] (head✝ :: tail✝) = map (f none) (head✝ :: tail✝)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
⊢ [].zipLeft [] = map (fun a ↦ (a, none)) []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft [] = map (fun a ↦ (a, none)) (head✝ :: tail✝)

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
bs : List β
⊢ zipWithLeft Prod.mk [] bs = (zipWithLeft' Prod.mk [] bs).fst

Tactic:
rfl

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

Goal state before:
pp: case cons.nil
α : Type u
β : Type v
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) [] = (zipWithLeft' Prod.mk (head✝ :: atl) []).fst

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u
β : Type v
⊢ [].zipRight [] = map (fun b ↦ (none, b)) []

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = map (fun b ↦ (none, b)) (head✝ :: tail✝)

Tactic:
rfl

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

Goal state before:
pp: case cons.zero.zero
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
hn hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = filter (fun x ↦ decide (x < n + 1)) (Ico n m)

Tactic:
exact filter_congr fun _ _ => by
    simpa using Nat.lt_succ_iff.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ ((f a b (foldr (fun ab s ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).1).1,
      (f a b (foldr (fun ab s ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).1).2 ::
        (foldr (fun ab s ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).2) =
    foldr (fun ab s ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) ((a :: as).zip (b :: bs))

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
cases t with
  | nil =>
    rw [List.append_nil]
    exact h
  | cons head tail =>
    apply of_length_lt
    rw [List.length_append, List.length_cons]
    lia

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔ ∀ i < w.length - p, w[i]? = w[i + p]?

Tactic:
by
  constructor
  · rw [HasPeriod]
    intro pref j len
    have i1 : j < w.length := by lia
    have i2 : j + p < w.length := by lia
    have min : p < w.length := by lia
    have : j + p - (List.take p w).length = j := by
      simp_all [min_eq_left_of_lt]
    simp_all [getElem_append_right, IsPrefix.getElem pref, min_eq_left_of_lt]
  · intro lhs
    rw [HasPeriod]
    have drop : drop p w <+: w := by
      simp only [prefix_iff_getElem?, length_drop, getElem_drop]
      intro i leni
      have len : i + p < w.length := by lia
      simp_all only [getElem?_pos, add_comm p i]
    rw [← prefix_append_right_inj (w.take p)] at drop
    simp_all

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

Goal state before:
pp: α : 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) []
⊢ ∀ (b_1 : α), b_1 ∈ (a :: g).head? → r b_1 b = true

Tactic:
grind

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

Goal state before:
pp: case h_2.inr
α : 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
hm : m ∈ splitBy.loop r l b [] []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
grind

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

Goal state before:

Tactic:
(j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h1
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ ∑ i, fst (A i✝ i * B i j✝) = ∑ j, fst (A i✝ j) * fst (B j j✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ diagonal (fun m ↦ r) i j, of fun i j ↦ 0) = inl (diagonal fun m ↦ r)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₁
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inl val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inl val✝) j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₂
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inr val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inr val✝) j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂).map f i✝ (Sum.inl val✝) = (A₁.map f).fromCols (A₂.map f) i✝ (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂).map f i✝ (Sum.inr val✝) = (A₁.map f).fromCols (A₂.map f) i✝ (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₁
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inl val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₂
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inr val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₁
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inl val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₂
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inr val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v : m₁ ⊕ m₂ → R
⊢ v ᵥ* B₁.fromRows B₂ = v ∘ Sum.inl ᵥ* B₁ + v ∘ Sum.inr ᵥ* B₂

Tactic:
simp [← sumElim_vecMul_fromRows]

Goal state after:
Module: Mathlib.Data.NNRat.Encodable

Goal state before:
pp: x✝ : ℚ≥0
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
num : ℕ
reduced✝ : (↑num).natAbs.Coprime den✝
hq : 0 ≤ { num := ↑num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }
⊢ (fun x ↦
        match x with
        | ⟨num, ⟨den, prop⟩⟩ => ⟨{ num := ↑num, den := den, den_nz := ⋯, reduced := ⋯ }, ⋯⟩)
      ((fun q ↦ ⟨q.num, ⟨q.den, ⋯⟩⟩) ⟨{ num := ↑num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }, hq⟩) =
    ⟨{ num := ↑num, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }, hq⟩

Tactic:
rfl

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

Tactic:
rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ Y₂ + X₂ = Z₁ + X₁
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inl
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hNM' : N.OneStep M
hNM : (a ::ₘ N).OneStep (a ::ₘ M)
⊢ Acc OneStep (a ::ₘ N)

pp: case intro.intro.inr
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
hNM : (M + N).OneStep (a ::ₘ M)
⊢ Acc OneStep (M + N)

Tactic:
· exact ihM _ hNM'

Goal state after:
case intro.intro.inr
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
hNM : (M + N).OneStep (a ::ₘ M)
⊢ Acc OneStep (M + N)
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = 0⁻¹

Tactic:
inv_zero,

Goal state after:
case inl
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = 0
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Icc ↑⊥ ↑a = Icc 0 ↑a

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Ico ↑⊥ ↑a = Ico 0 ↑a

Tactic:
rfl

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

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ↑(chineseRemainder ⋯ (a i) ↑(chineseRemainderOfList a s l ⋯)) < s i * (List.map s l).prod

Tactic:
refine chineseRemainder_lt_mul this (a i) (chineseRemainderOfList a s l co.of_cons)
      (hs i List.mem_cons_self) ?_

Goal state after:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ (List.map s l).prod ≠ 0
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ ↑10 % ↑11 = -1 % ↑11

Tactic:
rfl

Goal state after:
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
nod''✝ : (↑l).Nodup
hs''✝ : ∀ i ∈ ↑l, s i ≠ 0
co''✝ : {x | x ∈ ↑l}.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 ⋯) ⋯ nod''✝ hs''✝ co''✝) =
    ↑(chineseRemainderOfList a s l lco)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: ⊢ greatestFib 0 = 0

Tactic:
rfl

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

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 0 m k = k + 1

Tactic:
grind

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

Goal state before:
pp: n m : ℕ
⊢ hyperoperation (n + 3) m 0 = 1

Tactic:
grind

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

Goal state before:
pp: n m k : ℕ
⊢ hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

Tactic:
grind

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

Goal state before:
pp: case zero
m : ℕ
⊢ hyperoperation 1 m 0 = m + 0

Tactic:
grind

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

Goal state before:
pp: case succ
m n✝ : ℕ
a✝ : hyperoperation 1 m n✝ = m + n✝
⊢ hyperoperation 1 m (n✝ + 1) = m + (n✝ + 1)

Tactic:
grind

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

Goal state before:
pp: case zero
m : ℕ
⊢ hyperoperation 2 m 0 = m * 0

Tactic:
grind

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

Goal state before:
pp: case succ
m n✝ : ℕ
a✝ : hyperoperation 2 m n✝ = m * n✝
⊢ hyperoperation 2 m (n✝ + 1) = m * (n✝ + 1)

Tactic:
grind

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

Goal state before:
pp: case zero
m : ℕ
⊢ hyperoperation 3 m 0 = m ^ 0

Tactic:
grind

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

Goal state before:
pp: case succ
m n✝ : ℕ
a✝ : hyperoperation 3 m n✝ = m ^ n✝
⊢ hyperoperation 3 m (n✝ + 1) = m ^ (n✝ + 1)

Tactic:
grind

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

Goal state before:
pp: case zero
m : ℕ
⊢ hyperoperation (0 + 2) m 1 = m

Tactic:
grind

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

Goal state before:
pp: case succ
m n✝ : ℕ
a✝ : hyperoperation (n✝ + 2) m 1 = m
⊢ hyperoperation (n✝ + 1 + 2) m 1 = m

Tactic:
grind

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

Goal state before:
pp: case zero
⊢ hyperoperation (0 + 1) 2 2 = 4

Tactic:
grind

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

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : hyperoperation (n✝ + 1) 2 2 = 4
⊢ hyperoperation (n✝ + 1 + 1) 2 2 = 4

Tactic:
grind

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

Goal state before:
pp: case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 0 = if Even 0 then 1 else 0

Tactic:
grind

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

Goal state before:
pp: case succ
n n✝ : ℕ
a✝ : hyperoperation (n + 4) 0 n✝ = if Even n✝ then 1 else 0
⊢ hyperoperation (n + 4) 0 (n✝ + 1) = if Even (n✝ + 1) then 1 else 0

Tactic:
grind

Goal state after:
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)
⊢ i ≠ 0

Tactic:
grind

Goal state after:
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)
⊢ i ≠ n.minFac ^ k

Tactic:
grind

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

Goal state before:
pp: 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
⊢ k - (k - 1) < 2

Tactic:
grind

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

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ 1 ∈ Icc 1 (n - 1)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case lt
o₂ : Ordering
⊢ (lt.dthen fun x ↦ o₂) = lt.then o₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case eq
o₂ : Ordering
⊢ (eq.dthen fun x ↦ o₂) = eq.then o₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: case gt
o₂ : Ordering
⊢ (gt.dthen fun x ↦ o₂) = gt.then o₂

Tactic:
rfl

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

Goal state before:
pp: case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

Tactic:
grind

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

Goal state before:
pp: case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

Tactic:
grind

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

Goal state before:
pp: case a
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k < n

Tactic:
grind

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

Goal state before:
pp: case pos.h
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
this : f k < f n
⊢ nth p k < f n

Tactic:
grind

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

Goal state before:
pp: case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝ : n < k.bit1 * k.bit1
⊢ ↑n = ↑n

Tactic:
rfl

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

Goal state before:
pp: case pos
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : k.bit1 ∣ n
⊢ ↑k.bit1 = ↑k.bit1

Tactic:
rfl

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

Goal state before:
pp: case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
rfl

Goal state after:
case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3

Tactic:
rfl

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑2 = 2

Tactic:
rfl

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

Goal state before:
pp: case refine_2
n : PosNum
⊢ n.bit1.minFac = n.bit1 ↔ n.bit1.minFacAux (↑n) 1 = n.bit1

Tactic:
rfl

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

Goal state before:
pp: case succ.refine_2.ha
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

Tactic:
grind

Goal state after: