mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ ∀ ⦃i : Finset ι⦄, i ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id i)

Tactic:
intro f hf

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : f ∈ (map Finsupp.support tl).toFinset
⊢ _root_.Disjoint hd.support (id f)
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.ofNat_lt.symm

Goal state after:
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
by
  rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.ofNat_le.symm

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

Goal state before:
pp: a : ℤ
x✝ : a ∈ Iic 0
b : ℤ
hb : b ∈ Iic 0
hab : a < b
⊢ b.natAbs < a.natAbs

Tactic:
by
  simpa [Int.natAbs_neg] using
    natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)

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

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

Tactic:
ext x
  simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
  aesop

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

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.lor n).testBit k = (m.testBit k || n.testBit k)

Tactic:
by
  rw [← bitwise_or, testBit_bitwise]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
simp [rdropWhile, reverse_eq_iff, getLast_eq_getElem, Nat.pos_iff_ne_zero]

Goal state after:
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:
l.find?_eq_head?_dropWhile_not p,

Goal state after:
α : 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 ⋯)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro
α : 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
⊢ Acc (Shortlex r) (xa :: xb)

Tactic:
refine Acc.intro (xa :: xb) fun p lt => ?_
      rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
      · exact ih _ h1
      · cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          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
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r l a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
by
  induction l generalizing a g with
  | nil =>
    rw [splitBy.loop, reverse_cons, mem_append, mem_reverse, mem_singleton] at h
    obtain hm | rfl := h
    · cases not_mem_nil hm
    · apply List.isChain_reverse.1
      rw [reverse_reverse]
      exact isChain_cons.2 ⟨hga, hg⟩
  | cons b l IH =>
    simp only [splitBy.loop, reverse_cons] at h
    split at h
    · apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
      grind
    · rw [splitByLoop_eq_append, mem_append, reverse_singleton, mem_singleton] at h
      obtain rfl | hm := h
      · apply List.isChain_reverse.1
        rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
        exact isChain_cons.2 ⟨hga, hg⟩
      · grind

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

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

Tactic:
have : p ≤ n := le_of_dvd pos dvd

Goal state after:
α : 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
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this✝ : i % p < p
this : p ≤ n
⊢ i % p < n + w.length
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: m n : ℕ
hm : m ≠ 1
⊢ m.Coprime n ! ↔ n < m.minFac

Tactic:
rw [← not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd]
  constructor
  · intro h
    exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩
  · rintro ⟨p, hp, hdvd, hdvd'⟩
    exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib - 1).pred.succ + fib n.greatestFib

Tactic:
succ_pred,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n < fib (n.greatestFib - 1) + fib n.greatestFib

n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inl
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ a + 2 ≤ (n + 1).greatestFib

pp: case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
· simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
      subst ha
      exact le_greatestFib.2 le_add_self

Goal state after:
case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), p ∣ n.choose b
⊢ p = n.minFac

Tactic:
← modEq_zero_iff_dvd

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD p]
⊢ p = n.minFac
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), q ∣ n.choose b
⊢ IsPrimePow n

Tactic:
← modEq_zero_iff_dvd

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD q]
⊢ IsPrimePow n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ b % pos a ≤ pos a

Tactic:
rw [← le_to_nat, mod_to_nat]

Goal state after:
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ ↑b % ↑(pos a) ≤ ↑(pos a)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz 0 rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 0 ∧ BalancedSz (0 + 0 + 1) rr.size

Tactic:
le_antisymm (balancedSz_zero.1 this.symm) rr0

Goal state after:
case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz 0 rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 0 ∧ BalancedSz (0 + 0 + 1) 1
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
Hr : Relation.EqvGen R x y
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
induction Hr

Goal state after:
case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝

case refine_2.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ : P.M α
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝

