mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ {x ∈ Ico a b | r ∣ x} ↔ x ∈ map { toFun := fun x ↦ x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

Tactic:
simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]

Goal state after:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a ≤ x ∧ x < b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a ≤ a_1 * r ∧ a_1 * r < b) ∧ { toFun := fun x ↦ x * r, inj' := ⋯ } a_1 = x
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n✝ : ℕ
⊢ drop ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (take (n✝ + 1) (xs ++ [x]).reverse).reverse

Tactic:
· simp [drop_append, IH]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
⊢ zipWith f [] l = []

Tactic:
cases l <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
⊢ zipWith f l [] = []

Tactic:
cases l <;> rfl

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

Goal state before:
pp: case cons.succ.succ.refine_1
α : 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 : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ ∈ {n | n ≤ tl.length}

pp: case cons.succ.succ.refine_2
α : 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 : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ∈ {n | n ≤ tl.length}

Tactic:
· simpa [Nat.succ_le_succ_iff] using hn

Goal state after:
case cons.succ.succ.refine_2
α : 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 : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝ ∈ {n | n ≤ tl.length}
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ ((head :: tail).splitLengths l)[i].length ≤ (head :: tail)[i]

Tactic:
simp only [splitLengths_cons]
    cases i
    · simp
    · simp only [getElem_cons_succ, tail_ih]

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

Goal state before:
pp: case intro.intro.inr.cons
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h2len : (xa :: xs).length = (xa :: xb).length
h : Lex r xs xb
⊢ Acc (Shortlex r) (xa :: xs)

Tactic:
simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

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

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

Tactic:
intro i

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
⊢ ((splitBy r l).getLast ⋯).getLast ⋯ = l.getLast hn

Tactic:
simp [getLast_getLast_eq_getLast_flatten]

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

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ ∀ (i : ℕ) (h : i < w.length - p), w[i]? = some w[p + i]

Tactic:
intro i

Goal state after:
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
i : ℕ
⊢ ∀ (h : i < w.length - p), w[i]? = some w[p + i]
Module: Mathlib.Data.List.PeriodicityLemma

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

Tactic:
intro i

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
i : ℕ
⊢ i < w.length - p → w[i]? = w[i + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u w : List α
p : ℕ
per : w.HasPeriod p
h : u <:+: w
⊢ u.HasPeriod p

Tactic:
obtain ⟨s, t, rfl⟩ := h
  exact per.factor

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
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
⊢ ∀ i < n + w.length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?

Tactic:
intro i

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 : ℕ
⊢ i < n + w.length → (take n w ++ w)[i]? = (take n w ++ w)[i % p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
⊢ ∀ i < w.length - q - k, w[q + i]? = w[q + (i + k)]?

Tactic:
intro i

Goal state after:
α : Type u_1
q k : ℕ
w : List α
per_q : ∀ i < w.length - q, w[i]? = w[i + q]?
per_plus : ∀ i < w.length - (k + q), w[i]? = w[i + (k + q)]?
i : ℕ
⊢ i < w.length - q - k → w[q + i]? = w[q + (i + k)]?
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr.cons
α : 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)
b : α
N : Multiset α
ihN : (∀ (x : α), x ∈ N → x < a) → Acc OneStep (M + N)
hN : ∀ (x : α), x ∈ b ::ₘ N → x < a
⊢ Acc OneStep (M + b ::ₘ N)

Tactic:
simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢

Goal state after:
case intro.intro.inr.cons
α : 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)
b : α
N : Multiset α
ihN : (∀ (x : α), x ∈ N → x < a) → Acc OneStep (M + N)
hN : b < a ∧ ∀ (a_1 : α), a_1 ∈ N → a_1 < a
⊢ Acc OneStep (b ::ₘ (M + N))
Module: Mathlib.Data.NNRat.Floor

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

Tactic:
norm_cast

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

Goal state before:
pp: a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ 0 ≤ ↑a

Tactic:
norm_cast

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

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

Tactic:
norm_cast

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

Goal state before:
pp: a : ℚ≥0
b : ℕ
⊢ (fun q ↦ ⌈↑q⌉₊) a ≤ b ↔ a ≤ ↑b

Tactic:
rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast

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

Goal state before:
pp: case e'_2
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

Tactic:
norm_cast

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

Goal state before:
pp: case e'_3.e'_5.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

Tactic:
norm_cast

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

Goal state before:
pp: case e'_3.e'_5.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

Tactic:
norm_cast

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

Goal state before:
pp: case e'_3.e'_6.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs

Tactic:
norm_cast

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑↑⌊x⌋₊ + 1

Tactic:
norm_cast

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑(⌊x⌋₊ + 1)
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑(⌊x⌋₊ + 1)

Tactic:
norm_cast

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ x ∧ x < ↑(⌊x⌋₊ + 1)
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case e'_2.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑q₁.num = (↑q₁).num

Tactic:
norm_cast

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

Goal state before:
pp: case e'_2.e'_6
q₁ q₂ : ℚ≥0
⊢ ↑q₂.num = (↑q₂).num

Tactic:
norm_cast

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

Goal state before:
pp: case e'_3.e'_5
q₁ q₂ : ℚ≥0
⊢ ↑(q₁ * q₂).num = (↑q₁ * ↑q₂).num

Tactic:
norm_cast

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

Goal state before:
pp: case e'_3.e'_6.e'_3.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum

Tactic:
have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by simp) n

