mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty

Tactic:
rw [not_iff_comm, ← le_bot_iff, F.le_iff Realizer.bot, not_forall]

Goal state after:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case pos
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
h2 : Even l.length
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
if_pos h2,

Goal state after:
case pos
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
h2 : Even l.length
⊢ 2 * count b l = l.length
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ (⨆ i, f a i) + ∑ a ∈ s, ⨆ i, f a i = ⨆ i, f a i + ∑ a ∈ s, f a i

Tactic:
ihs

Goal state after:
case cons
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ (⨆ i, f a i) + ⨆ i, ∑ a ∈ s, f a i = ⨆ i, f a i + ∑ a ∈ s, f a i
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ emin = max (emin + ↑(Nat.size 0) - ↑prec) emin

Tactic:
(simp [sub_eq_add_neg, Int.natCast_nonneg])

Goal state after:
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin (n + 1)
⊢ f k < x

Tactic:
induction k using Fin.induction with
  | zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
  | succ k ihk =>
    rw [range_subset_iff] at hbt
    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (List.map Prod.toSigma f.graph.toList).keys.Nodup

Tactic:
List.keys,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (List.map Sigma.fst (List.map Prod.toSigma f.graph.toList)).Nodup
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]

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ ↑a.natAbs < ↑b.natAbs
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)

Tactic:
cases m <;> cases n <;> simp only [testBit, bitwise, natBitwise]
  · by_cases h : f false false <;> simp [h]
  · by_cases h : f false true <;> simp [h]
  · by_cases h : f true false <;> simp [h]
  · by_cases h : f true true <;> simp [h]

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

Tactic:
by_cases hp : p hd

Goal state after:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true

case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
hp : ¬p hd = true
⊢ ¬p
        ((match p hd with
            | true => dropWhile p tl
            | false => hd :: tl).get
          ⟨0, hl⟩) =
      true
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
⊢ dropWhile p (hd :: tl) = hd :: tl ↔ ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
rw [dropWhile]
    by_cases h_p_hd : p hd
    · simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]
      intro h
      replace h := congrArg length h
      have := length_dropWhile_le p tl
      simp at h
      lia
    · simp [h_p_hd]

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

Goal state before:
pp: case cons
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
by_cases hp : p hd

Goal state after:
case pos
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : p hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

case neg
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
hp : ¬p hd = true
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rdrop n = (drop n l.reverse).reverse

Tactic:
rdrop

Goal state after:
α : Type u_1
l : List α
n : ℕ
⊢ take (l.length - n) l = (drop n l.reverse).reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
i j : ℕ
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)

Tactic:
by
  simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Nat.cast '' Iic a = Icc 0 ↑a

Tactic:
rw [← Icc_bot, image_cast_int_Icc]; rfl

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

Goal state before:
pp: case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂

Tactic:
simp only [mem_product, mem_range] at hx

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
hx : x₁ < n % p + 1 ∧ x₂ < n / p + 1
⊢ k % p = x₁ ∧ k / p = x₂
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: ⊢ [].IsZeckendorfRep

Tactic:
by simp [IsZeckendorfRep]

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

Goal state before:
pp: case h₁
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / p ^ a / p).choose (k / p ^ a / p)) ≡
    ↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]

Tactic:
Nat.div_div_eq_div_mul,

Goal state after:
case h₁
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) ≡
    ↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
apply (choose_modEq_choose_mul_prod_range_choose a).trans
  simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
    Int.ModEq.refl]

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
· rw [minFac, Nat.minFac_eq, if_pos]
    · rfl
    simp [← two_mul]

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

Goal state before:
pp: n : PosNum
⊢ ↑n.minFac = (↑n).minFac

Tactic:
obtain - | n := n
  · simp [minFac]
  · rw [minFac, Nat.minFac_eq, if_neg]
    swap
    · simp [← two_mul]
    rw [minFacAux_to_nat]
    · rfl
    simp only [cast_one, cast_bit1]
    rw [Nat.sqrt_lt]
    calc
      (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
      _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
      _ < _ := by simp [mul_lt_mul]
  · rw [minFac, Nat.minFac_eq, if_pos]
    · rfl
    simp [← two_mul]

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

Goal state before:
pp: case refine_1
n : PosNum
⊢ 2 ≤ ↑n.bit1

Tactic:
simp only [cast_bit1]
          have := to_nat_pos n
          lia

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn p.pred' 1 bit1) = ↑(neg p) + ↑(neg p) + 1

Tactic:
cast_neg

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑b + -↑a = -↑a + ↑b

Tactic:
← PosNum.cast_to_int a,

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a + ↑b = ↑b + ↑a

Tactic:
← PosNum.cast_to_int a,

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

Goal state before:
pp: case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 + ↑d * (↑q + ↑q) = ↑n.bit0

Tactic:
simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ delta * r.dual.size < l.dual.size

pp: case refine_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3

Tactic:
· rwa [size_dual, size_dual]

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3

Tactic:
· rwa [size_dual, size_dual]

Goal state after:
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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.rotateR x r) o₂

