-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
    l.lookup k = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ p ∈ l₁, k != p.1

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true
⊢ (if (k == (k, b).fst) = true then some (k, b).snd else none) = some b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ lookup k l = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true

Tactic:
simp only [lookup_eq_findSome?, findSome?_eq_some_iff]

Result:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ (∃ l₁ a l₂,
      l = l₁ ++ a :: l₂ ∧
        (if (k == a.fst) = true then some a.snd else none) = some b ∧
          ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none) ↔
    ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true

Proof state:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (a_1 : α) (b : β), (a_1, b) ∈ l₁ → ¬a.fst = a_1
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (a.fst, a.snd) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (a.fst != p.fst) = true

Tactic:
exact ⟨l₁, l₂, rfl, by simpa using h₂⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (a_1 : α) (b : β), (a_1, b) ∈ l₁ → ¬a.fst = a_1
⊢ ∀ (p : α × β), p ∈ l₁ → (a.fst != p.fst) = true

Tactic:
simpa using h₂

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none
h₁ : k = a.fst ∧ a.snd = b
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (k, b) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (k != p.fst) = true

Tactic:
obtain ⟨rfl, rfl⟩ := h₁

Result:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (x : α × β), x ∈ l₁ → (if (a.fst == x.fst) = true then some x.snd else none) = none
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (a.fst, a.snd) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (a.fst != p.fst) = true

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true
⊢ ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₁ : (if (k == a.fst) = true then some a.snd else none) = some b
h₂ : ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (k, b) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (k != p.fst) = true

Tactic:
simp only [beq_iff_eq, Option.ite_none_right_eq_some, Option.some.injEq] at h₁

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none
h₁ : k = a.fst ∧ a.snd = b
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (k, b) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (k != p.fst) = true

Proof state:
case mp
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ (∃ l₁ a l₂,
      l = l₁ ++ a :: l₂ ∧
        (if (k == a.fst) = true then some a.snd else none) = some b ∧
          ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none) →
    ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true

Tactic:
rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₁ : (if (k == a.fst) = true then some a.snd else none) = some b
h₂ : ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (k, b) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (k != p.fst) = true

Proof state:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (x : α × β), x ∈ l₁ → (if (a.fst == x.fst) = true then some x.snd else none) = none
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (a.fst, a.snd) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (a.fst != p.fst) = true

Tactic:
simp at h₂

Result:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l₁ : List (α × β)
a : α × β
l₂ : List (α × β)
h₂ : ∀ (a_1 : α) (b : β), (a_1, b) ∈ l₁ → ¬a.fst = a_1
⊢ ∃ l₁_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ (a.fst, a.snd) :: l₂_1 ∧ ∀ (p : α × β), p ∈ l₁_1 → (a.fst != p.fst) = true

Proof state:
case mpr
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ (∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true) →
    ∃ l₁ a l₂,
      l = l₁ ++ a :: l₂ ∧
        (if (k == a.fst) = true then some a.snd else none) = some b ∧
          ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none

Tactic:
rintro ⟨l₁, l₂, rfl, h⟩

Result:
case mpr.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true
⊢ ∃ l₁_1 a l₂_1,
    l₁ ++ (k, b) :: l₂ = l₁_1 ++ a :: l₂_1 ∧
      (if (k == a.fst) = true then some a.snd else none) = some b ∧
        ∀ (x : α × β), x ∈ l₁_1 → (if (k == x.fst) = true then some x.snd else none) = none

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ (∃ l₁ a l₂,
      l = l₁ ++ a :: l₂ ∧
        (if (k == a.fst) = true then some a.snd else none) = some b ∧
          ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none) ↔
    ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ (∃ l₁ a l₂,
      l = l₁ ++ a :: l₂ ∧
        (if (k == a.fst) = true then some a.snd else none) = some b ∧
          ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none) →
    ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true

case mpr
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
b : β
⊢ (∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true) →
    ∃ l₁ a l₂,
      l = l₁ ++ a :: l₂ ∧
        (if (k == a.fst) = true then some a.snd else none) = some b ∧
          ∀ (x : α × β), x ∈ l₁ → (if (k == x.fst) = true then some x.snd else none) = none

Proof state:
case mpr.intro.intro.intro
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true
⊢ ∃ l₁_1 a l₂_1,
    l₁ ++ (k, b) :: l₂ = l₁_1 ++ a :: l₂_1 ∧
      (if (k == a.fst) = true then some a.snd else none) = some b ∧
        ∀ (x : α × β), x ∈ l₁_1 → (if (k == x.fst) = true then some x.snd else none) = none

Tactic:
exact ⟨l₁, (k, b), l₂, rfl, by simp, by simpa using h⟩

Result:
no goals