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

Goal state before:
pp: case zero
α : 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
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
⊢ (fun x ↦ assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x) = Fix.approx f 0

Tactic:
ext x : 1

Goal state after:
case zero
α : 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
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x) = Fix.approx f 0 x
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝² : WriterT ω M α✝
x✝¹ : α✝ → WriterT ω M β✝
x✝ : β✝ → WriterT ω M γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x ↦ x✝¹ x >>= x✝

Tactic:
ext; simp [mul_assoc]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b

pp: α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
case : i ≤ j
⊢ y = b

Tactic:
· rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption

Goal state after:
α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
case : i ≤ j
⊢ y = b
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁶ : Traversable t
inst✝⁵ : LawfulTraversable t
inst✝⁴ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ traverse (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)

Tactic:
by rw [h₂, Equiv.comp_traverse, h₂]; congr; rw [h₂]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = (DFinsupp.single a n) i

Tactic:
simp [count_replicate]

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ t ≤ s

Tactic:
by
      rw [eq_pure h, eq_pure (h.mono st)]; simpa using h _ (get_mem _) _ (st <| get_mem _)

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

Goal state before:
pp: case cons.none
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match none with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match none with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Tactic:
simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl

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

Goal state before:
pp: case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa [lookmap_cons_some _ _ h₁, h₂] using Perm.swap _ _ _

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
⊢ insertRec H0 IH ∅ = H0

Tactic:
change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0
  rw [insertRec]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
b' : β ⟨a, b⟩.fst
h' : dlookup ⟨a, b⟩.fst l = some b'
⊢ b ∈ dlookup a l

Tactic:
cases nd.eq_of_mk_mem h (of_mem_dlookup h')

Goal state after:
case refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : dlookup ⟨a, b⟩.fst l = some b
⊢ b ∈ dlookup a l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Tactic:
· rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l] <;> assumption

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂

