awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
rw :
  Valid' o₁
      (match (motive := Ordering → Ordnode α)
        if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α)
          if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)))
⊢ Valid' o₁ (insertWith f x (node sz l y r)) o₂ ∧ Raised (node sz l y r).size (insertWith f x (node sz l y r)).size

Tactic:
rw [insertWith, cmpLE]

Premises used: Ordnode.insertWith, cmpLE
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
pos :
  ∀ (h_1 : x ≤ y) (h_2 : y ≤ x),
    Valid' o₁
        (match (motive := Ordering → Ordnode α) Ordering.eq with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r))
        o₂ ∧
      Raised (node sz l y r).size
        (size.{u_1} (α := α)
          (match (motive := Ordering → Ordnode α) Ordering.eq with
          | Ordering.lt => (insertWith f x l).balanceL y r
          | Ordering.eq => node sz l (f y) r
          | Ordering.gt => l.balanceR y (insertWith f x r)))
neg :
  ∀ (h_1 : x ≤ y) (h_2 : ¬y ≤ x),
    Valid' o₁
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r))
        o₂ ∧
      Raised (node sz l y r).size
        (size.{u_1} (α := α)
          (match (motive := Ordering → Ordnode α) Ordering.lt with
          | Ordering.lt => (insertWith f x l).balanceL y r
          | Ordering.eq => node sz l (f y) r
          | Ordering.gt => l.balanceR y (insertWith f x r)))
neg₁ :
  ∀ (h_1 : ¬x ≤ y),
    Valid' o₁
        (match (motive := Ordering → Ordnode α) Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r))
        o₂ ∧
      Raised (node sz l y r).size
        (size.{u_1} (α := α)
          (match (motive := Ordering → Ordnode α) Ordering.gt with
          | Ordering.lt => (insertWith f x l).balanceL y r
          | Ordering.eq => node sz l (f y) r
          | Ordering.gt => l.balanceR y (insertWith f x r)))
⊢ Valid' o₁
      (match (motive := Ordering → Ordnode α)
        if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α)
          if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)))

Tactic:
split_ifs with h_1 h_2
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
⊢ (node sz l y r).Sized

Tactic:
rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
⊢ (node sz l y r).Balanced

Tactic:
rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
⊢ l.Bounded o₁ (↑y : WithTop α)

Tactic:
rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
lx : l.Bounded o₁ (↑y : WithTop α)
⊢ r.Bounded (↑y : WithBot α) o₂

Tactic:
rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
lx : l.Bounded o₁ (↑y : WithTop α)
xr : r.Bounded (↑y : WithBot α) o₂
⊢ x ≤ f y

Tactic:
rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩

Premises used: And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
lx : l.Bounded o₁ (↑y : WithTop α)
xr : r.Bounded (↑y : WithBot α) o₂
xf : x ≤ f y
⊢ f y ≤ x

Tactic:
rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩

Premises used: And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
lx : l.Bounded o₁ (↑y : WithTop α)
xr : r.Bounded (↑y : WithBot α) o₂
xf : x ≤ f y
fx : f y ≤ x
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size

Tactic:
⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩

Premises used: Ordnode.Bounded.mono_right, And.intro, Ordnode.Bounded.mono_left, Or.inl, rfl, Ordnode.Valid'.mk, le_trans
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : y ≤ x
hs : (node sz l y r).Sized
hb : (node sz l y r).Balanced
lx : l.Bounded o₁ (↑y : WithTop α)
xr : r.Bounded (↑y : WithBot α) o₂
xf : x ≤ f y
fx : f y ≤ x
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size

Tactic:
refine
        ⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
⊢ Valid' o₁ (insertWith f x l) (↑y : WithTop α)

Tactic:
rcases insertWith.valid_aux f x hf h.left bl (lt_of_le_not_ge h_1 h_2) with ⟨vl, e⟩

Premises used: lt_of_le_not_ge, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
⊢ Raised l.size (insertWith f x l).size

Tactic:
rcases insertWith.valid_aux f x hf h.left bl (lt_of_le_not_ge h_1 h_2) with ⟨vl, e⟩

Premises used: lt_of_le_not_ge, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
H :
  (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
⟨vl.balanceL h.right H, ?_⟩

Premises used: Ordnode.Valid'.balanceL, Ordnode.Valid'.right, And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
H :
  (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
refine : Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
refine ⟨vl.balanceL h.right H, ?_⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
H :
  (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
rw : Raised (l.size + r.size + 1) ((insertWith f x l).size + r.size + 1)
⊢ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]

Premises used: Ordnode.Valid'.bal, Ordnode.size_balanceL, Ordnode.Valid'.sz, And.right, Ordnode.Sized.size_eq
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
H :
  (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Raised (l.size + r.size + 1) ((insertWith f x l).size + r.size + 1)

Tactic:
(e.add_right _).add_right _

Premises used: Ordnode.Raised.add_right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
H :
  (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Raised (l.size + r.size + 1) ((insertWith f x l).size + r.size + 1)

Tactic:
exact (e.add_right _).add_right _

Premises used: Ordnode.Raised.add_right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
neg :
  (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
suffices H : _ by
        refine ⟨vl.balanceL h.right H, ?_⟩
        rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
        exact (e.add_right _).add_right _
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
⊢ (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'

Tactic:
Or.inl ⟨_, e, h.3.1⟩

Premises used: Ordnode.Valid'.bal, And.left, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) (↑y : WithTop α)
e : Raised l.size (insertWith f x l).size
⊢ (∃ (l' : ℕ), Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'

Tactic:
exact Or.inl ⟨_, e, h.3.1⟩

Premises used: Or.inl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
⊢ y < x

Tactic:
have : y < x := lt_of_le_not_ge ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
⊢ Valid' (↑y : WithBot α) (insertWith f x r) o₂

Tactic:
rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩

Premises used: Ordnode.Valid'.right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
⊢ Raised r.size (insertWith f x r).size

Tactic:
rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩

Premises used: Ordnode.Valid'.right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
⟨h.left.balanceR vr H, ?_⟩

Premises used: And.intro, Ordnode.Valid'.balanceR, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
refine : Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
refine ⟨h.left.balanceR vr H, ?_⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
rw : Raised (l.size + r.size + 1) (l.size + (insertWith f x r).size + 1)
⊢ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.size_balanceR, And.right, And.left, Ordnode.Sized.size_eq
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Raised (l.size + r.size + 1) (l.size + (insertWith f x r).size + 1)

Tactic:
(e.add_left _).add_right _

Premises used: Ordnode.Raised.add_right, Ordnode.Raised.add_left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
H :
  (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Raised (l.size + r.size + 1) (l.size + (insertWith f x r).size + 1)

Tactic:
exact (e.add_left _).add_right _

Premises used: Ordnode.Raised.add_right, Ordnode.Raised.add_left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
neg :
  (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
suffices H : _ by
        refine ⟨h.left.balanceR vr H, ?_⟩
        rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
        exact (e.add_left _).add_right _