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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
v : β → α → β
b : β
inst✝ : RightCommutative v
⊢ foldr (flip v) b l = foldl v b l

Tactic:
induction l generalizing b

Goal state after:
case nil
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
b : β
⊢ foldr (flip v) b [] = foldl v b []

case cons
α : Type u_1
β : Type u_2
v : β → α → β
inst✝ : RightCommutative v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {b : β}, foldr (flip v) b tail✝ = foldl v b tail✝
b : β
⊢ foldr (flip v) b (head✝ :: tail✝) = foldl v b (head✝ :: tail✝)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ find? p l = some ((dropWhile (fun x ↦ !p x) l).head ⋯)

Tactic:
by
  rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]

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

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

Tactic:
rw [← reverse_prefix, rtakeWhile, reverse_reverse]

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

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ Ico n m = []

Tactic:
by
  simp [Ico, Nat.sub_eq_zero_iff_le.mpr h]

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

Goal state before:
pp: n m l : ℕ
⊢ ∀ (a : ℕ), ¬a ∈ Ico n m ∩ Ico m l

Tactic:
intro a

Goal state after:
n m l a : ℕ
⊢ ¬a ∈ Ico n m ∩ Ico m l
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.zero.succ
α : 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 : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ 0 = n✝ + 1

pp: case cons.succ.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
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

pp: case cons.succ.succ
α : 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
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
· simp [hx.left] at h

Goal state after:
case cons.succ.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
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) 0
⊢ n✝ + 1 = 0

case cons.succ.succ
α : 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
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
⊢ splitBy r l = [] ↔ l = []

Tactic:
have := flatten_splitBy r l
  refine ⟨fun _ ↦ ?_, ?_⟩ <;> simp_all

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

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a.length = 0
⊢ Acc (Shortlex r) a

Tactic:
| zero =>

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

Goal state before:
pp: case inr.inr
α : 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
⊢ ∀ i < (take n w ++ w).length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?

Tactic:
have mod_w : ∀ i < w.length, w[i % p]? = w[i]? := (per.getElem?_mod)

Goal state after:
case inr.inr
α : 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 < (take n w ++ w).length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j

Tactic:
replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
inhabited_h : Inhabited n
i : l
j : m
h : (mulLeftLinearMap n R a) (Matrix.single j default 1) = 0 (Matrix.single j default 1)
⊢ a i j = 0 i j
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
⊢ fst (∑ j, A i✝ j * B j j✝) = ∑ j, fst (A i✝ j) * fst (B j j✝)

Tactic:
fst_sum

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Tactic:
tsub_add_cancel_of_le

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M

case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ {b} ≤ M
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ b ∣ n ↔ ↑b ∣ ofDigits c (b'.digits n)

Tactic:
rw [← Int.natCast_dvd_natCast]
  exact
    dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd

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

Goal state before:
pp: case zero
A : Type u_1
inst✝ : Semiring A
m : ℕ
hn_fac : IsUnit ↑(m + 0)!
⊢ IsUnit ↑m !

Tactic:
| zero =>

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

Goal state before:
pp: case zero
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
⊢ IsUnit ↑0! ↔ 0 < p

Tactic:
| zero =>

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

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
h : 0 < p
⊢ IsUnit ↑0!

Tactic:
| zero =>

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

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
mem_product,

Goal state after:
case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : ¬((k % p, k / p).1 ∈ range (n % p + 1) ∧ (k % p, k / p).2 ∈ range (n / p + 1))
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
⊢ (map fib (a :: l)).sum < fib n

Tactic:
simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons] at hl
    have : ∀ b, b ∈ head? (l ++ [0]) → b < a - 1 :=
      fun b hb ↦ lt_tsub_iff_right.2 <| hl.1 _ <| mem_of_mem_head? hb
    simp only [mem_append, mem_singleton, ← isChain_iff_pairwise, or_imp, forall_and, forall_eq,
      zero_add] at hl
    calc
      fib a + (map fib l).sum < fib a + fib (a - 1) := by gcongr; exact sum_fib_lt hl.2 this
      _ ≤ fib n := by
        rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']; exact fib_mono (hn _ rfl)

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

Goal state before:
pp: case zero
k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p ^ 0 * a).choose (p ^ 0 * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
| zero =>

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

Goal state before:
pp: case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k

Tactic:
· rcases subset_range_nth ha with ⟨n, rfl⟩
    rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h

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

Goal state before:
pp: case zero
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}
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ f 0 ≤ nth p 0

Tactic:
| zero =>

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

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