Goal state after:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ ↑p ^ m * ↑((p ^ m).gcdA n) + ↑n * ↑((p ^ m).gcdB n) = 1

Tactic:
norm_cast

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
⊢ ↑(↑(p ^ m) * (p ^ m).gcdA n + ↑n * (p ^ m).gcdB n) = 1
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
⊢ (n.floorRoot a).factorization = a.factorization ⌊/⌋ n

Tactic:
rw [floorRoot_def]

Goal state after:
n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2).factorization = a.factorization ⌊/⌋ n
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 + fib (a - 1) ≤ fib n

Tactic:
rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']

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.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:
norm_cast

Goal state after:
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
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ ¬n.minFac ^ 2 ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
by
  obtain ⟨k, _, k_pos, hn₁⟩ := (isPrimePow_nat_iff_bounded_log_minFac _).mp h
  have isPrime := minFac_prime_iff.mpr (IsPrimePow.ne_one h)
  refine mt Finset.dvd_gcd_iff.mp ?_
  simp only [mem_Icc, not_forall]
  have : n.minFac ^ (k - 1) ≤ n.minFac ^ k := Nat.pow_le_pow_right (minFac_pos n) (sub_le k 1)
  refine ⟨n.minFac ^ (k - 1), ⟨one_le_pow _ _ (minFac_pos n), ?_⟩, ?_⟩
  · refine le_sub_one_of_lt ?_
    nth_rw 2 [hn₁]
    exact Nat.pow_lt_pow_of_lt (Prime.one_lt isPrime) (sub_one_lt_of_lt k_pos)
  · refine emultiplicity_lt_iff_not_dvd.mp ?_
    nth_rw 2 [hn₁]
    rw [Nat.Prime.emultiplicity_choose_prime_pow isPrime this (pow_ne_zero _
      (Nat.Prime.ne_zero isPrime)), multiplicity_pow_self_of_prime (prime_iff.mp isPrime)]
    norm_cast
    grind

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

Goal state before:
pp: case refine_1
p : ℕ → Prop
n : ℕ
h : nth p n = 0
⊢ (∀ (x : (Set.ofPred p).Finite), n < #x.toFinset) → p 0 ∧ n = 0

Tactic:
exact fun hn => ⟨h ▸ nth_mem _ hn, nonpos_iff_eq_zero.1 <| h ▸ le_nth hn⟩

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

Goal state before:
pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
rw [nth_of_card_le _ hk] at h
      exact absurd h (zero_le _).not_gt

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

Goal state before:
pp: case succ.refine_2
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
⊢ f (n + 1) ≤ f m

Tactic:
apply hmono hn hm

Goal state after:
case succ.refine_2
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 + 1 ≤ m
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case h.right.right
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ ∀ (i : P.B a), r (↑(f i)).1 (↑(f i)).2

Tactic:
intro i

Goal state after:
case h.right.right
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
i : P.B a
⊢ r (↑(f i)).1 (↑(f i)).2
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∃ y, f y = x

Tactic:
apply @h fun x => ∃ y : P.B a, f y = x
    rw [liftp_iff']
    intro
    exact ⟨_, rfl⟩

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

Goal state before:
pp: case h.right.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ ∀ (i : Fin2 n) (j : P.B a i), r (↑(f i j)).1 (↑(f i j)).2

Tactic:
intro i

Goal state after:
case h.right.right
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
i : Fin2 n
⊢ ∀ (j : P.B a i), r (↑(f i j)).1 (↑(f i j)).2
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝¹ i) (f✝ i)

Tactic:
intro i

Goal state after:
case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
i : F.B a✝
⊢ Agree' n✝ (f✝¹ i) (f✝ i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr.succ.step.f.f.refl.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
⊢ ∀ (i : F.B a), Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))

Tactic:
intro i

Goal state after:
case mpr.succ.step.f.f.refl.refl
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: 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
⊢ ∀ (i : ℕ), x.approx i = y.approx i

Tactic:
intro i

Goal state after:
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
i : ℕ
⊢ x.approx i = y.approx i
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : m.Sized
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2

Tactic:
by
  cases m
  · simp [node4L, node3L, node']
    abel
  · simp [node4L, node', size, hm.1]; abel

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∀ (i : (P.B ax).last), R (lastFun fx i) (lastFun fy i)

Tactic:
intro i

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
i : (P.B ax).last
⊢ R (lastFun fx i) (lastFun fy i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5

pp: case inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
· rw [r0]; exact Nat.zero_le _

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
⊢ P.WPath (WType.mk a f) ⟹ α

Tactic:
intro i

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{?u.9} n
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
⊢ P.WPath (WType.mk a f) i → α i
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∀ (i : P.B a), ∃ x', True ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Tactic:
intro i

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
i : P.B a
⊢ ∃ x', True ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : 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
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs

Tactic:
· rw [splitMin_eq]
    · obtain ⟨v, e⟩ := Valid'.eraseMin_aux hr
      suffices H : _ by
        refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩
        · refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil
          exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)
        · exact
            @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)
        · rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl
      refine Or.inr ⟨_, Or.inr e, ?_⟩
      rwa [hr.2.eq_node'] at bal

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

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

Tactic:
· rw [hlt₁.antisymm hlt₂]

Goal state after: