Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : 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 : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : y ≤ x
⊢ Valid' o₁
      (match Ordering.eq with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (match Ordering.eq with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)).size

pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : 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 : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
⊢ Valid' o₁
      (match Ordering.lt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (match Ordering.lt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)).size

pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : 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 : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
⊢ Valid' o₁
      (match Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (match Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)).size

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : 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 : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : y ≤ x
⊢ Valid' o₁
      (match Ordering.eq with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (match Ordering.eq with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)).size

case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : 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 : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
⊢ Valid' o₁
      (match Ordering.lt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (match Ordering.lt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)).size

case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : 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 : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
⊢ Valid' o₁
      (match Ordering.gt with
      | Ordering.lt => (insertWith f x l).balanceL y r
      | Ordering.eq => node sz l (f y) r
      | Ordering.gt => l.balanceR y (insertWith f x r))
      o₂ ∧
    Raised (node sz l y r).size
      (match Ordering.gt with
        | Ordering.lt => (insertWith f x l).balanceL y r
        | Ordering.eq => node sz l (f y) r
        | Ordering.gt => l.balanceR y (insertWith f x r)).size