Tactic:
refine Valid'.dual_iff.2 ?_
  rw [dual_rotateR]
  refine hr.dual.rotateL hl.dual ?_ ?_ ?_
  · rwa [size_dual, size_dual, add_comm]
  · rwa [size_dual, size_dual]
  · rwa [size_dual, size_dual]

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

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

Tactic:
exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2

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

Goal state before:
pp: case node.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
hl : (nil.node' lx lr).Balanced
sl : (node ls nil lx lr).Sized
⊢ (nil.node' lx lr).balance x nil = (nil.node' lx lr).balance' x nil

Tactic:
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr

Goal state after:
case node.nil.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
hl : (nil.node' lx nil).Balanced
sl : (node ls nil lx nil).Sized
⊢ (nil.node' lx nil).balance x nil = (nil.node' lx nil).balance' x nil

case node.nil.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ (nil.node' lx (node lrs lrl lrx lrr)).balance x nil = (nil.node' lx (node lrs lrl lrx lrr)).balance' x nil
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
⊢ ((node lls lll llx llr).node' lx lr).balance x nil = ((node lls lll llx llr).node' lx lr).balance' x nil

Tactic:
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr

Goal state after:
case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ ((node lls lll llx llr).node' lx nil).balance x nil = ((node lls lll llx llr).node' lx nil).balance' x nil

case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).balance x nil =
    ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).balance' x nil
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) =
    if 1 + 1 ≤ 1 then ((node 1 nil llx nil).node' lx nil).node' x nil
    else ((node 1 nil llx nil).node' lx nil).rotateR x nil

Tactic:
rw [if_neg, rotateR_node, if_pos]

Goal state after:
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = (node 1 nil llx nil).node3R lx nil x nil

case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ nil.size < ratio * (node 1 nil llx nil).size

case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ ¬1 + 1 ≤ 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
⊢ (u.wp + 1) * (u.ap + 1) + u.x * (u.bp + 1) = u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp + 1

Tactic:
ring_nf

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

Goal state before:
pp: case snd
u : XgcdType
⊢ u.y * (u.ap + 1) + (u.zp + 1) * (u.bp + 1) = u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp + 1

Tactic:
ring_nf

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balanceL rx rr).size = ls + rs

Tactic:
balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂,

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ (t.balance rx rr).size = ls + rs
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case inr.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
hji : j < i
⊢ ⟨i, a⟩ ≤ ⟨j, b⟩ ∨ ⟨j, b⟩ ≤ ⟨i, a⟩

Tactic:
· exact Or.inr (Lex.left _ _ hji)

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

Goal state before:
pp: case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ ↑u.w * ↑u.b + (↑u.w * u.qp + u.x) * ↑u.b = ↑u.w * (↑u.b * u.q) + u.x * ↑u.b

Tactic:
u.qp_eq hr

Goal state after:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ ↑u.w * ↑u.b + (↑u.w * u.qp + u.x) * ↑u.b = ↑u.w * (↑u.b * (u.qp + 1)) + u.x * ↑u.b
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.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * (↑u.b * u.q) + ↑u.z * ↑u.b

Tactic:
u.qp_eq hr

Goal state after:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * (↑u.b * (u.qp + 1)) + ↑u.z * ↑u.b
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
ld : delta ≤ (node lls lll llx llr).size + lr.size
⊢ (node ls (node lls lll llx llr) lx lr).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      (node lls lll llx llr)

Tactic:
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr

Goal state after:
case pos.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
ld : delta ≤ (node lls lll llx llr).size + nil.size
⊢ (node ls (node lls lll llx llr) lx nil).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) nil x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          nil)
      (node lls lll llx llr)

case pos.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
⊢ (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).rotateR x (node rs rl rx rr) =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx
                (node (size_1 + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          (node lrs lrl lrx lrr))
      (node lls lll llx llr)