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

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ 0 < p - q

Tactic:
;

Goal state after:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
⊢ 0 < p - q
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ p - q + q ≤ w.length - q + (p - q).gcd q

Tactic:
;

Goal state after:
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
per_q' : (drop q w).HasPeriod q
gcd_stable : (p - q).gcd q = p.gcd q
drop_len : q ≤ (drop q w).length
take_eq : take q (drop q w) = take q w
⊢ p - q + q ≤ w.length - q + (p - q).gcd q
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1

pp: case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)

Tactic:
;

Goal state after:
case inr.inr.refine_1
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ ∀ (m_1 : List α), m_1 ∈ splitBy r l ++ splitBy r m → IsChain (fun x y ↦ r x y = true) m_1

case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)
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:
;

Goal state after:
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⟩
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen OneStep M N
X Y : Multiset α
a : α
hYa : ∀ (y : α), y ∈ Y → y < a
⊢ (X + Y).IsDershowitzMannaLT (X + {a})

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
hMN : TransGen OneStep M N
X Y : Multiset α
a : α
hYa : ∀ (y : α), y ∈ Y → y < a
⊢ (X + Y).IsDershowitzMannaLT (X + {a})
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
b : ℕ
⊢ ↑a ≤ ↑b ↔ ↑a ≤ ↑↑b

Tactic:
;

Goal state after:
a : ℚ≥0
b : ℕ
⊢ ↑a ≤ ↑b ↔ ↑a ≤ ↑↑b
Module: Mathlib.Data.Nat.Cast.SetInterval

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

Tactic:
;

Goal state after:
a : ℕ
⊢ Icc ↑⊥ ↑a = Icc 0 ↑a
Module: Mathlib.Data.Nat.Cast.SetInterval

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

Tactic:
;

Goal state after:
a : ℕ
⊢ Ico ↑⊥ ↑a = Ico 0 ↑a
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α (↑q.num / ↑q.den)

Tactic:
;

Goal state after:
q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α (↑q.num / ↑q.den)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons.mpr
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h : ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
⊢ a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
;

Goal state after:
case cons.mpr
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h : ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]
⊢ a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
Module: Mathlib.Data.Nat.Digits.Div

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

Tactic:
;

Goal state after:
n : ℕ
⊢ ↑10 % ↑11 = -1 % ↑11
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 + (k + 1))!
⊢ IsUnit ↑m !

Tactic:
rw [← add_assoc, add_right_comm] at hn_fac

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)!
⊢ IsUnit ↑m !
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)

Tactic:
let z := chineseRemainderOfList a s l' (co.perm hl coprime_comm.mpr)

Goal state after:
ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)
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:
;

Goal state after:
ι : 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)
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:
;

Goal state after:
ι : 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' ⋯)
Module: Mathlib.Data.Nat.Dist

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

Tactic:
by simp [dist, tsub_self]

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

Goal state before:
pp: n m : ℕ
h : n - m + (m - n) = 0
⊢ n = m

Tactic:
;

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

Goal state before:
pp: n m : ℕ
h : n = m
⊢ n - m + (m - n) = 0

Tactic:
;

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 - m + (m - n) = m - n

Tactic:
;

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 - m + (m - n) = n - m

Tactic:
;

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 - m + (m - n) + n

Tactic:
;

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 - m + (m - n))

Tactic:
;

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

Goal state before:
pp: n m : ℕ
⊢ n ≤ n - m + (m - n) + m

Tactic:
;

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 - m + (m - n))

Tactic:
;

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

Goal state before:
pp: n : ℕ
⊢ n - 0 + (0 - n) = n

Tactic:
;

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

Goal state before:
pp: n : ℕ
⊢ 0 - n + (n - 0) = n

Tactic:
;

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

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

Tactic:
;

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 - (k + m) + (k + m - (k + n)) = n - m + (m - n)

Tactic:
;

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 - k + (k - n) = l - m + (m - l)

Tactic:
;

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 - k + (k - n) ≤ n - m + (m - n) + (m - k + (k - m))

Tactic:
;

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 - j.succ + (j.succ - i.succ) = i - j + (j - i)

Tactic:
;

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 - j + (j - i)

Tactic:
;

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

Goal state before:
pp: a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ (k / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
;

Goal state after:
a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ (k / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ k) = a

Tactic:
;

Goal state after:
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun p k ↦ p ^ k) = a
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a

Tactic:
;

Goal state after:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 ↦ x1 ^ x2) = a
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case bc
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib l).sum < fib (a - 1)

Tactic:
;

Goal state after:
case bc
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib l).sum < fib (a - 1)
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n

Tactic:
;

Goal state after:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: ⊢ greatestFib 0 = 0

Tactic:
;

Goal state after:
⊢ greatestFib 0 = 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
exact_mod_cast choose_modEq_prod_range_choose ha₁ ha₂

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

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

Tactic:
by
  induction k with grind

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

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 2 m k = m * k

Tactic:
by
  induction k with grind

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

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 3 m k = m ^ k

Tactic:
by
  induction k with grind

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

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

Tactic:
by
  induction k with grind

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ 1 ≤ n - 1 ∧ ¬n = 0

Tactic:
;

Goal state after:
n : ℕ
h : IsPrimePow n
⊢ 1 ≤ n - 1 ∧ ¬n = 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).length ≤ n

Tactic:
;

Goal state after:
case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).length ≤ n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (Set.ofPred p)

Tactic:
;

Goal state after:
p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (Set.ofPred p)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (Set.ofPred p) = Nat.find h

Tactic:
;

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ sInf (Set.ofPred p) = Nat.find h
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
⊢ nth p k < f n

Tactic:
have : f k < f n := by apply hmono <;> grind

Goal state after:
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
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:
;

Goal state after:
case refine_2
n : PosNum
⊢ n.bit1.minFac = n.bit1 ↔ n.bit1.minFacAux (↑n) 1 = n.bit1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inl
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
this : nth p k < nth p (k + 1)
⊢ nth p k < nth p (k + 1) ∧ p (nth p k)

pp: case inr
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
· exact ⟨this, nth_mem _ fun hf => k.lt_succ_self.trans (hlt hf)⟩

Goal state after:
case inr
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred

Tactic:
;

Goal state after:
case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case neg
a✝ : PosNum
⊢ a✝.pred'.toZNum = (-neg a✝).pred

Tactic:
;

Goal state after:
case neg
a✝ : PosNum
⊢ a✝.pred'.toZNum = (-neg a✝).pred
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
hm : Valid' (↑x) nil ↑y
Hm : 0 < nil.size
H :
  l.size = 0 ∧ nil.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ nil.size ∧
        delta * l.size ≤ nil.size + r.size ∧ 3 * (nil.size + r.size) ≤ 16 * l.size + 9 ∧ nil.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x nil y r) o₂

pp: case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂

Tactic:
;

Goal state after:
case nil
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
hm : Valid' (↑x) nil ↑y
Hm : 0 < nil.size
H :
  l.size = 0 ∧ nil.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ nil.size ∧
        delta * l.size ≤ nil.size + r.size ∧ 3 * (nil.size + r.size) ≤ 16 * l.size + 9 ∧ nil.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x nil y r) o₂

case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1

Tactic:
;

Goal state after:
a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑p + ↑p

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit0 = ↑p + ↑p
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑p + ↑p + 1

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑p + ↑p + 1
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
hn' : n' ∈ Set.ofPred p
⊢ n' ∈ ↑(range n)

Tactic:
contrapose! hp

Goal state after:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ ∃ n' ≥ n, p n'