awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
⊢ (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'

Tactic:
Or.inr ⟨_, e, h.3.1⟩

Premises used: Ordnode.Valid'.bal, And.left, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : Bounded nil o₁ (↑x : WithTop α)
br : Bounded nil (↑x : WithBot α) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y : WithBot α) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
⊢ (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' (insertWith f x r).size) ∨
    ∃ (r' : ℕ), Raised r' (insertWith f x r).size ∧ BalancedSz l.size r'

Tactic:
exact Or.inr ⟨_, e, h.3.1⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
t : Ordnode α
h : t.Valid
⊢ (insertWith f x t).Valid

Tactic:
(insertWith.valid_aux _ _ hf h ⟨⟩ ⟨⟩).1

Premises used: Ordnode.insertWith.valid_aux, Ordnode.Valid, And.left, True.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
unfold :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)
⊢ Ordnode.insert x (node size l y r) = insertWith (fun (x_1 : α) ↦ x) x (node size l y r)

Tactic:
unfold Ordnode.insert insertWith

Premises used: Ordnode.insertWith, Ordnode.insert
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)
eq :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)
gt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)

Tactic:
cases cmpLE x y

Premises used: cmpLE
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)

Tactic:
simp [insert_eq_insertWith]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)

Tactic:
simp [insert_eq_insertWith]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (insertWith (fun (x_1 : α) ↦ x) x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (insertWith (fun (x_1 : α) ↦ x) x r) :
      Ordnode α)

Tactic:
simp [insert_eq_insertWith]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
rw : (insertWith (fun (x_1 : α) ↦ x) x t).Valid
⊢ (Ordnode.insert x t).Valid

Tactic:
rw [insert_eq_insertWith]

Premises used: Ordnode.insert_eq_insertWith
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun (x_1 : α) ↦ x) x t).Valid

Tactic:
insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

Premises used: le_rfl, Ordnode.insertWith.valid, And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun (x_1 : α) ↦ x) x t).Valid

Tactic:
exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

Premises used: le_rfl, Ordnode.insertWith.valid, And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
unfold :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)
⊢ insert' x (node size l y r) = insertWith id x (node size l y r)

Tactic:
unfold insert' insertWith

Premises used: Ordnode.insertWith, Ordnode.insert'
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)
eq :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)
gt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)

Tactic:
cases cmpLE x y

Premises used: cmpLE
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)

