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

State before:
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
xs : List (BinTree α✝)
m : ℕ
⊢ IsHeapForest' n xs → m ≤ n → IsHeapForest' m xs
Tactic:
intros hf hle
State after:
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
xs : List (BinTree α✝)
m : ℕ
hf : IsHeapForest' n xs
hle : m ≤ n
⊢ IsHeapForest' m xs

State before:
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
xs : List (BinTree α✝)
m : ℕ
hf : IsHeapForest' n xs
hle : m ≤ n
⊢ IsHeapForest' m xs
Tactic:
cases hf with 
| nil => constructor
| cons hlt _ _ => 
  constructor <;> try assumption
  . apply Nat.lt_of_le_of_lt hle hlt
State after:
no goals

State before:
case nil
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
m : ℕ
hle : m ≤ n
⊢ IsHeapForest' m []
Tactic:
constructor
State after:
no goals

State before:
case cons
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
m : ℕ
hle : m ≤ n
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝¹ : IsBinTree t✝
a✝ : IsHeapForest' t✝.rank ts✝
hlt : n < t✝.rank
⊢ IsHeapForest' m (t✝ :: ts✝)
Tactic:
constructor <;> try assumption
State after:
case cons.a
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
m : ℕ
hle : m ≤ n
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝¹ : IsBinTree t✝
a✝ : IsHeapForest' t✝.rank ts✝
hlt : n < t✝.rank
⊢ m < t✝.rank

State before:
case cons.a
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
m : ℕ
hle : m ≤ n
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝¹ : IsBinTree t✝
a✝ : IsHeapForest' t✝.rank ts✝
hlt : n < t✝.rank
⊢ m < t✝.rank
Tactic:
. apply Nat.lt_of_le_of_lt hle hlt
State after:
no goals

State before:
case cons.a
α : Sort ?u.12184
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
n : ℕ
α✝ : Type u_1
m : ℕ
hle : m ≤ n
t✝ : BinTree α✝
ts✝ : List (BinTree α✝)
a✝¹ : IsBinTree t✝
a✝ : IsHeapForest' t✝.rank ts✝
hlt : n < t✝.rank
⊢ IsHeapForest' t✝.rank ts✝
Tactic:
assumption
State after:
no goals