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

State before:
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ts : List (BinTree α✝)
ry : ℕ
⊢ IsHeapForest' rx ts → ry < hRank ts → IsHeapForest' ry ts
Tactic:
intros hf _
State after:
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ts : List (BinTree α✝)
ry : ℕ
hf : IsHeapForest' rx ts
a✝ : ry < hRank ts
⊢ IsHeapForest' ry ts

State before:
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ts : List (BinTree α✝)
ry : ℕ
hf : IsHeapForest' rx ts
a✝ : ry < hRank ts
⊢ IsHeapForest' ry ts
Tactic:
cases hf
State after:
case nil
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
a✝ : ry < hRank []
⊢ IsHeapForest' ry []

case cons
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝³ : IsBinTree t✝
a✝² : IsHeapForest' t✝.rank ts✝
a✝¹ : rx < t✝.rank
a✝ : ry < hRank (t✝ :: ts✝)
⊢ IsHeapForest' ry (t✝ :: ts✝)

State before:
case nil
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
a✝ : ry < hRank []
⊢ IsHeapForest' ry []

case cons
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝³ : IsBinTree t✝
a✝² : IsHeapForest' t✝.rank ts✝
a✝¹ : rx < t✝.rank
a✝ : ry < hRank (t✝ :: ts✝)
⊢ IsHeapForest' ry (t✝ :: ts✝)
Tactic:
. constructor
State after:
case cons
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝³ : IsBinTree t✝
a✝² : IsHeapForest' t✝.rank ts✝
a✝¹ : rx < t✝.rank
a✝ : ry < hRank (t✝ :: ts✝)
⊢ IsHeapForest' ry (t✝ :: ts✝)

State before:
case cons
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝³ : IsBinTree t✝
a✝² : IsHeapForest' t✝.rank ts✝
a✝¹ : rx < t✝.rank
a✝ : ry < hRank (t✝ :: ts✝)
⊢ IsHeapForest' ry (t✝ :: ts✝)
Tactic:
. constructor
  repeat assumption
State after:
no goals

State before:
case cons.a
α : Sort ?u.15173
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
α✝ : Type u_1
ry : ℕ
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝³ : IsBinTree t✝
a✝² : IsHeapForest' t✝.rank ts✝
a✝¹ : rx < t✝.rank
a✝ : ry < hRank (t✝ :: ts✝)
⊢ IsHeapForest' t✝.rank ts✝
Tactic:
assumption
State after:
no goals