awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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)))
⊢ 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)))
have 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)))
Tactic: split_ifs with h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size
have hs : (node sz l y r).Sized
Tactic: rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size
have hb : (node sz l y r).Balanced
Tactic: rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size
have lx : l.Bounded o₁ (↑y : WithTop α)
Tactic: rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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 α)
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size
have xr : r.Bounded (↑y : WithBot α) o₂
Tactic: rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₂
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size
have xf : x ≤ f y
Tactic: rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ Valid' o₁ (node sz l (f y) r) o₂ ∧ Raised (node sz l y r).size (node sz l (f y) r).size
have fx : f y ≤ x
Tactic: rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size
have vl : 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⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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 α)
⊢ 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
have e : 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⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
have refine : Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size
Tactic: refine ⟨vl.balanceL h.right H, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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 (node sz l y r).size ((insertWith f x l).balanceL y r).size
have rw : Raised (l.size + r.size + 1) ((insertWith f x l).size + r.size + 1)
Tactic: rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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
have 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'
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 _
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ 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
have this : y < x
Tactic: have : y < x := lt_of_le_not_ge ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size
have vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
Tactic: rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₂
⊢ 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
have e : Raised r.size (insertWith f x r).size
Tactic: rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
have refine : Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size
Tactic: refine ⟨h.left.balanceR vr H, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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 (node sz l y r).size (l.balanceR y (insertWith f x r)).size
have rw : Raised (l.size + r.size + 1) (l.size + (insertWith f x r).size + 1)
Tactic: rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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
have 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'
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 _
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Ordnode.insert x (node size l y r) = insertWith (fun (x_1 : α) ↦ x) x (node size l y r)
have unfold : Eq.{u_1 + 1} (α := Ordnode α)
  (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
    Ordnode α)
  (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
    Ordnode α)
Tactic: unfold Ordnode.insert insertWith
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
      Ordnode α)
have lt : Eq.{u_1 + 1} (α := Ordnode α)
  (match (motive := Ordering → Ordnode α) 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) :
    Ordnode α)
  (match (motive := Ordering → Ordnode α) 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) :
    Ordnode α)
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) 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) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) 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) :
      Ordnode α)
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
      Ordnode α)
have eq : Eq.{u_1 + 1} (α := Ordnode α)
  (match (motive := Ordering → Ordnode α) 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) :
    Ordnode α)
  (match (motive := Ordering → Ordnode α) 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) :
    Ordnode α)
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) 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) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) 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) :
      Ordnode α)
eq :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) 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) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) 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) :
      Ordnode α)
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y 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) :
      Ordnode α)
have gt : Eq.{u_1 + 1} (α := Ordnode α)
  (match (motive := Ordering → Ordnode α) 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) :
    Ordnode α)
  (match (motive := Ordering → Ordnode α) 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) :
    Ordnode α)
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (Ordnode.insert x t).Valid
have rw : (insertWith (fun (x_1 : α) ↦ x) x t).Valid
Tactic: rw [insert_eq_insertWith]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ insert' x (node size l y r) = insertWith id x (node size l y r)
have unfold : Eq.{u_1 + 1} (α := Ordnode α)
  (match (motive := Ordering → Ordnode α) cmpLE x y with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size l y r
    | Ordering.gt => l.balanceR y (insert' x r) :
    Ordnode α)
  (match (motive := Ordering → Ordnode α) cmpLE x y with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r) :
    Ordnode α)
Tactic: unfold insert' insertWith
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)
have lt : Eq.{u_1 + 1} (α := Ordnode α)
  (match (motive := Ordering → Ordnode α) Ordering.lt with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size l y r
    | Ordering.gt => l.balanceR y (insert' x r) :
    Ordnode α)
  (match (motive := Ordering → Ordnode α) Ordering.lt with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r) :
    Ordnode α)
Tactic: cases cmpLE x y