α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
⊢ lookupAll a l = Option.toList (head? (lookupAll a l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
⊢ lookupAll a l = Option.toList (dlookup a l)
rw [← head?_lookupAll]
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
h1 : length (lookupAll a l) ≤ 1
⊢ lookupAll a l = Option.toList (head? (lookupAll a l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
⊢ lookupAll a l = Option.toList (head? (lookupAll a l))
have h1 := lookupAll_length_le_one a h
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
⊢ length (lookupAll a l) ≤ 1 → lookupAll a l = Option.toList (head? (lookupAll a l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
h1 : length (lookupAll a l) ≤ 1
⊢ lookupAll a l = Option.toList (head? (lookupAll a l))
revert h1
case cons.cons
α : Type u
β : α → Type v
l✝¹ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : NodupKeys l✝
b c : β a
l : List (β a)
h1 : length (b :: c :: l) ≤ 1
⊢ b :: c :: l = Option.toList (head? (b :: c :: l))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : NodupKeys l
⊢ length (lookupAll a l) ≤ 1 → lookupAll a l = Option.toList (head? (lookupAll a l))
rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩) <;> intro h1 <;> try rfl
no goals
case cons.cons
α : Type u
β : α → Type v
l✝¹ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : NodupKeys l✝
b c : β a
l : List (β a)
h1 : length (b :: c :: l) ≤ 1
⊢ b :: c :: l = Option.toList (head? (b :: c :: l))
exact absurd h1 (by simp)
case cons.cons
α : Type u
β : α → Type v
l✝¹ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : NodupKeys l✝
b c : β a
l : List (β a)
h1 : length (b :: c :: l) ≤ 1
⊢ b :: c :: l = Option.toList (head? (b :: c :: l))
case cons.cons
α : Type u
β : α → Type v
l✝¹ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : NodupKeys l✝
b c : β a
l : List (β a)
h1 : length (b :: c :: l) ≤ 1
⊢ b :: c :: l = Option.toList (head? (b :: c :: l))
rfl
no goals
α : Type u
β : α → Type v
l✝¹ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : NodupKeys l✝
b c : β a
l : List (β a)
h1 : length (b :: c :: l) ≤ 1
⊢ ¬length (b :: c :: l) ≤ 1
simp