Theorem: List.NodupKeys.lookup_eq_some (Lean4Lean/Std/NodupKeys.lean)

State before:
case nil
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
nd : NodupKeys []
⊢ lookup a [] = some b ↔ (a, b) ∈ []
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
nd : NodupKeys (p :: l)
⊢ lookup a (p :: l) = some b ↔ (a, b) ∈ p :: l
Tactic:
let (a', b') := p
State after:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : NodupKeys ((a', b') :: l)
⊢ lookup a ((a', b') :: l) = some b ↔ (a, b) ∈ (a', b') :: l

State before:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : NodupKeys ((a', b') :: l)
⊢ lookup a ((a', b') :: l) = some b ↔ (a, b) ∈ (a', b') :: l
Tactic:
simp [lookup] at nd ⊢
State after:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
⊢ (match a == a' with
      | true => some b'
      | false => lookup a l) =
      some b ↔
    a = a' ∧ b = b' ∨ (a, b) ∈ l

State before:
case cons
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
⊢ (match a == a' with
      | true => some b'
      | false => lookup a l) =
      some b ↔
    a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
split <;> rename_i h
State after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = true
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l

case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = false
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l

State before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = true
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp at h
State after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : a = a'
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l

State before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : a = a'
⊢ some b' = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
subst a'
State after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ some b' = some b ↔ a = a ∧ b = b' ∨ (a, b) ∈ l

State before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ some b' = some b ↔ a = a ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp [eq_comm]
State after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ b = b' ↔ b = b' ∨ (a, b) ∈ l

State before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
⊢ b = b' ↔ b = b' ∨ (a, b) ∈ l
Tactic:
refine (or_iff_left_of_imp fun h => ?_).symm
State after:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
h : (a, b) ∈ l
⊢ b = b'

State before:
case cons.h_1
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
b' : β
x✝ : Bool
nd : (∀ (a' : α × β), a' ∈ l → ¬a = a'.fst) ∧ NodupKeys l
h : (a, b) ∈ l
⊢ b = b'
Tactic:
cases nd.1 _ h rfl
State after:
no goals

State before:
case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : (a == a') = false
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp at h
State after:
case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : ¬a = a'
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l

State before:
case cons.h_2
α : Type u_1
β : Type u_2
a : α
b : β
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α × β
l : List (α × β)
ih : NodupKeys l → (lookup a l = some b ↔ (a, b) ∈ l)
a' : α
b' : β
nd : (∀ (a'_1 : α × β), a'_1 ∈ l → ¬a' = a'_1.fst) ∧ NodupKeys l
x✝ : Bool
h : ¬a = a'
⊢ lookup a l = some b ↔ a = a' ∧ b = b' ∨ (a, b) ∈ l
Tactic:
simp [h, ih nd.2]
State after:
no goals