mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
·

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
·

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).Sized
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ Valid' o₁ (l.rotateL x r) o₂

pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂

pp: case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ Valid' o₁ (l.rotateL x r) o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
·

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).Sized
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized

Tactic:
·

Goal state after:
case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).Sized
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂

pp: case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_3
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
this : ∀ (x y : P.M α), Relation.EqvGen R x y → x = y
⊢ x = y

pp: case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

pp: case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
·

Goal state after:
case refine_3
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
this : ∀ (x y : P.M α), Relation.EqvGen R x y → x = y
⊢ x = y
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).size = l.size + r.size + 1

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).size = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
this : r.size ≤ 3 * (l.size + 1)
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
·

Goal state after:
case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)

pp: case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
·

Goal state after:
case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ Equivalence (Relation.EqvGen R)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl.inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inl.inr
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left✝ : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inr.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
·

Goal state after:
case inl.inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
·

Goal state after:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ ∀ (x y : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl.inr
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left✝ : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inr.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
·

Goal state after:
case inl.inr
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left✝ : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
cases m <;> simp [node4R, all_node', All, all_node3R, and_assoc]

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl.inr
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left✝ : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact
      le_trans h₂
        (Nat.mul_le_mul_left _ <| le_trans (Nat.dist_tri_right _ _) (Nat.add_le_add_left hl _))

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ 1 + 1 ≤ 3 * (l.size + 1)

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (r.dual.rotateL x l.dual) ↔ All P l ∧ P x ∧ All P r

Tactic:
all_rotateL

Goal state after:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝

pp: case refine_2.refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ : P.M α
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝

pp: case refine_2.symm
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : Relation.EqvGen R x✝ y✝
a_ih✝ :
  (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝

pp: case refine_2.trans
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ z✝ : P.M α
a✝¹ : Relation.EqvGen R x✝ y✝
a✝ : Relation.EqvGen R y✝ z✝
a_ih✝¹ :
  (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝
a_ih✝ :
  (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P z✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P z✝

Tactic:
·

Goal state after:
case refine_2.rel
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x✝ y✝ : P.M α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y✝
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5

pp: case inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size

pp: case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
·

Goal state after:
case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
·

Goal state after:
case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5

pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.eraseMin

Tactic:
← dual_dual (eraseMin _),

Goal state after:
α : Type u_1
t : Ordnode α
⊢ t.eraseMax.dual = t.dual.eraseMin.dual.dual
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case pos
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

pp: case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
·

Goal state after:
case pos
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
·

Goal state after:
case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