Tactic:
lookup_union_left_of_not_in (h' _ hs₂),

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some ⟨a, b⟩ else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some ⟨a, b⟩ else none
⊢ x = y ∧ z = w

Tactic:
split_ifs at h₁ h₂ with h_2 h_1 <;> cases h₁

Goal state after:
case pos.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ ⟨a, b⟩ = w

case neg.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ ⟨a, b⟩ = w
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩

Goal state after:
case neg.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h✝ : ¬a' = x.fst
h : ¬x.fst = a'
tail_ih✝ : kerase x.fst (kerase a' xs) = kerase a' (kerase x.fst xs)
⊢ kerase x.fst (kerase a' (x :: xs)) = kerase a' (kerase x.fst (x :: xs))

Tactic:
simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
h : sizeOf xs.dedupKeys ≤ sizeOf xs
⊢ sizeOf (x :: xs).dedupKeys ≤ sizeOf (x :: xs)

Tactic:
simp only [dedupKeys_cons, kinsert_def, Sigma.eta]

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
h : sizeOf xs.dedupKeys ≤ sizeOf xs
⊢ sizeOf (x :: kerase x.fst xs.dedupKeys) ≤ sizeOf (x :: xs)
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ ↑(f.neLocus g) = {x | f x ≠ g x}

Tactic:
by
  ext
  exact mem_neLocus

Goal state after:
Module: Mathlib.Data.Finsupp.Pointwise

Goal state before:
pp: α : Type u₁
β : Type u₂
γ : Type u₃
δ : Type u₄
ι : Type u₅
inst✝ : Semiring β
r : β
f : α → β
m : α →₀ β
⊢ (r • f) • m = r • f • m

Tactic:
ext; simp [mul_assoc]

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

Goal state before:
pp: m n : ℤ
⊢ m >>> (-n) = m <<< n

Tactic:
← shiftLeft_neg,

Goal state after:
m n : ℤ
⊢ m <<< (- -n) = m <<< n
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : 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
hp : p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
simp_all only [get_eq_getElem]
      apply IH
      simp_all only [dropWhile_cons_of_pos]

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

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

Tactic:
convert! l.find?_eq_head?_dropWhile_not ?_

Goal state after:
case e'_3
α : Type u_1
p : α → Bool
l : List α
x✝ : α
⊢ p x✝ = !!p x✝
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
· rw [min_eq_right hlm, filter_lt_of_ge hlm]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r (b :: l) a g []

Tactic:
rw [splitBy.loop]
    split
    · exact IH
    · rw [splitByLoop_eq_append, mem_append]
      simpa using IH

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

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
minus : i - p < w.length - p
⊢ w[i % p]? = w[i]?

Tactic:
have per' := per (i - p) minus

Goal state after:
case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
minus : i - p < w.length - p
per' : w[i - p]? = w[i - p + p]?
⊢ w[i % p]? = w[i]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ r (m.getLast ha) ((g.reverse ++ [a] ++ [b]).head ⋯) = false

Tactic:
head_append_of_ne_nil

Goal state after:
case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ r (m.getLast ha) ((g.reverse ++ [a]).head ?h_1✝) = false

case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ g.reverse ++ [a] ≠ []
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
⊢ v.HasPeriod p

Tactic:
suffices ∀ j < v.length - p, v[j]? = v[j + p]? by simpa [hasPeriod_iff_getElem?]
  intro j len
  have shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]? := by
    rw [getElem?_append_right, Nat.add_sub_cancel, getElem?_append_left]
    all_goals lia
  have shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]? := by
    have eq : j + u.length + p - u.length = j + p := by lia
    rw [getElem?_append_right]
    · rw [getElem?_append_left]
      · exact congrArg (getElem? v) eq
      · lia
    · lia
  have : ∀ i < u.length + (v.length + w.length) - p,
      (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]? := by
    simp_all [hasPeriod_iff_getElem?]
  rw [← shift_position', ← shift_position]
  exact this (j + u.length) (by lia)

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ {x | x ∈ t.val}.Pairwise (Coprime on s)

Tactic:
simpa using pp

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

Goal state before:
pp: a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
h : (fib a + (map fib l).sum).greatestFib = a
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
by
      simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
      add_tsub_cancel_left, zeckendorf_sum_fib hl.2]

Goal state after:
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 / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ nth p 0 = Nat.find h

Tactic:
by
  rw [nth_zero]; convert! Nat.sInf_def h

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

Goal state before:
pp: p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
⊢ nth p a = 0

Tactic:
simp [nth_eq_zero, h']

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ #({x ∈ range (nth p 0) | p x}) = 0

Tactic:
card_eq_zero,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ {x ∈ range (nth p 0) | p x} = ∅
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(-(-n).bit1) = ↑n + ↑n - 1

Tactic:
cast_zneg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ -↑(-n).bit1 = ↑n + ↑n - 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑↑n.pred' + 1

Tactic:
rw [← n.to_nat_to_int, to_nat_eq_succ_pred]; rfl

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

Goal state before:
pp: n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -↑n / ↑d

Tactic:
n.to_int_eq_succ_pred,

Goal state after:
n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / ↑d
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑(n.pred' / Num.pos d).succ' = -↑n / -↑d

Tactic:
n.to_int_eq_succ_pred,

Goal state after:
n d : PosNum
⊢ ↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / -↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
h₁ : M.mk ⟨a, f₁⟩ = M.mk ⟨a, f₁⟩
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)

Tactic:
clear h₁

Goal state after:
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝, f✝⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a✝ fun j ↦ (f✝ j).approx (n + 1)) = CofixA.intro a fun j ↦ (f₁ j).approx (n + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).Sized

Tactic:
exact hl.node3L hr.2.1 hr.2.2

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : ↑P (α ::: P.W α)
⊢ P.wDest' (P.wMk' x) = x

Tactic:
by
  obtain ⟨a, f⟩ := x; rw [wMk', wDest'_wMk, split_dropFun_lastFun]

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

Goal state before:
pp: p : Nat.Primes
⊢ (↑p).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod

Tactic:
rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H : ?m.112
⊢ Valid' o₁
      (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
      ls + rs

Tactic:
by
        refine ⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩
        · refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)
          exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)
        · exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2
        · rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.2.1]; rfl

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₂, b₂✝⟩

Tactic:
left
        assumption

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₃, b₃⟩

Tactic:
left
        assumption

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

Goal state before:
pp: case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ (wp + 1) * (zp + 1) = x * y + 1

pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp + zp + wp * zp = x * y

Tactic:
· simp_all [← h]; ring

Goal state after:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp + zp + wp * zp = x * y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.zp + u.wp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x

Tactic:
add_comm u.zp

Goal state after:
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish

Tactic:
exact if_pos h

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

Goal state before:
pp: case node.node.hnc
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ ¬ls + rs ≤ 1

Tactic:
exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))

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

Goal state before:
pp: n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ n.dist m ≤ 1

Tactic:
Nat.dist_eq_sub_of_le H1,

Goal state after:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ m - n ≤ 1