case refine_2.symm
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : Relation.EqvGen R x✝ y✝
a_ih✝ :
  (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝

case refine_2.trans
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ z✝ : P.M α
a✝¹ : Relation.EqvGen R x✝ y✝
a✝ : Relation.EqvGen R y✝ z✝
a_ih✝¹ :
  (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝
a_ih✝ :
  (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P z✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P z✝
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : 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', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceL x r) o₂

Tactic:
by
  rw [balanceL_eq_balance' hl.3 hr.3 hl.2 hr.2 H]
  refine hl.balance' hr ?_
  rcases H with (⟨l', e, H⟩ | ⟨r', e, H⟩)
  · exact ⟨_, _, H, Or.inl ⟨e.dist_le', rfl⟩⟩
  · exact ⟨_, _, H, Or.inr ⟨e.dist_le, rfl⟩⟩

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

Goal state before:
pp: case succ
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
⊢ u.prod ^ n * u.prod = u.prod ^ (n + 1)

Tactic:
pow_succ

Goal state after:
case succ
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
⊢ u.prod ^ n * u.prod = u.prod ^ n * u.prod
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
by
  rw [← Nat.card_Ioo, ← map_subtype_embedding_Ioo, card_map]

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

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [balanceL_eq_balance' hl hr sl sr H, all_balance']

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 α
x : α
t : Ordnode α
h : t.Valid
⊢ (insert' x t).Valid

Tactic:
insert'_eq_insertWith

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ IsUniform

Tactic:
by
  constructor
  · intro h α a a' f f' h' i
    rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]
  · rintro h α ⟨a, f⟩
    ext
    rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]

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

Goal state before:
pp: case node.eq.right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_glue_valid : Valid' a₁ (t_l.glue t_r) a₂
h_glue_sized : (t_l.glue t_r).size = t_l.size + t_r.size
⊢ t_l.size + t_r.size + 1 =
    (match Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size +
      1

Tactic:
rw [h_glue_sized]

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

Goal state before:
pp: case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Subtype.val <$> abs ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = x

Tactic:
rw [← abs_map, ← h₀]

Goal state after:
case h
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : abs ⟨a, f⟩ = x
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hn]
    simp

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ supp x = {u | ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ}

Tactic:
ext
  apply mem_supp

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

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
liftp_iff,

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp x, p u
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
c : Computation (WSeq α)
⊢ (flatten c).destruct = c >>= destruct

Tactic:
refine
    Computation.eq_of_bisim
      (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct) ?_
      (Or.inr ⟨c, rfl, rfl⟩)
  intro c1 c2 h
  exact
    match c1, c2, h with
    | c, _, Or.inl rfl => by cases c.destruct <;> simp
    | _, _, Or.inr ⟨c, rfl, rfl⟩ => by
      induction c using Computation.recOn with
      | pure a => simp; cases (destruct a).destruct <;> simp
      | think c' => simpa using Or.inr ⟨c', rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
⊢ S.destruct = some (o, S.tail)

Tactic:
dsimp [Seq.destruct]

Goal state after:
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
⊢ Option.map (fun a' ↦ (a', S.tail)) (S.get? 0) = some (o, S.tail)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
⊢ ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
intro S T ST a ra

Goal state after:
case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : S.join.destruct.Results a n
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b
Module: Mathlib.Data.String.Basic

Goal state before:
pp: s₁ s₂ : String
⊢ s₁ < s₂ ↔ ltb (Legacy.iter s₁) (Legacy.iter s₂) = true

Tactic:
rw [Iff.comm]
  obtain ⟨s₁, rfl⟩ := s₁.exists_eq_ofList
  obtain ⟨s₂, rfl⟩ := s₂.exists_eq_ofList
  simp only [lt_iff_toList_lt, String.Legacy.iter, String.Legacy.mkIterator, String.toList_ofList]
  induction s₁ generalizing s₂ <;> cases s₂
  · unfold ltb; decide
  · rename_i c₂ cs₂; apply iff_of_true
    · unfold ltb
      simp [Legacy.Iterator.hasNext, Char.utf8Size_pos]
    · apply List.nil_lt_cons
  · rename_i c₁ cs₁ ih; apply iff_of_false
    · unfold ltb
      simp [Legacy.Iterator.hasNext]
    · apply not_lt_of_gt; apply List.nil_lt_cons
  · rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb
    simp only [Legacy.Iterator.hasNext, Pos.Raw.byteIdx_zero, rawEndPos_ofList, utf8Len_cons,
      add_pos_iff, Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Legacy.Iterator.curr,
      Pos.Raw.get, String.toList_ofList, Pos.Raw.utf8GetAux, Legacy.Iterator.next, Pos.Raw.next,
      Bool.ite_eq_true_distrib, decide_eq_true_eq]
    split_ifs with h
    · subst c₂
      suffices ltb ⟨ofList (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩
          ⟨ofList (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ =
            ltb ⟨ofList cs₁, 0⟩ ⟨ofList cs₂, 0⟩ by
        rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
      apply ltb_cons_addChar
    · refine ⟨List.Lex.rel, fun e ↦ ?_⟩
      cases e <;> rename_i h'
      · assumption
      · contradiction

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.cons
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (cons s T).join.destruct.destruct (cons s T).join.destruct.destruct

Tactic:
simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case snoc
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧
    (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2

Tactic:
next xs x ih =>
    rcases (hR x h₀) with ⟨hR, _⟩
    simp only [mapAccumr_snoc, ih hR, true_and]
    congr 1

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ ⇑(f ^ (n + 1)) = (⇑f)^[n + 1]

Tactic:
simp [coe_pow n, pow_succ]

Goal state after: