awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
nil :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ Ordnode.nil a₂),
    Valid' (Option.map f a₁) (map f Ordnode.nil) (Option.map f a₂) ∧
      (map f Ordnode.nil).size = size.{u_1} (α := α) Ordnode.nil
⊢ Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.size
have node : ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α)
  (t_ih_l :
    ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ l a₂),
      Valid' (Option.map f a₁) (map f l) (Option.map f a₂) ∧ (map f l).size = l.size)
  (t_ih_r :
    ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ r a₂),
      Valid' (Option.map f a₁) (map f r) (Option.map f a₂) ∧ (map f r).size = r.size)
  {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ (Ordnode.node size l x r) a₂),
  Valid' (Option.map f a₁) (map f (Ordnode.node size l x r)) (Option.map f a₂) ∧
    (map f (Ordnode.node size l x r)).size = (Ordnode.node size l x r).size
Tactic: induction t generalizing a₁ a₂ with
  | nil =>
    simp only [map, size_nil, and_true]; apply valid'_nil
    cases a₁; · trivial
    cases a₂; · trivial
    simp only [Option.map, Bounded]
    exact f_strict_mono h.ord
  | node _ _ _ _ t_ih_l t_ih_r =>
    have t_ih_l' := t_ih_l h.left
    have t_ih_r' := t_ih_r h.right
    clear t_ih_l t_ih_r
    obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
    obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
    simp only [map, size_node, and_true]
    constructor
    · exact And.intro t_l_valid.ord t_r_valid.ord
    · constructor
      · rw [t_l_size, t_r_size]; exact h.sz.1
      · constructor
        · exact t_l_valid.sz
        · exact t_r_valid.sz
    · constructor
      · rw [t_l_size, t_r_size]; exact h.bal.1
      · constructor
        · exact t_l_valid.bal
        · exact t_r_valid.bal
Cleared hypotheses: t, a₁, a₂, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_l a₂),
    Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_r a₂),
    Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
⊢ Valid' a₁ (erase x (Ordnode.node size t_l t_x t_r)) a₂ ∧
    Raised (erase x (Ordnode.node size t_l t_x t_r)).size (Ordnode.node size t_l t_x t_r).size
have node : Valid' a₁
    (match (motive := Ordering → Ordnode α) cmpLE x t_x with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    size
Tactic: simp only [erase, size_node]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_l a₂),
    Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_r a₂),
    Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have t_ih_l' : Valid' a₁ (erase x t_l) (↑t_x : WithTop α) ∧ Raised (erase x t_l).size t_l.size
Tactic: have t_ih_l' := t_ih_l h.left
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_l a₂),
    Valid' a₁ (erase x t_l) a₂ ∧ Raised (erase x t_l).size t_l.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_r a₂),
    Valid' a₁ (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) (↑t_x : WithTop α) ∧ Raised (erase x t_l).size t_l.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have t_ih_r' : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
Tactic: have t_ih_r' := t_ih_r h.right
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) (↑t_x : WithTop α) ∧ Raised (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
Tactic: obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
Cleared hypotheses: t_ih_l'
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_ih_l' : Valid' a₁ (erase x t_l) (↑t_x : WithTop α) ∧ Raised (erase x t_l).size t_l.size
t_ih_r' : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have t_l_size : Raised (erase x t_l).size t_l.size
Tactic: obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
Cleared hypotheses: t_ih_l'
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_ih_r' : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
Tactic: obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
Cleared hypotheses: t_ih_r'
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_ih_r' : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have t_r_size : Raised (erase x t_r).size t_r.size
Tactic: obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
Cleared hypotheses: t_ih_r'
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have node : Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.lt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    size
Tactic: cases cmpLE x t_x
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
node :
  Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have node₁ : Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.eq with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    size
Tactic: cases cmpLE x t_x
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
node :
  Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
node₁ :
  Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) cmpLE x t_x with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) cmpLE x t_x with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have node₂ : Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.gt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    size
Tactic: cases cmpLE x t_x
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have node : Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.lt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    (t_l.size + t_r.size + 1)
Tactic: rw [h.sz.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.eq with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have node : Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.eq with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    (t_l.size + t_r.size + 1)
Tactic: rw [h.sz.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.gt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      size
have node : Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.gt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂ ∧
  Raised
    (Ordnode.size.{u_1} (α := α)
      (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
    (t_l.size + t_r.size + 1)
Tactic: rw [h.sz.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ (r' : ℕ), Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      (t_l.size + t_r.size + 1)
have left : Valid' a₁
  (match (motive := Ordering → Ordnode α) Ordering.lt with
  | Ordering.lt => (erase x t_l).balanceR t_x t_r
  | Ordering.eq => t_l.glue t_r
  | Ordering.gt => t_l.balanceL t_x (erase x t_r))
  a₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) (↑t_x : WithTop α)
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ (l' : ℕ), Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ (r' : ℕ), Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
left :
  Valid' a₁
    (match (motive := Ordering → Ordnode α) Ordering.lt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r))
    a₂
⊢ Valid' a₁
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r))
      a₂ ∧
    Raised
      (Ordnode.size.{u_1} (α := α)
        (match (motive := Ordering → Ordnode α) Ordering.lt with
        | Ordering.lt => (erase x t_l).balanceR t_x t_r
        | Ordering.eq => t_l.glue t_r
        | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
      (t_l.size + t_r.size + 1)
have right : Raised
  (Ordnode.size.{u_1} (α := α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
    | Ordering.lt => (erase x t_l).balanceR t_x t_r
    | Ordering.eq => t_l.glue t_r
    | Ordering.gt => t_l.balanceL t_x (erase x t_r)))
  (t_l.size + t_r.size + 1)
Tactic: constructor