Theorem: MinHeap.head?_def (Algorithm/Data/Classes/MinHeap.lean)

State before:
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
by_cases hc : isEmpty c
State after:
case pos
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf

case neg
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf

State before:
case pos
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
simp [head?_eq_top c hc, hc]
State after:
no goals

State before:
case neg
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
apply le_antisymm
State after:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf

case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c

State before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
have := head?_le c
State after:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : ∀ x ∈ c, head? c ≤ ↑x
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf

State before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : ∀ x ∈ c, head? c ≤ ↑x
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
aesop
State after:
no goals

State before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c
Tactic:
have := head?_mem_toMultiset_map c hc
State after:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c

State before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c
Tactic:
apply Multiset.inf_le
State after:
case neg.a.h
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ head? c ∈ Multiset.map WithTop.some (toMultiset c)

State before:
case neg.a.h
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ head? c ∈ Multiset.map WithTop.some (toMultiset c)
Tactic:
aesop
State after:
no goals