-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertList [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)) (k : α) :
    getEntry? k (insertList l toInsert) = (getEntry? k toInsert).or (getEntry? k l)

Proof state:
case cons.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = true
⊢ (if true = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l t)) =
    (getEntry? k (h :: t)).or (getEntry? k l)

Tactic:
simp only [↓reduceIte]

Result:
case cons.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = true
⊢ some ⟨h.fst, h.snd⟩ = (getEntry? k (h :: t)).or (getEntry? k l)

Proof state:
case cons.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = false
⊢ (if false = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l t)) =
    (getEntry? k (h :: t)).or (getEntry? k l)

Tactic:
simp only [Bool.false_eq_true, ↓reduceIte]

Result:
case cons.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = false
⊢ getEntry? k (insertList l t) = (getEntry? k (h :: t)).or (getEntry? k l)

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) []
⊢ getEntry? k (insertList l []) = (getEntry? k []).or (getEntry? k l)

Tactic:
simp [insertList]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
⊢ (if (h.fst == k) = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l t)) =
    (getEntry? k (h :: t)).or (getEntry? k l)

Tactic:
cases hk : h.1 == k

Result:
case cons.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = false
⊢ (if false = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l t)) =
    (getEntry? k (h :: t)).or (getEntry? k l)

case cons.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = true
⊢ (if true = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l t)) =
    (getEntry? k (h :: t)).or (getEntry? k l)

Proof state:
case cons.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = false
⊢ getEntry? k (insertList l t) = (getEntry? k (h :: t)).or (getEntry? k l)

Tactic:
rw [ih distinct_l distinct_toInsert.tail, getEntry?_cons_of_false hk]

Result:
no goals

Proof state:
case cons.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
hk : (h.fst == k) = true
⊢ some ⟨h.fst, h.snd⟩ = (getEntry? k (h :: t)).or (getEntry? k l)

Tactic:
rw [getEntry?_cons_of_true hk, Option.some_or]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
⊢ getEntry? k (insertList l (h :: t)) = (getEntry? k (h :: t)).or (getEntry? k l)

Tactic:
rw [getEntry?_of_perm distinct_l.insertList
  (insertList_cons_perm distinct_l (DistinctKeys.def.2 distinct_toInsert)),
  getEntry?_insertEntry]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    DistinctKeys l →
      List.Pairwise (fun a b => (a.fst == b.fst) = false) t →
        getEntry? k (insertList l t) = (getEntry? k t).or (getEntry? k l)
l : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) (h :: t)
⊢ (if (h.fst == k) = true then some ⟨h.fst, h.snd⟩ else getEntry? k (insertList l t)) =
    (getEntry? k (h :: t)).or (getEntry? k l)