Tactic:
simp [insert'_eq_insertWith]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)

Tactic:
simp [insert'_eq_insertWith]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (insert' x l).balanceL y r
      | Ordering.eq => node size l y r
      | Ordering.gt => l.balanceR y (insert' x r) :
      Ordnode α)
    (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (insertWith id x l).balanceL y r
      | Ordering.eq => node size l (id y) r
      | Ordering.gt => l.balanceR y (insertWith id x r) :
      Ordnode α)

Tactic:
simp [insert'_eq_insertWith]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
rw : (insertWith id x t).Valid
⊢ (insert' x t).Valid

Tactic:
rw [insert'_eq_insertWith]

Premises used: Ordnode.insert'_eq_insertWith
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid

Tactic:
insertWith.valid _ _ (fun _ => id) h

Premises used: Ordnode.insertWith.valid, id
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith id x t).Valid

Tactic:
exact insertWith.valid _ _ (fun _ => id) h

Premises used: Ordnode.insertWith.valid, id
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ Ordnode.nil a₂
nil : Valid' (Option.map f a₁) Ordnode.nil (Option.map f a₂)
⊢ Valid' (Option.map f a₁) (map f Ordnode.nil) (Option.map f a₂) ∧
    (map f Ordnode.nil).size = size.{u_1} (α := α) Ordnode.nil

Tactic:
simp only [map, size_nil, and_true]

Premises used: and_true, Ordnode.size_nil, Ordnode.map
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ Ordnode.nil a₂
nil : Bounded Ordnode.nil (Option.map f a₁) (Option.map f a₂)
⊢ Valid' (Option.map f a₁) Ordnode.nil (Option.map f a₂)

Tactic:
apply valid'_nil

Premises used: 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
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ Ordnode.nil a₂
nil : ∀ (h : Valid' ⊥ Ordnode.nil a₂), Bounded Ordnode.nil (Option.map f ⊥) (Option.map f a₂)
nil₁ :
  ∀ (a : α) (h : Valid' (↑a : WithBot α) Ordnode.nil a₂),
    Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f a₂)
⊢ Bounded Ordnode.nil (Option.map f a₁) (Option.map f a₂)

Tactic:
cases a₁
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
h : Valid' ⊥ nil a₂
⊢ Bounded nil (Option.map f ⊥) (Option.map f a₂)

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₂ : WithTop α
a : α
h : Valid' (↑a : WithBot α) Ordnode.nil a₂
nil :
  ∀ (h : Valid' (↑a : WithBot α) Ordnode.nil ⊤), Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f ⊤)
nil₁ :
  ∀ (a_1 : α) (h : Valid' (↑a : WithBot α) Ordnode.nil (↑a_1 : WithTop α)),
    Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f (↑a_1 : WithTop α))
⊢ Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f a₂)

Tactic:
cases a₂
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a : α
h : Valid' (↑a : WithBot α) nil ⊤
⊢ Bounded nil (Option.map f (↑a : WithBot α)) (Option.map f ⊤)

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a a_1 : α
h : Valid' (↑a : WithBot α) Ordnode.nil (↑a_1 : WithTop α)
nil : f a < f a_1
⊢ Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f (↑a_1 : WithTop α))

Tactic:
simp only [Option.map, Bounded]

Premises used: Option.map, Ordnode.Bounded
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
β : Type u_2
inst_1 : Preorder β
f : α → β
f_strict_mono : StrictMono f
a a_1 : α
h : Valid' (↑a : WithBot α) nil (↑a_1 : WithTop α)
⊢ f a < f a_1

Tactic:
f_strict_mono h.ord

Premises used: 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
a a_1 : α
h : Valid' (↑a : WithBot α) nil (↑a_1 : WithTop α)
⊢ f a < f a_1

Tactic:
exact f_strict_mono h.ord

Premises used: 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 α
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 l) (Option.map f (↑x : WithTop α)) ∧ (map f l).size = l.size

Tactic:
have t_ih_l' := t_ih_l h.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 α
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₂
t_ih_l' : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α)) ∧ (map f l).size = l.size
⊢ Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂) ∧ (map f r).size = r.size

Tactic:
have t_ih_r' := t_ih_r h.right
-- 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_ih_l' : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α)) ∧ (map f l).size = l.size
t_ih_r' : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂) ∧ (map f r).size = r.size
⊢ Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
-- 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_ih_l' : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α)) ∧ (map f l).size = l.size
t_ih_r' : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂) ∧ (map f r).size = r.size
t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑x : WithTop α))
⊢ (map f l).size = l.size

Tactic:
obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
-- 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_ih_r' : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂) ∧ (map f r).size = r.size
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
⊢ Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂)

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
-- 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_ih_r' : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f a₂) ∧ (map f r).size = r.size
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₂)
⊢ (map f r).size = r.size

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
-- 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 : Valid' (Option.map f a₁) (Ordnode.node size (map f l) (f x) (map f r)) (Option.map f 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:
simp only [map, size_node, and_true]

Premises used: Ordnode.size_node, and_true, Ordnode.map
-- 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 : (Ordnode.node size (map f l) (f x) (map f r)).Bounded (Option.map f a₁) (Option.map f a₂)
node₁ : (Ordnode.node size (map f l) (f x) (map f r)).Sized
node₂ : (Ordnode.node size (map f l) (f x) (map f r)).Balanced
⊢ Valid' (Option.map f a₁) (Ordnode.node size (map f l) (f x) (map f r)) (Option.map f a₂)

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
⊢ (Ordnode.node size (map f l) (f x) (map f r)).Bounded (Option.map f a₁) (Option.map f a₂)

Tactic:
And.intro t_l_valid.ord t_r_valid.ord

Premises used: And.intro, Ordnode.Valid'.ord, Ordnode.Bounded