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

State before:
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hf : IsHeapForest' r (t :: ts)
hpos : t.rank > 0
⊢ IsHeapForest' (t.rank - 1) (t :: ts)
Tactic:
cases hf
State after:
case cons
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hpos : t.rank > 0
a✝² : IsBinTree t
a✝¹ : r < t.rank
a✝ : IsHeapForest' t.rank ts
⊢ IsHeapForest' (t.rank - 1) (t :: ts)

State before:
case cons
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hpos : t.rank > 0
a✝² : IsBinTree t
a✝¹ : r < t.rank
a✝ : IsHeapForest' t.rank ts
⊢ IsHeapForest' (t.rank - 1) (t :: ts)
Tactic:
constructor <;> try assumption
State after:
case cons.a
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hpos : t.rank > 0
a✝² : IsBinTree t
a✝¹ : r < t.rank
a✝ : IsHeapForest' t.rank ts
⊢ t.rank - 1 < t.rank

State before:
case cons.a
α : Sort ?u.14584
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
α✝ : Type u_1
t : BinTree α✝
ts : List (BinTree α✝)
hpos : t.rank > 0
a✝² : IsBinTree t
a✝¹ : r < t.rank
a✝ : IsHeapForest' t.rank ts
⊢ t.rank - 1 < t.rank
Tactic:
. apply Nat.sub_lt_self
  . decide
  . assumption
State after:
no goals

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