awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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.{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 α)
have 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 α)
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases cmpLE x y
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (insert' x t).Valid
have rw : (insertWith id x t).Valid
Tactic: rw [insert'_eq_insertWith]
-- 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
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) (map f nil) (Option.map f a₂) ∧ (map f nil).size = size.{u_1} (α := α) nil
have nil : Valid' (Option.map f a₁) nil (Option.map f a₂)
Tactic: simp only [map, size_nil, and_true]
-- 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
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) nil (Option.map f a₂)
have nil : Bounded nil (Option.map f a₁) (Option.map f a₂)
Tactic: apply valid'_nil
-- 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
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Bounded nil (Option.map f a₁) (Option.map f a₂)
have nil : ∀ (h : Valid' ⊥ nil a₂), Bounded nil (Option.map f ⊥) (Option.map f a₂)
Tactic: cases a₁
Cleared hypotheses: a₁, h
-- 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
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₂)
⊢ Bounded Ordnode.nil (Option.map f a₁) (Option.map f a₂)
have nil₁ : ∀ (a : α) (h : Valid' (↑a : WithBot α) Ordnode.nil a₂),
  Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f a₂)
Tactic: cases a₁
Cleared hypotheses: a₁, h
-- 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
a₂ : WithTop α
a : α
h : Valid' (↑a : WithBot α) nil a₂
⊢ Bounded nil (Option.map f (↑a : WithBot α)) (Option.map f a₂)
have nil : ∀ (h : Valid' (↑a : WithBot α) nil ⊤), Bounded nil (Option.map f (↑a : WithBot α)) (Option.map f ⊤)
Tactic: cases a₂
Cleared hypotheses: a₂, h
-- 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
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 ⊤)
⊢ Bounded Ordnode.nil (Option.map f (↑a : WithBot α)) (Option.map f a₂)
have 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 α))
Tactic: cases a₂
Cleared hypotheses: a₂, h
-- 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
a a_1 : α
h : Valid' (↑a : WithBot α) nil (↑a_1 : WithTop α)
⊢ Bounded nil (Option.map f (↑a : WithBot α)) (Option.map f (↑a_1 : WithTop α))
have nil : f a < f a_1
Tactic: simp only [Option.map, Bounded]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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 (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
have t_ih_l' : 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
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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 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
have t_ih_r' : 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
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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 (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
have t_l_valid : Valid' (Option.map f a₁) (map f l) (Option.map f (↑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 α
β : 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 α))
⊢ 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
have t_l_size : (map f l).size = 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 α
β : 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 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
have t_r_valid : Valid' (Option.map f (↑x : WithBot α)) (map f r) (Option.map f 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 α
β : 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₂)
⊢ 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
have t_r_size : (map f r).size = 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 α
β : 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
⊢ 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
have node : Valid' (Option.map f a₁) (Ordnode.node size (map f l) (f x) (map f r)) (Option.map f a₂)
Tactic: simp only [map, size_node, and_true]
-- 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
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
⊢ Valid' (Option.map f a₁) (Ordnode.node size (map f l) (f x) (map f r)) (Option.map f a₂)
have node : (Ordnode.node size (map f l) (f x) (map f r)).Bounded (Option.map f a₁) (Option.map f a₂)
Tactic: constructor
-- 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
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₂)
⊢ Valid' (Option.map f a₁) (Ordnode.node size (map f l) (f x) (map f r)) (Option.map f a₂)
have node₁ : (Ordnode.node size (map f l) (f x) (map f r)).Sized
Tactic: constructor
-- 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
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
⊢ Valid' (Option.map f a₁) (Ordnode.node size (map f l) (f x) (map f r)) (Option.map f a₂)
have node₂ : (Ordnode.node size (map f l) (f x) (map f r)).Balanced
Tactic: constructor
-- 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
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)).Sized
have node : size = (map f l).size + (map f r).size + 1
Tactic: constructor
-- 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
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
⊢ (Ordnode.node size (map f l) (f x) (map f r)).Sized
have node₁ : (map f l).Sized ∧ (map f r).Sized
Tactic: constructor
-- 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
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 = (map f l).size + (map f r).size + 1
have node : size = l.size + r.size + 1
Tactic: rw [t_l_size, t_r_size]
-- 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
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 ∧ (map f r).Sized
have node : (map f l).Sized
Tactic: constructor
-- 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
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
⊢ (map f l).Sized ∧ (map f r).Sized
have node₁ : (map f r).Sized
Tactic: constructor
-- 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
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)).Balanced
have node : BalancedSz (map f l).size (map f r).size
Tactic: constructor
-- 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
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
⊢ (Ordnode.node size (map f l) (f x) (map f r)).Balanced
have node₁ : (map f l).Balanced ∧ (map f r).Balanced
Tactic: constructor
-- 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
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 (map f l).size (map f r).size
have node : BalancedSz l.size r.size
Tactic: rw [t_l_size, t_r_size]
-- 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
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 ∧ (map f r).Balanced
have node : (map f l).Balanced
Tactic: constructor
-- 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
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
⊢ (map f l).Balanced ∧ (map f r).Balanced
have node₁ : (map f r).Balanced
Tactic: constructor
-- 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₂
⊢ Valid' (Option.map f a₁) (map f t) (Option.map f a₂) ∧ (map f t).size = t.size
have nil : ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ nil a₂),
  Valid' (Option.map f a₁) (map f nil) (Option.map f a₂) ∧ (map f nil).size = size.{u_1} (α := α) nil
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