mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((update g i (insert x (g i)) i).erase x)
hx' : x ∉ g i
⊢ p (update g i (insert x (g i)))

Tactic:
update_self,

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((insert x (g i)).erase x)
hx' : x ∉ g i
⊢ p (update g i (insert x (g i)))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ 1 + 2 * -[n.div2+1] = -[0 + 2 * n.div2+1]

Tactic:
change -[2 * Nat.div2 n+1] = _
      rw [zero_add]

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

Goal state before:
pp: ⊢ (bitwise fun a b ↦ a && !b) = ldiff

Tactic:
funext m n
  rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false,
      cond_false, cond_true, Nat.ldiff, Bool.and_true, negSucc.injEq,
      Bool.and_false, Bool.not_true, ldiff]
  · congr
    simp
  · congr
    simp
  · rw [Nat.bitwise_swap, Function.swap]
    congr
    funext x y
    cases x <;> cases y <;> rfl

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

Goal state before:
pp: case ofNat
n a✝ : ℕ
⊢ (match ofNat a✝, ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    (ofNat a✝).mul ↑(Nat.pow 2 n)

Tactic:
simp only [Nat.shiftLeft'_false, natCast_shiftLeft, ofNat_eq_natCast,
    Nat.pow_eq, Int.natCast_pow, Nat.cast_ofNat, mul_def]

Goal state after:
case ofNat
n a✝ : ℕ
⊢ ↑a✝ <<< n = ↑a✝ * 2 ^ n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc
n a✝ : ℕ
⊢ (match -[a✝+1], ↑n with
    | ofNat m, ofNat n => ↑(Nat.shiftLeft' false m n)
    | ofNat m, -[n+1] => ↑(m.shiftRight n.succ)
    | -[m+1], ofNat n => -[Nat.shiftLeft' true m n+1]
    | -[m+1], -[n+1] => -[m.shiftRight n.succ+1]) =
    -[a✝+1].mul ↑(Nat.pow 2 n)

Tactic:
simp only [Nat.shiftLeft'_false, natCast_shiftLeft, ofNat_eq_natCast,
    Nat.pow_eq, Int.natCast_pow, Nat.cast_ofNat, mul_def]

Goal state after:
case negSucc
n a✝ : ℕ
⊢ -[Nat.shiftLeft' true a✝ n+1] = -[a✝+1] * 2 ^ n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n

Tactic:
by
          rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]; apply Nat.le_add_right

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

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ 0 < ↑(b % r - v % r) ∧ ↑(b % r - v % r) ≤ 1 * ↑r

Tactic:
cast_pos,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ 0 < b % r - v % r ∧ ↑(b % r - v % r) ≤ 1 * ↑r
Module: Mathlib.Data.List.TakeWhile

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

Tactic:
← head_eq_iff_head?_eq_some

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

α : Type u_1
p : α → Bool
l : List α
h : ∃ x, x ∈ l ∧ p x = true
⊢ dropWhile (fun x ↦ !p x) l ≠ []
Module: Mathlib.Data.List.Intervals

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

pp: case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
· rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
      filter_le_of_le_bot (le_refl l), nil_append]

Goal state after:
case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m
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 : ℕ
less : i < w.length - p
⊢ w[i]? = w[i + p]?

Tactic:
rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]

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

Goal state before:
pp: case neg
α : 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 : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
calc
        (take n w ++ w)[j]? = w[j - (take n w).length]? := getElem?_append_right (by simp_all)
        _ = w[j - n]? := by simp_all
        _ = w[(j - n) % p]? := Eq.symm (mod_w (j - n) (by lia))
        _ = w[j % p]? := by rw [j_mod]

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

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
rw [← ofDigits_one]

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
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:
split_ifs <;> simp [*]

Goal state after:
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:
split_ifs <;> simp [*]

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

Goal state before:
pp: case refine_2
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ emultiplicity n.minFac ((n.minFac ^ k).choose (n.minFac ^ (k - 1))) < ↑2

Tactic:
Nat.Prime.emultiplicity_choose_prime_pow isPrime this (pow_ne_zero _
      (Nat.Prime.ne_zero isPrime)),

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 - multiplicity n.minFac (n.minFac ^ (k - 1))) < ↑2
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

Tactic:
rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_getElem, Fin.getElem_fin]

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
x : ℕ
h : p x
⊢ ∃ n < #hf.toFinset, nth p n = x

Tactic:
← @Set.mem_ofPred_eq _ _ p,

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
x : ℕ
h : x ∈ {y | p y}
⊢ ∃ n < #hf.toFinset, nth p n = x
Module: Mathlib.Data.Nat.Nth

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

Tactic:
← @Set.mem_ofPred_eq _ _ p,

Goal state after:
case refine_2
p : ℕ → Prop
x : ℕ
h : x ∈ {y | p y}
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x
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
⊢ sInf {x | p x ∧ ∀ k < n, nth p k < x} ≤ f n

