-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
    (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).length = if containsKey k l = true then l.length - 1 else l.length

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
⊢ (eraseKey k []).length = if containsKey k [] = true then [].length - 1 else [].length

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : (eraseKey k tail✝).length = if containsKey k tail✝ = true then tail✝.length - 1 else tail✝.length
⊢ (eraseKey k (⟨k✝, v✝⟩ :: tail✝)).length =
    if containsKey k (⟨k✝, v✝⟩ :: tail✝) = true then (⟨k✝, v✝⟩ :: tail✝).length - 1 else (⟨k✝, v✝⟩ :: tail✝).length

Proof state:
case false.false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = false
⊢ (if false = true then t.length - 1 else t.length) + 1 =
    if false = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
simp

Result:
no goals

Proof state:
case false.true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = true
⊢ t.length - 1 + 1 = t.length

Tactic:
rw [Nat.sub_add_cancel]

Result:
case false.true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = true
⊢ 1 ≤ t.length

Proof state:
case false.true.cons
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih :
  (eraseKey k (head✝ :: tail✝)).length =
    if containsKey k (head✝ :: tail✝) = true then (head✝ :: tail✝).length - 1 else (head✝ :: tail✝).length
h : containsKey k (head✝ :: tail✝) = true
⊢ 1 ≤ (head✝ :: tail✝).length

Tactic:
simp

Result:
no goals

Proof state:
case false.true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = true
⊢ (if true = true then t.length - 1 else t.length) + 1 =
    if true = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
simp only [Nat.succ_eq_add_one, List.length_cons, Nat.add_sub_cancel, if_true]

Result:
case false.true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = true
⊢ t.length - 1 + 1 = t.length

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (bif k' == k then t else ⟨k', v'⟩ :: eraseKey k t).length =
    if (k' == k || containsKey k t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
cases k' == k

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (bif false then t else ⟨k', v'⟩ :: eraseKey k t).length =
    if (false || containsKey k t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

case true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (bif true then t else ⟨k', v'⟩ :: eraseKey k t).length =
    if (true || containsKey k t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Proof state:
case false.true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = true
⊢ 1 ≤ t.length

Tactic:
cases t

Result:
case false.true.nil
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
ih : (eraseKey k []).length = if containsKey k [] = true then [].length - 1 else [].length
h : containsKey k [] = true
⊢ 1 ≤ [].length

case false.true.cons
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
ih :
  (eraseKey k (head✝ :: tail✝)).length =
    if containsKey k (head✝ :: tail✝) = true then (head✝ :: tail✝).length - 1 else (head✝ :: tail✝).length
h : containsKey k (head✝ :: tail✝) = true
⊢ 1 ≤ (head✝ :: tail✝).length

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (bif true then t else ⟨k', v'⟩ :: eraseKey k t).length =
    if (true || containsKey k t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (eraseKey k (⟨k', v'⟩ :: t)).length =
    if containsKey k (⟨k', v'⟩ :: t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
rw [eraseKey_cons, containsKey_cons]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (bif k' == k then t else ⟨k', v'⟩ :: eraseKey k t).length =
    if (k' == k || containsKey k t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (bif false then t else ⟨k', v'⟩ :: eraseKey k t).length =
    if (false || containsKey k t) = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
rw [cond_false, Bool.false_or, List.length_cons, ih]

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (if containsKey k t = true then t.length - 1 else t.length) + 1 =
    if containsKey k t = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
⊢ (eraseKey k []).length = if containsKey k [] = true then [].length - 1 else [].length

Tactic:
simp

Result:
no goals

Proof state:
case false.true.nil
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
ih : (eraseKey k []).length = if containsKey k [] = true then [].length - 1 else [].length
h : containsKey k [] = true
⊢ 1 ≤ [].length

Tactic:
simp at h

Result:
no goals