mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: 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

pp: 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

pp: 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

pp: 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

Tactic:
<;>

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

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.PNat.Xgcd

Goal state before:
pp: case fst
u : XgcdType
⊢ u.v.1 = (succ₂ u.vp).1

pp: case snd
u : XgcdType
⊢ u.v.2 = (succ₂ u.vp).2

Tactic:
<;>

Goal state after:
case fst
u : XgcdType
⊢ u.v.1 = (succ₂ u.vp).1

case snd
u : XgcdType
⊢ u.v.2 = (succ₂ u.vp).2
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

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:
<;>

Goal state after:
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

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
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hab : ⟨a₂✝, a⟩ < ⟨a₁✝, i⟩
⊢ False

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

Tactic:
<;>

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hab : ⟨a₂✝, a⟩ < ⟨a₁✝, i⟩
⊢ False

case refine_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : ⟨i, b₂✝⟩ < ⟨i, b₁✝⟩
⊢ False
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y

Tactic:
<;>

Goal state after:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y

Tactic:
<;>

Goal state after:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ ⟨wp + 1, ⋯⟩ * ⟨zp + 1, ⋯⟩ = ⟨x * y + 1, ⋯⟩

pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : ⟨wp + 1, ⋯⟩ * ⟨zp + 1, ⋯⟩ = ⟨x * y + 1, ⋯⟩
⊢ wp + zp + wp * zp = x * y

Tactic:
<;>

Goal state after:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ ⟨wp + 1, ⋯⟩ * ⟨zp + 1, ⋯⟩ = ⟨x * y + 1, ⋯⟩

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : ⟨wp + 1, ⋯⟩ * ⟨zp + 1, ⋯⟩ = ⟨x * y + 1, ⋯⟩
⊢ wp + zp + wp * zp = x * y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp + zp + wp * zp = x * y

Tactic:
simp only [Nat.mul_add, Nat.add_mul, one_mul, mul_one, ← Nat.add_assoc,
      Nat.add_right_cancel_iff] at h
    rw [← h]; ring

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

Goal state before:
pp: case mp
u : XgcdType
⊢ u.bp = u.ap → u.ap = u.bp

pp: case mpr
u : XgcdType
⊢ u.ap = u.bp → u.bp = u.ap

Tactic:
<;>

Goal state after:
case mp
u : XgcdType
⊢ u.bp = u.ap → u.ap = u.bp

case mpr
u : XgcdType
⊢ u.ap = u.bp → u.bp = u.ap
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp

pp: case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap

Tactic:
<;>

Goal state after:
case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp

case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap
Module: Mathlib.Data.PNat.Xgcd

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

Tactic:
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b

Goal state after:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b
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 : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioo a b) = ∏ i, #(Icc (a i) (b i)) - 2

Tactic:
by
  rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

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

Goal state before:
pp: case h.right.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
u : F 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 F).A
f : (P F).B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
rw [← yeq, ← abs_repr u, h, ← abs_map]; rfl

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

Goal state before:
pp: case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
h✝ : delta * rs < ls
⊢ 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) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2 (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      ll =
    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) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2 (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      ll

pp: case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
h✝ : ¬delta * rs < ls
⊢ node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
h✝ : delta * rs < ls
⊢ 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) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2 (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      ll =
    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) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2 (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      ll

case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
h✝ : ¬delta * rs < ls
⊢ node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case right.right.right.left
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
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(z * a') = ↑(x * ↑b').succPNat

Tactic:
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']

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

Goal state before:
pp: case bot
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
h : nil.Bounded ⊥ o₂
⊢ nil.dual.Bounded o₂ ⊥

pp: case coe
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
a✝ : α
h : nil.Bounded (↑a✝) o₂
⊢ nil.dual.Bounded o₂ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
h : nil.Bounded ⊥ o₂
⊢ nil.dual.Bounded o₂ ⊥

case coe
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
a✝ : α
h : nil.Bounded (↑a✝) o₂
⊢ nil.dual.Bounded o₂ ↑a✝
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : Preorder α
h : nil.Bounded ⊥ ⊤
⊢ nil.dual.Bounded ⊤ ⊥

pp: case bot.coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
h : nil.Bounded ⊥ ↑a✝
⊢ nil.dual.Bounded ↑a✝ ⊥

pp: case coe.top
α : Type u_1
inst✝ : Preorder α
a✝ : α
h : nil.Bounded ↑a✝ ⊤
⊢ nil.dual.Bounded ⊤ ↑a✝

pp: case coe.coe
α : Type u_1
inst✝ : Preorder α
a✝¹ a✝ : α
h : nil.Bounded ↑a✝¹ ↑a✝
⊢ nil.dual.Bounded ↑a✝ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.top
α : Type u_1
inst✝ : Preorder α
h : nil.Bounded ⊥ ⊤
⊢ nil.dual.Bounded ⊤ ⊥

case bot.coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
h : nil.Bounded ⊥ ↑a✝
⊢ nil.dual.Bounded ↑a✝ ⊥

case coe.top
α : Type u_1
inst✝ : Preorder α
a✝ : α
h : nil.Bounded ↑a✝ ⊤
⊢ nil.dual.Bounded ⊤ ↑a✝

case coe.coe
α : Type u_1
inst✝ : Preorder α
a✝¹ a✝ : α
h : nil.Bounded ↑a✝¹ ↑a✝
⊢ nil.dual.Bounded ↑a✝ ↑a✝¹
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
h : nil.Bounded o₁ ⊤
⊢ nil.Bounded ⊥ ⊤

pp: case coe
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
a✝ : α
h : nil.Bounded o₁ ↑a✝
⊢ nil.Bounded ⊥ ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
h : nil.Bounded o₁ ⊤
⊢ nil.Bounded ⊥ ⊤

case coe
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
a✝ : α
h : nil.Bounded o₁ ↑a✝
⊢ nil.Bounded ⊥ ↑a✝
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case bot
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
h : nil.Bounded ⊥ o₂
⊢ nil.Bounded ⊥ ⊤

pp: case coe
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
a✝ : α
h : nil.Bounded (↑a✝) o₂
⊢ nil.Bounded ↑a✝ ⊤

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
h : nil.Bounded ⊥ o₂
⊢ nil.Bounded ⊥ ⊤

case coe
α : Type u_1
inst✝ : Preorder α
o₂ : WithTop α
a✝ : α
h : nil.Bounded (↑a✝) o₂
⊢ nil.Bounded ↑a✝ ⊤
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.lt with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.lt with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

pp: case eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.eq with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.eq with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

pp: case gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.gt with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.gt with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

Tactic:
<;>

Goal state after:
case lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.lt with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.lt with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

case eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.eq with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.eq with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)

case gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match Ordering.gt with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match Ordering.gt with
    | Ordering.lt => (insertWith (fun x_1 ↦ x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 ↦ x) x r)