Tactic:
refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩

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
⊢ nth p k < f n
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n k : PosNum
h : (↑n).sqrt < 0 + ↑k.bit1
⊢ ↑n = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
Nat.zero_add,

Goal state after:
n k : PosNum
h : (↑n).sqrt < ↑k.bit1
⊢ ↑n = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Ordmap.Ordnode

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

pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
· 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)

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(pos p) = ↑(pos p)

Tactic:
cast_pos,

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑p = ↑(pos p)

Tactic:
cast_pos,

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

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

Tactic:
cast_pos,

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

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

Tactic:
cast_pos,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑(pos p) + ↑(pos p) + 1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
p : ↑P P.W
⊢ (mk p).dest = p

Tactic:
cases p

Goal state after:
case mk
P : PFunctor.{uA, uB}
fst✝ : P.A
snd✝ : P.B fst✝ → P.W
⊢ (mk ⟨fst✝, snd✝⟩).dest = ⟨fst✝, snd✝⟩
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
p : P.W
⊢ mk p.dest = p

Tactic:
cases p

Goal state after:
case mk
P : PFunctor.{uA, uB}
a✝ : P.A
f✝ : P.B a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ neg p + 1 = (neg p).succ

Tactic:
cases p

Goal state after:
case one
⊢ neg one + 1 = (neg one).succ

case bit1
a✝ : PosNum
⊢ neg a✝.bit1 + 1 = (neg a✝.bit1).succ

case bit0
a✝ : PosNum
⊢ neg a✝.bit0 + 1 = (neg a✝.bit0).succ
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : ZNum
⊢ ↑(b + 0) = ↑b + ↑0

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

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

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(pos a) = pos a

Tactic:
cast_pos,

Goal state after:
a : PosNum
⊢ ofInt' ↑a = pos a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) * 2 ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))

Tactic:
mul_two,

Goal state after:
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑b % ↑(pos a)) ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑↑(Num.pos n % d.abs) = ↑(pos n) % ↑d

Tactic:
cast_pos,

Goal state after:
n : PosNum
d : ZNum
⊢ ↑↑(Num.pos n % d.abs) = ↑n % ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩)).head = (isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)).head ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
simp only [h, h', isubtree_cons] at ps_ih ⊢

Goal state after:
case f.f.cons.f.f
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk ⟨a₀, f₀⟩
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk ⟨a₁, f₁⟩
⊢ (isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₁, f₁⟩)).head ∧
    ∃ a f f',
      isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧
        isubtree ps (M.mk ⟨a₁, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝ : l.size + r.size ≤ 1
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

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

Goal state before:
pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

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

Goal state before:
pp: case pos
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

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

Goal state before:
pp: case neg
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ All P (l.node' x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_node', all_rotateL, all_rotateR]

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:
splitMax',

Goal state after:
α : Type u_1
x✝ : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ (match ll.splitMax' lx lr with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x✝ l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h

Tactic:
ext i x; cases x <;> rfl

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
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) ⟹ α
⊢ h ⊚ P.wPathCasesOn g' g = P.wPathCasesOn (h ⊚ g') fun i ↦ h ⊚ g i

Tactic:
ext i x; cases x <;> rfl

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

Goal state before:
pp: case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.2 = u.v.2

Tactic:
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b
    rw [← ha, u.qp_eq hr]
    ring

Goal state after:
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ (∀ (a_1 : ι), x a_1 ∈ Ici (a a_1)) ↔ a ≤ x

Tactic:
mem_Ici,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a✝ a x : (i : ι) → α i
⊢ (∀ (a_1 : ι), a a_1 ≤ x a_1) ↔ a ≤ x
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
⊢ let b' := a.gcdB' b;
  w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
b'

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
⊢ w * z = (x * y).succPNat ∧
    a = a' * d ∧
      b = b' * d ∧
        z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
have hza' : (z * a' : ℕ) = x * b' + 1 := by
    rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
    ring

Goal state after:
case right.right.right
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
⊢ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) ll → Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) lr → Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rl o₂ →
        All (fun x ↦ All (fun y ↦ x < y) rl) (Ordnode.node ls ll lx lr) →
          Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
            ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih✝ :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rr o₂ →
        All (fun x ↦ All (fun y ↦ x < y) rr) (Ordnode.node ls ll lx lr) →
          Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
            ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
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)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
v : Valid' (↑lx) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
this :
  (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + rs →
    Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
      (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))).size = ls + rs
⊢ Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
    (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size

Tactic:
exact this e

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
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 : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv ((P F).wMk a₁ f'₁ f₁) ((P F).wMk a₀ f'₀ f₀)

Tactic:
| abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
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 : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv (g <$$> (P F).wMk a₀ f'₀ f₀) (g <$$> (P F).wMk a₁ f'₁ f₁)

Tactic:
| abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>

Goal state after: