-- Mathlib/Testing/Plausible/Functions.lean
theorem apply_eq_dlookup (m : List (Σ _ : α, β)) (y : β) (x : α) :
     (withDefault m y).apply x = (m.dlookup x).getD y

Proof state:
case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ ⟨fst, snd⟩.fst ≠ x

Tactic:
simp [heq]

Result:
no goals

Proof state:
case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Tactic:
symm

Result:
case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ ⟨fst, snd⟩.fst ≠ x

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ (withDefault m y).apply x = (List.dlookup x m).getD y

Tactic:
dsimp only [apply]

Result:
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ (Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m)).getD y = (List.dlookup x m).getD y

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ (Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m)).getD y = (List.dlookup x m).getD y

Tactic:
congr 1

Result:
case e_opt
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m

Proof state:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m

Tactic:
simp [heq, ih]

Result:
no goals

Proof state:
case e_opt.cons
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
p : (_ : α) × β
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (p :: m)) = List.dlookup x (p :: m)

Tactic:
rcases p with ⟨fst, snd⟩

Result:
case e_opt.cons.mk
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Proof state:
case e_opt.cons.mk
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Tactic:
by_cases heq : fst = x

Result:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Proof state:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Tactic:
simp [heq]

Result:
no goals

Proof state:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Tactic:
rw [List.dlookup_cons_ne]

Result:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m

case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Proof state:
case e_opt.nil
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 => decide (x_1.fst = x)) []) = List.dlookup x []

Tactic:
simp

Result:
no goals