Theorem: MinHeap.coe_eq_head?_of_forall_le (Algorithm/Data/Classes/MinHeap.lean)

State before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ ↑x = head? c
Tactic:
contrapose! h
State after:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
⊢ ∃ y ∈ c, p y ∧ y ≠ x ∧ ¬x < y

State before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
⊢ ∃ y ∈ c, p y ∧ y ≠ x ∧ ¬x < y
Tactic:
exact ⟨head c (ToMultiset.not_isEmpty_of_mem hx), MinHeap.head_mem _ _, pc, by intro h'; simp [← h'] at h,
  fun h' ↦ (h'.trans_le (head_le c _ hx)).ne rfl⟩
State after:
no goals

State before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
⊢ head c ⋯ ≠ x
Tactic:
intro h'
State after:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
h' : head c ⋯ = x
⊢ False

State before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
h' : head c ⋯ = x
⊢ False
Tactic:
simp [← h'] at h
State after:
no goals