-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertList [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)}
    {k : α} : containsKey k (List.insertList l toInsert) =
    (containsKey k l || (toInsert.map Sigma.fst).contains k)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (containsKey k l || k == hd.fst || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (k == hd.fst || (List.map Sigma.fst tl).contains k))

Tactic:
rw [Bool.or_assoc]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
⊢ containsKey k (insertList l toInsert) = (containsKey k l || (List.map Sigma.fst toInsert).contains k)

Tactic:
induction toInsert generalizing l with
| nil =>  simp only [insertList, List.map_nil, List.elem_nil, Bool.or_false]
| cons hd tl ih =>
  unfold insertList
  rw [ih]
  rw [containsKey_insertEntry]
  simp only [Bool.or_eq_true, List.map_cons, List.contains_cons]
  rw [BEq.comm]
  conv => left; left; rw [Bool.or_comm]
  rw [Bool.or_assoc]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (containsKey k (insertEntry hd.fst hd.snd l) || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Tactic:
rw [containsKey_insertEntry]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (hd.fst == k || containsKey k l || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (hd.fst == k || containsKey k l || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (k == hd.fst || (List.map Sigma.fst tl).contains k))

Tactic:
rw [BEq.comm]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (k == hd.fst || containsKey k l || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (k == hd.fst || (List.map Sigma.fst tl).contains k))

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ containsKey k (insertList (insertEntry hd.fst hd.snd l) tl) =
    (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Tactic:
rw [ih]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (containsKey k (insertEntry hd.fst hd.snd l) || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (hd.fst == k || containsKey k l || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Tactic:
simp only [Bool.or_eq_true, List.map_cons, List.contains_cons]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (hd.fst == k || containsKey k l || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (k == hd.fst || (List.map Sigma.fst tl).contains k))

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
l : List ((a : α) × β a)
⊢ containsKey k (insertList l []) = (containsKey k l || (List.map Sigma.fst []).contains k)

Tactic:
simp only [insertList, List.map_nil, List.elem_nil, Bool.or_false]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ containsKey k (insertList l (hd :: tl)) = (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Tactic:
unfold insertList

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ containsKey k (insertList (insertEntry hd.fst hd.snd l) tl) =
    (containsKey k l || (List.map Sigma.fst (hd :: tl)).contains k)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (k == hd.fst || containsKey k l || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (k == hd.fst || (List.map Sigma.fst tl).contains k))

Tactic:
conv => left; left; rw [Bool.or_comm]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {l : List ((a : α) × β a)},
    containsKey k (insertList l tl) = (containsKey k l || (List.map Sigma.fst tl).contains k)
l : List ((a : α) × β a)
⊢ (containsKey k l || k == hd.fst || (List.map Sigma.fst tl).contains k) =
    (containsKey k l || (k == hd.fst || (List.map Sigma.fst tl).contains k))