awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (Ordnode.node size (map f l) (f x) (map f r)).Bounded (Option.map f a₁) (Option.map f a₂)

Tactic:
exact And.intro t_l_valid.ord t_r_valid.ord

Premises used: And.intro, Ordnode.Valid'.ord
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
node : size = (map f l).size + (map f r).size + 1
node₁ : (map f l).Sized ∧ (map f r).Sized
⊢ (Ordnode.node size (map f l) (f x) (map f r)).Sized

Tactic:
constructor
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
node : size = l.size + r.size + 1
⊢ size = (map f l).size + (map f r).size + 1

Tactic:
rw [t_l_size, t_r_size]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ size = l.size + r.size + 1

Tactic:
h.sz.1

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ size = l.size + r.size + 1

Tactic:
exact h.sz.1

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
node : (map f l).Sized
node₁ : (map f r).Sized
⊢ (map f l).Sized ∧ (map f r).Sized

Tactic:
constructor
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f l).Sized

Tactic:
t_l_valid.sz

Premises used: Ordnode.Valid'.sz
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f l).Sized

Tactic:
exact t_l_valid.sz

Premises used: Ordnode.Valid'.sz
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f r).Sized

Tactic:
t_r_valid.sz

Premises used: Ordnode.Valid'.sz
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f r).Sized

Tactic:
exact t_r_valid.sz

Premises used: Ordnode.Valid'.sz
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
node : BalancedSz (map f l).size (map f r).size
node₁ : (map f l).Balanced ∧ (map f r).Balanced
⊢ (Ordnode.node size (map f l) (f x) (map f r)).Balanced

Tactic:
constructor
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
node : BalancedSz l.size r.size
⊢ BalancedSz (map f l).size (map f r).size

Tactic:
rw [t_l_size, t_r_size]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ BalancedSz l.size r.size

Tactic:
h.bal.1

Premises used: Ordnode.Valid'.bal, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ BalancedSz l.size r.size

Tactic:
exact h.bal.1

Premises used: Ordnode.Valid'.bal, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
node : (map f l).Balanced
node₁ : (map f r).Balanced
⊢ (map f l).Balanced ∧ (map f r).Balanced

Tactic:
constructor
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f l).Balanced

Tactic:
t_l_valid.bal

Premises used: Ordnode.Valid'.bal
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f l).Balanced

Tactic:
exact t_l_valid.bal

Premises used: Ordnode.Valid'.bal
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f r).Balanced

Tactic:
t_r_valid.bal

Premises used: Ordnode.Valid'.bal
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size l x r) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
t_l_size : (map f l).size = l.size
t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)
t_r_size : (map f r).size = r.size
⊢ (map f r).Balanced

Tactic:
exact t_r_valid.bal

Premises used: Ordnode.Valid'.bal
-- Module: Mathlib.Data.Ordmap.Ordset
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
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
⊢ Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.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

Premises used: Ordnode.size_node, and_true, Ordnode.size_nil, Ordnode.map, Option.map, Ordnode.nil, Ordnode.Bounded, Ordnode.Valid'.node, Ordnode.valid'_nil
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
t : Ordnode α
h : t.Valid
⊢ (map f t).Valid

Tactic:
(Valid'.map_aux f_strict_mono h).1

Premises used: Ordnode.Valid'.map_aux, Ordnode.Valid, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' a₁ (erase x nil) a₂ ∧ Raised (erase x nil).size (size.{u_1} (α := α) nil)

Tactic:
simpa [erase, Raised]

Premises used: Ordnode.erase, Ordnode.Raised
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
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
⊢ 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

Tactic:
simp only [erase, size_node]

Premises used: Ordnode.size_node, Ordnode.erase
-- Module: Mathlib.Data.Ordmap.Ordset
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 t_l) (↑t_x : WithTop α) ∧ Raised (erase x t_l).size t_l.size

Tactic:
have t_ih_l' := t_ih_l h.left
-- Module: Mathlib.Data.Ordmap.Ordset
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' (↑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
-- Module: Mathlib.Data.Ordmap.Ordset
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₁ (erase x t_l) (↑t_x : WithTop α)

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
-- Module: Mathlib.Data.Ordmap.Ordset
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 α)
⊢ Raised (erase x t_l).size t_l.size

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
-- Module: Mathlib.Data.Ordmap.Ordset
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' (↑t_x : WithBot α) (erase x t_r) a₂

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
⊢ Raised (erase x t_r).size t_r.size

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
-- Module: Mathlib.Data.Ordmap.Ordset
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
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
⊢ 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:
cases cmpLE x t_x

Premises used: cmpLE
-- Module: Mathlib.Data.Ordmap.Ordset
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)))
      (t_l.size + t_r.size + 1)
⊢ 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:
rw [h.sz.1]

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
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.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)
⊢ 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:
rw [h.sz.1]

Premises used: Ordnode.Valid'.sz, And.left