Tactic:
by
  rcases id l with _ | ⟨ls, ll, lx, lr⟩
  · rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact ι x
    · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · cases id rr
        · exact node 2 nil x r
        · exact node 3 (ι x) rx rr
      · rcases id rr with _ | rrs
        · exact node 3 (ι x) rlx ι rx
        · 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)
  · rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · 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)
    · refine
        if delta * ls < rs then ?_ else if delta * rs < ls then ?_ else node (ls + rs + 1) l x r
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact nil
        --should not happen
        rcases id rr with _ | rrs
        · exact nil
        --should not happen
        exact
          if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
          else
            node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
              (node (size rlr + rrs + 1) rlr rx rr)
      · 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 (lrs + rs + 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.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
⊢ {n ∈ range (nth p (k + 1)) | p n} ⊆ insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
intro a

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
k a : ℕ
⊢ a ∈ {n ∈ range (nth p (k + 1)) | p n} → a ∈ insert (nth p k) ({n ∈ range (nth p k) | p n})
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case zero
p : ℕ → Prop
inst✝ : DecidablePred p
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ count p (nth p 0) = 0

Tactic:
| zero =>

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n

Tactic:
refine (count_monotone p).reflect_lt ?_
  rwa [count_nth]
  exact fun hf => h.trans_le (count_le_card hf n)

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

Goal state before:
pp: b : ZNum
⊢ ↑(b * 0) = ↑b * ↑0

Tactic:
cases b <;> exact (mul_zero _).symm

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

Goal state before:
pp: n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNumNeg = -(Num.ofNat' (n + 1)).toZNum

Tactic:
Num.zneg_toZNum

Goal state after:
n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNumNeg = (Num.ofNat' (n + 1)).toZNumNeg
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
hl : t.Sized
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
⊢ C t

Tactic:
by
  induction t with
  | nil => exact H0
  | node _ _ _ _ t_ih_l t_ih_r =>
    rw [hl.eq_node']
    exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
intro a

Goal state after:
α : Type u_1
a : ZNum
⊢ ∀ (b c : ZNum), a ≤ b → b ≤ c → a ≤ c
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
intro a

Goal state after:
α : Type u_1
a : ZNum
⊢ ∀ (b : ZNum), a < b ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a ≤ b → b ≤ a → a = b

Tactic:
intro a

Goal state after:
α : Type u_1
a : ZNum
⊢ ∀ (b : ZNum), a ≤ b → b ≤ a → a = b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a ≤ b ∨ b ≤ a

Tactic:
intro a

Goal state after:
α : Type u_1
a : ZNum
⊢ ∀ (b : ZNum), a ≤ b ∨ b ≤ a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n).toZNumNeg = -(↑n).toZNum

Tactic:
Num.zneg_toZNum

Goal state after:
n : ℕ
⊢ (↑n).toZNumNeg = (↑n).toZNumNeg
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
r₂ : Num
⊢ Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d

Tactic:
apply Num.mem_ofZNum'.trans

Goal state after:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ r.sub' (Num.pos d) = r₂.toZNum ↔ ↑r = ↑r₂ + ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F (succ 0)
h : Agree x y
⊢ truncate y = x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
i : X
⊢ Agree (sCorec f i 0) (sCorec f i (succ 0))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (x (succ 0)) = head' (x 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Approx.sMk x.dest 0 = x.approx 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x

Tactic:
| zero =>

Goal state after:
case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.zero
F : PFunctor.{uA, uB}
x y : F.M
h : Agree (x.approx 0) (y.approx (0 + 1))
⊢ Agree' 0 x y

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.zero
F : PFunctor.{uA, uB}
x y : F.M
h : Agree' 0 x y
⊢ Agree (x.approx 0) (y.approx (0 + 1))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : ∀ (ps : Path F), 0 = length ps → iselect ps x = iselect ps y
⊢ x.approx (0 + 1) = y.approx (0 + 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x.approx 0 = y.approx 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case pos
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
H :
  iselect ps s₁ = iselect ps s₂ ∧
    ∃ a f f', isubtree ps s₁ = M.mk ⟨a, f⟩ ∧ isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
exact H.left

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

Goal state before:
pp: α : Type u_1
x✝ : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ l.splitMax' x (node ls ll lx lr) = ((node x✝ l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))

Tactic:
by rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]

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

Goal state before:
pp: case zero
u : PrimeMultiset
⊢ (0 • u).prod = u.prod ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ (m.factorMultiset + (n.factorMultiset - m.factorMultiset)).prod = n

Tactic:
add_tsub_cancel_of_le h,

Goal state after:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ n.factorMultiset.prod = n
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_3
α : 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' (↑(rl.findMin' rx)) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ l',
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ r',
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
    ls + rs

Tactic:
· rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl

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

Goal state before:
pp: case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False

Tactic:
· exact hab.not_ge hba

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 ⟹ α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 i✝ '' univ) → u ∈ f i✝ '' univ

Tactic:
intro h'
    apply h' _ _ rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H : ?m.362
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
refine ⟨h.left.balanceR vr H, ?_⟩

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ l', Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ r', Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)

Tactic:
intro a

Goal state after:
case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
a : (P F).A
⊢ ∀ (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x : (P F).M α
y : Cofix F α
⊢ r (Quot.mk Mcongr x) y → Quot.mk Mcongr x = y

Tactic:
rcases y

Goal state after:
case mk.mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x : (P F).M α
y : Cofix F α
a✝ : (P F).M α
⊢ r (Quot.mk Mcongr x) (Quot.mk Mcongr a✝) → Quot.mk Mcongr x = Quot.mk Mcongr a✝