Theorem: project.IsHeapForest'_of_IsHeapForest' (Project/Merge.lean)

State before:
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
⊢ IsBinTree r → y < r.rank → IsHeapForest' r.rank x → IsHeapForest' y (r :: x)
Tactic:
intros
State after:
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
a✝² : IsBinTree r
a✝¹ : y < r.rank
a✝ : IsHeapForest' r.rank x
⊢ IsHeapForest' y (r :: x)

State before:
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
a✝² : IsBinTree r
a✝¹ : y < r.rank
a✝ : IsHeapForest' r.rank x
⊢ IsHeapForest' y (r :: x)
Tactic:
constructor <;> assumption
State after:
no goals