awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₂ : r.dual.balanceL x (node sz l' y r').dual.eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₃ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₄ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz l' y r').dual).eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw₅ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz r'.dual y l'.dual)).eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₂ : r.dual.balanceL x (node sz l' y r').dual.eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₃ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₄ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz l' y r').dual).eraseMax
rw₅ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz r'.dual y l'.dual)).eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
have rw₆ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax
Tactic: rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.eraseMin
have rw : t.eraseMax.dual = t.dual.eraseMin.dual.dual
Tactic: rw [← dual_dual (eraseMin _), dual_eraseMin, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
rw : t.eraseMax.dual = t.dual.eraseMin.dual.dual
⊢ t.eraseMax.dual = t.dual.eraseMin
have rw₁ : t.eraseMax.dual = t.dual.dual.eraseMax.dual
Tactic: rw [← dual_dual (eraseMin _), dual_eraseMin, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
rw : t.eraseMax.dual = t.dual.eraseMin.dual.dual
rw₁ : t.eraseMax.dual = t.dual.dual.eraseMax.dual
⊢ t.eraseMax.dual = t.dual.eraseMin
have rw₂ : t.eraseMax.dual = t.eraseMax.dual
Tactic: rw [← dual_dual (eraseMin _), dual_eraseMin, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
have rw : (match (motive := α × Ordnode α → α × Ordnode α) ll.splitMin' lx lr with
  | (xm, l') => (xm, l'.balanceR x r)) =
  ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
Tactic: rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
rw :
  (match (motive := α × Ordnode α → α × Ordnode α) ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
have rw₁ : (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
  | (xm, l') => (xm, l'.balanceR x r)) =
  ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
Tactic: rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
rw :
  (match (motive := α × Ordnode α → α × Ordnode α) ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
rw₁ :
  (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
have rw₂ : (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
  | (xm, l') => (xm, l'.balanceR x r)) =
  (ll.findMin' lx, (node x_1 (node ls ll lx lr) x r).eraseMin)
Tactic: rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
rw :
  (match (motive := α × Ordnode α → α × Ordnode α) ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
rw₁ :
  (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
rw₂ :
  (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    (ll.findMin' lx, (node x_1 (node ls ll lx lr) x r).eraseMin)
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
have rw₃ : (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
  | (xm, l') => (xm, l'.balanceR x r)) =
  (ll.findMin' lx, (node ls ll lx lr).eraseMin.balanceR x r)
Tactic: rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ l.splitMax' x (node ls ll lx lr) = ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
have rw : (match (motive := Ordnode α × α → Ordnode α × α) ll.splitMax' lx lr with
  | (r', xm) => (l.balanceL x r', xm)) =
  ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
Tactic: rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rw :
  (match (motive := Ordnode α × α → Ordnode α × α) ll.splitMax' lx lr with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
⊢ l.splitMax' x (node ls ll lx lr) = ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
have rw₁ : (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
  | (r', xm) => (l.balanceL x r', xm)) =
  ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
Tactic: rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rw :
  (match (motive := Ordnode α × α → Ordnode α × α) ll.splitMax' lx lr with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
rw₁ :
  (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
⊢ l.splitMax' x (node ls ll lx lr) = ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
have rw₂ : (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
  | (r', xm) => (l.balanceL x r', xm)) =
  ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' lx lr)
Tactic: rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x_1 : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rw :
  (match (motive := Ordnode α × α → Ordnode α × α) ll.splitMax' lx lr with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
rw₁ :
  (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
rw₂ :
  (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' lx lr)
⊢ l.splitMax' x (node ls ll lx lr) = ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
have rw₃ : (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
  | (r', xm) => (l.balanceL x r', xm)) =
  (l.balanceL x (node ls ll lx lr).eraseMax, findMax' lx lr)
Tactic: rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
⊢ t.merge nil = t
have nil : Eq.{u_1 + 1} (α := Ordnode α) (merge nil nil) nil
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
nil : Eq.{u_1 + 1} (α := Ordnode α) (merge Ordnode.nil Ordnode.nil) Ordnode.nil
⊢ t.merge Ordnode.nil = t
have node : ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α), (node size l x r).merge Ordnode.nil = node size l x r
Tactic: cases t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (Ordnode.insert x (node size l y r)).dual = Ordnode.insert x (node size l y r).dual
have this : cmpLE x y = cmpLE y x
Tactic: have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (Ordnode.insert x (node size l y r)).dual = Ordnode.insert x (node size l y r).dual
have rw : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (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)))
  (match (motive := Ordering → Ordnode αᵒᵈ) (cmpLE x y).swap with
  | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
  | Ordering.eq => node size r.dual x l.dual
  | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
Tactic: rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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)))
    (match (motive := Ordering → Ordnode αᵒᵈ) (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
have lt : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (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)))
  (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.lt.swap with
  | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
  | Ordering.eq => node size r.dual x l.dual
  | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.lt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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)))
    (match (motive := Ordering → Ordnode αᵒᵈ) (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
have eq : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (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)))
  (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.eq.swap with
  | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
  | Ordering.eq => node size r.dual x l.dual
  | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.lt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
eq :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.eq.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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)))
    (match (motive := Ordering → Ordnode αᵒᵈ) (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
have gt : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (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)))
  (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.gt.swap with
  | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
  | Ordering.eq => node size r.dual x l.dual
  | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
⊢ l.balance x r = l.balance' x r
have nil : ∀ (hl : Balanced.{u_1} (α := α) nil) (sl : Sized.{u_1} (α := α) nil), balance nil x r = balance' nil x r
Tactic: obtain - | ⟨ls, ll, lx, lr⟩ := l
Cleared hypotheses: l, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
nil :
  ∀ (hl : Balanced.{u_1} (α := α) Ordnode.nil) (sl : Sized.{u_1} (α := α) Ordnode.nil),
    balance Ordnode.nil x r = balance' Ordnode.nil x r
⊢ l.balance x r = l.balance' x r
have node : ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α) (hl : (node ls ll lx lr).Balanced)
  (sl : (node ls ll lx lr).Sized), (node ls ll lx lr).balance x r = (node ls ll lx lr).balance' x r
Tactic: obtain - | ⟨ls, ll, lx, lr⟩ := l
Cleared hypotheses: l, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
r : Ordnode α
hr : r.Balanced
sr : r.Sized
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
⊢ balance nil x r = balance' nil x r
have nil : ∀ (hr : Balanced.{u_1} (α := α) nil) (sr : Sized.{u_1} (α := α) nil), balance nil x nil = balance' nil x nil
Tactic: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
r : Ordnode α
hr : r.Balanced
sr : r.Sized
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
nil :
  ∀ (hr : Balanced.{u_1} (α := α) Ordnode.nil) (sr : Sized.{u_1} (α := α) Ordnode.nil),
    balance Ordnode.nil x Ordnode.nil = balance' Ordnode.nil x Ordnode.nil
⊢ balance Ordnode.nil x r = balance' Ordnode.nil x r
have nil₁ : ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) (hr : (node rs rl rx rr).Balanced)
  (sr : (node rs rl rx rr).Sized), balance Ordnode.nil x (node rs rl rx rr) = balance' Ordnode.nil x (node rs rl rx rr)
Tactic: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ balance nil x (node rs rl rx rr) = balance' nil x (node rs rl rx rr)
have nil : ∀ (hr : (rl.node' rx rr).Balanced) (sr : (node rs rl rx rr).Sized),
  balance nil x (rl.node' rx rr) = balance' nil x (rl.node' rx rr)
Tactic: rw [sr.eq_node'] at hr ⊢
Cleared hypotheses: hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (rl.node' rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ balance nil x (rl.node' rx rr) = balance' nil x (rl.node' rx rr)
have nil : ∀ (hr : (node' nil rx rr).Balanced) (sr : (node rs nil rx rr).Sized),
  balance nil x (node' nil rx rr) = balance' nil x (node' nil rx rr)
Tactic: obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
Cleared hypotheses: rl, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (rl.node' rx rr).Balanced
sr : (node rs rl rx rr).Sized
nil :
  ∀ (hr : (node' Ordnode.nil rx rr).Balanced) (sr : (node rs Ordnode.nil rx rr).Sized),
    balance Ordnode.nil x (node' Ordnode.nil rx rr) = balance' Ordnode.nil x (node' Ordnode.nil rx rr)
⊢ balance Ordnode.nil x (rl.node' rx rr) = balance' Ordnode.nil x (rl.node' rx rr)
have nil₁ : ∀ (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) (hr : ((node rls rll rlx rlr).node' rx rr).Balanced)
  (sr : (node rs (node rls rll rlx rlr) rx rr).Sized),
  balance Ordnode.nil x ((node rls rll rlx rlr).node' rx rr) =
    balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx rr)
Tactic: obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
Cleared hypotheses: rl, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rr : Ordnode α
hr : (node' nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
⊢ balance nil x (node' nil rx rr) = balance' nil x (node' nil rx rr)
have nil : ∀ (hr : (node' nil rx nil).Balanced) (sr : (node rs nil rx nil).Sized),
  balance nil x (node' nil rx nil) = balance' nil x (node' nil rx nil)
Tactic: obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
Cleared hypotheses: rr, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rr : Ordnode α
hr : (node' Ordnode.nil rx rr).Balanced
sr : (node rs Ordnode.nil rx rr).Sized
nil :
  ∀ (hr : (node' Ordnode.nil rx Ordnode.nil).Balanced) (sr : (node rs Ordnode.nil rx Ordnode.nil).Sized),
    balance Ordnode.nil x (node' Ordnode.nil rx Ordnode.nil) = balance' Ordnode.nil x (node' Ordnode.nil rx Ordnode.nil)
⊢ balance Ordnode.nil x (node' Ordnode.nil rx rr) = balance' Ordnode.nil x (node' Ordnode.nil rx rr)
have nil₁ : ∀ (rrs : ℕ) (rrl : Ordnode α) (rrx : α) (rrr : Ordnode α) (hr : (node' Ordnode.nil rx (node rrs rrl rrx rrr)).Balanced)
  (sr : (node rs Ordnode.nil rx (node rrs rrl rrx rrr)).Sized),
  balance Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr)) =
    balance' Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))
Tactic: obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
Cleared hypotheses: rr, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
⊢ balance nil x ((node rls rll rlx rlr).node' rx rr) = balance' nil x ((node rls rll rlx rlr).node' rx rr)
have nil : ∀ (hr : ((node rls rll rlx rlr).node' rx nil).Balanced) (sr : (node rs (node rls rll rlx rlr) rx nil).Sized),
  balance nil x ((node rls rll rlx rlr).node' rx nil) = balance' nil x ((node rls rll rlx rlr).node' rx nil)
Tactic: obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
Cleared hypotheses: rr, hr, sr