awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : All P (l.balance' x r) ↔ All P l ∧ P x ∧ All P r
⊢ All P (l.balanceR x r) ↔ All P l ∧ P x ∧ All P r
have rw₁ : All P l ∧ P x ∧ All P r ↔ All P l ∧ P x ∧ All P r
Tactic: rw [balanceR_eq_balance' hl hr sl sr H, all_balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
⊢ Bounded (Ordnode.dual nil) o₂ o₁
have bot : ∀ (h : Bounded nil ⊥ o₂), Bounded (Ordnode.dual nil) o₂ ⊥
Tactic: cases o₁
Cleared hypotheses: o₁, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
bot : ∀ (h : Bounded nil ⊥ o₂), Bounded (Ordnode.dual nil) o₂ ⊥
⊢ Bounded (Ordnode.dual nil) o₂ o₁
have coe : ∀ (a : α) (h : Bounded nil (↑a : WithBot α) o₂), Bounded (Ordnode.dual nil) o₂ (↑a : WithBot α)
Tactic: cases o₁
Cleared hypotheses: o₁, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
h : Bounded nil ⊥ o₂
⊢ Bounded (Ordnode.dual nil) o₂ ⊥
have bot : ∀ (h : Bounded.{u_1} (α := α) nil ⊥ ⊤), Bounded.{u_1} (α := αᵒᵈ) (Ordnode.dual nil) ⊤ ⊥
Tactic: cases o₂
Cleared hypotheses: o₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
h : Bounded nil ⊥ o₂
bot : ∀ (h : Bounded.{u_1} (α := α) nil ⊥ ⊤), Bounded.{u_1} (α := αᵒᵈ) (Ordnode.dual nil) ⊤ ⊥
⊢ Bounded (Ordnode.dual nil) o₂ ⊥
have bot₁ : ∀ (a : α) (h : Bounded nil ⊥ (↑a : WithTop α)), Bounded (Ordnode.dual nil) (↑a : WithTop α) ⊥
Tactic: cases o₂
Cleared hypotheses: o₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
a : α
h : Bounded nil (↑a : WithBot α) o₂
⊢ Bounded (Ordnode.dual nil) o₂ (↑a : WithBot α)
have coe : ∀ (h : Bounded nil (↑a : WithBot α) ⊤), Bounded (Ordnode.dual nil) ⊤ (↑a : WithBot α)
Tactic: cases o₂
Cleared hypotheses: o₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
a : α
h : Bounded nil (↑a : WithBot α) o₂
coe : ∀ (h : Bounded nil (↑a : WithBot α) ⊤), Bounded (Ordnode.dual nil) ⊤ (↑a : WithBot α)
⊢ Bounded (Ordnode.dual nil) o₂ (↑a : WithBot α)
have coe₁ : ∀ (a_1 : α) (h : Bounded nil (↑a : WithBot α) (↑a_1 : WithTop α)),
  Bounded (Ordnode.dual nil) (↑a_1 : WithTop α) (↑a : WithBot α)
Tactic: cases o₂
Cleared hypotheses: o₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
⊢ t.Bounded o₁ o₂
have this : t.dual.dual.Bounded o₁ o₂
Tactic: have := Bounded.dual h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂
have rwa : ∀ (this : t.Bounded o₁ o₂), t.Bounded o₁ o₂
Tactic: rwa [dual_dual, OrderDual.Preorder.dual_dual] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
⊢ Bounded nil ⊥ o₂
have top : ∀ (h : Bounded nil o₁ ⊤), Bounded.{u_1} (α := α) nil ⊥ ⊤
Tactic: cases o₂
Cleared hypotheses: o₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
top : ∀ (h : Bounded nil o₁ ⊤), Bounded.{u_1} (α := α) nil ⊥ ⊤
⊢ Bounded nil ⊥ o₂
have coe : ∀ (a : α) (h : Bounded nil o₁ (↑a : WithTop α)), Bounded nil ⊥ (↑a : WithTop α)
Tactic: cases o₂
Cleared hypotheses: o₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
⊢ Bounded nil o₁ ⊤
have bot : ∀ (h : Bounded nil ⊥ o₂), Bounded.{u_1} (α := α) nil ⊥ ⊤
Tactic: cases o₁
Cleared hypotheses: o₁, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
bot : ∀ (h : Bounded nil ⊥ o₂), Bounded.{u_1} (α := α) nil ⊥ ⊤
⊢ Bounded nil o₁ ⊤
have coe : ∀ (a : α) (h : Bounded nil (↑a : WithBot α) o₂), Bounded nil (↑a : WithBot α) ⊤
Tactic: cases o₁
Cleared hypotheses: o₁, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ (↑x : WithTop α)
h₂ : t₂.Bounded (↑x : WithBot α) o₂
⊢ All (fun (y : α) ↦ All (fun (z : α) ↦ y < z) t₂) t₁
have refine : ∀ (y : α) (yx : y < x), All (fun (z : α) ↦ y < z) t₂
Tactic: refine h₁.mem_lt.imp fun y yx => ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
⊢ Ordnode α
have node : (rs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id r with _ | rs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
⊢ Ordnode α
have nil₁ : (ls : ℕ) → (ll : Ordnode α) → (lx : α) → (lr : Ordnode α) → Ordnode α
Tactic: rcases id l with _ | ⟨ls, ll, lx, lr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr nil : Ordnode α
⊢ Ordnode α
have nil₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id ll with _ | lls
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr nil : Ordnode α
⊢ Ordnode α
have nil₁ : ℕ → Ordnode α → (lrx : α) → Ordnode α → Ordnode α
Tactic: rcases lr with _ | ⟨_, _, lrx⟩
Cleared hypotheses: lr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 nil : Ordnode α
⊢ Ordnode α
have nil₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
Tactic: rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
⊢ Ordnode α
have node₁ : (ls : ℕ) → (ll : Ordnode α) → (lx : α) → (lr : Ordnode α) → Ordnode α
Tactic: rcases id l with _ | ⟨ls, ll, lx, lr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
⊢ Ordnode α
have node₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id ll with _ | lls
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_2 : Ordnode α
x_2 : α
r_2 node : Ordnode α
⊢ Ordnode α
have node₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
Tactic: rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
⊢ Ordnode α
have node : (ls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id l with _ | ls
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
⊢ Ordnode α
have nil₁ : (rs : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → Ordnode α
Tactic: rcases id r with _ | ⟨rs, rl, rx, rr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
⊢ Ordnode α
have nil₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id rr with _ | rrs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
⊢ Ordnode α
have nil₁ : ℕ → Ordnode α → (rlx : α) → Ordnode α → Ordnode α
Tactic: rcases rl with _ | ⟨_, _, rlx⟩
Cleared hypotheses: rl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 nil : Ordnode α
⊢ Ordnode α
have nil₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
Tactic: rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
⊢ Ordnode α
have node₁ : (rs : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → Ordnode α
Tactic: rcases id r with _ | ⟨rs, rl, rx, rr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node : Ordnode α
⊢ Ordnode α
have node₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id rr with _ | rrs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_2 : Ordnode α
x_2 : α
r_2 node : Ordnode α
⊢ Ordnode α
have node₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
Tactic: rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
⊢ Ordnode α
have node : (ls : ℕ) → (ll : Ordnode α) → (lx : α) → (lr : Ordnode α) → Ordnode α
Tactic: rcases id l with _ | ⟨ls, ll, lx, lr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
⊢ Ordnode α
have nil₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
Tactic: rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
⊢ Ordnode α
have nil₁ : ℕ → Ordnode α → α → Ordnode α → Ordnode α
Tactic: cases id rr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr nil : Ordnode α
⊢ Ordnode α
have nil₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id rr with _ | rrs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
⊢ Ordnode α
have node₁ : (rs : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → Ordnode α
Tactic: rcases id r with _ | ⟨rs, rl, rx, rr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
⊢ Ordnode α
have node₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id ll with _ | lls
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
⊢ Ordnode α
have node₁ : ℕ → Ordnode α → (lrx : α) → Ordnode α → Ordnode α
Tactic: rcases lr with _ | ⟨_, _, lrx⟩
Cleared hypotheses: lr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
⊢ Ordnode α
have node₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
Tactic: rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node : Ordnode α
⊢ Ordnode α
have node₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
Tactic: rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr node : Ordnode α
⊢ Ordnode α
have node₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id rr with _ | rrs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node : Ordnode α
⊢ Ordnode α
have node₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
Tactic: rcases id ll with _ | lls
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordnode (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
⊢ Ordnode α
have node₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
Tactic: rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
r : Ordnode α
lo : WithBot α
hi : WithTop α
ol : l.Bounded lo (↑x : WithTop α)
Or : r.Bounded (↑x : WithBot α) hi
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x : WithTop α) lo
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi (↑x : WithBot α)
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.dual.size l.dual.size
have rw : BalancedSz r.size l.size
Tactic: rw [size_dual, size_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
⊢ Valid' o₁ t o₂
have this : Valid' o₁ t.dual.dual o₂
Tactic: have := Valid'.dual h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂
have rwa : ∀ (this : Valid' o₁ t o₂), Valid' o₁ t o₂
Tactic: rwa [dual_dual, OrderDual.Preorder.dual_dual] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hm : Valid' (↑x : WithBot α) m (↑y : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
Hm : 0 < m.size
H :
  l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ m.size ∧
        delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x m y r) o₂
have nil : ∀ (hm : Valid' (↑x : WithBot α) nil (↑y : WithTop α)) (Hm : 0 < size.{u_1} (α := α) nil)
  (H :
    l.size = 0 ∧ size.{u_1} (α := α) nil = 1 ∧ r.size ≤ 1 ∨
      0 < l.size ∧
        ratio * r.size ≤ size.{u_1} (α := α) nil ∧
          delta * l.size ≤ size.{u_1} (α := α) nil + r.size ∧
            3 * (size.{u_1} (α := α) nil + r.size) ≤ 16 * l.size + 9 ∧ size.{u_1} (α := α) nil ≤ delta * r.size),
  Valid' o₁ (l.node4L x nil y r) o₂
Tactic: obtain - | ⟨s, ml, z, mr⟩ := m
Cleared hypotheses: m, hm, Hm, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hm : Valid' (↑x : WithBot α) m (↑y : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
Hm : 0 < m.size
H :
  l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ m.size ∧
        delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ delta * r.size
nil :
  ∀ (hm : Valid' (↑x : WithBot α) Ordnode.nil (↑y : WithTop α)) (Hm : 0 < size.{u_1} (α := α) Ordnode.nil)
    (H :
      l.size = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 1 ∧ r.size ≤ 1 ∨
        0 < l.size ∧
          ratio * r.size ≤ size.{u_1} (α := α) Ordnode.nil ∧
            delta * l.size ≤ size.{u_1} (α := α) Ordnode.nil + r.size ∧
              3 * (size.{u_1} (α := α) Ordnode.nil + r.size) ≤ 16 * l.size + 9 ∧
                size.{u_1} (α := α) Ordnode.nil ≤ delta * r.size),
    Valid' o₁ (l.node4L x Ordnode.nil y r) o₂
⊢ Valid' o₁ (l.node4L x m y r) o₂
have node : ∀ (s : ℕ) (ml : Ordnode α) (z : α) (mr : Ordnode α)
  (hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)) (Hm : 0 < (Ordnode.node s ml z mr).size)
  (H :
    l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
      0 < l.size ∧
        ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
          delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
            3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
              (Ordnode.node s ml z mr).size ≤ delta * r.size),
  Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂
Tactic: obtain - | ⟨s, ml, z, mr⟩ := m
Cleared hypotheses: m, hm, Hm, H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂
have node : BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: suffices
    BalancedSz (size l) (size ml) ∧
      BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1) from
    Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have node : ∀ (l0 : l.size = 0) (m1 : (Ordnode.node s ml z mr).size = 1) (r0 : r.size ≤ 1),
  BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
node :
  ∀ (l0 : l.size = 0) (m1 : (Ordnode.node s ml z mr).size = 1) (r0 : r.size ≤ 1),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have node₁ : ∀ (l0 : 0 < l.size) (mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size)
  (lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size)
  (lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9)
  (mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size),
  BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Tactic: rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : (Ordnode.node s ml z mr).size = 1
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have m1₁ : ml.size = 0 ∧ mr.size = 0
Tactic: rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1
Cleared hypotheses: m1, r0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
have node : BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
Tactic: rw [l0, m1.1, m1.2]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
have node : ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
Tactic: revert r0
Cleared hypotheses: r0