-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem mem_replaceF {l : List (α × β)} {x : α × β} {p : α × β → Bool} {f : α × β → β} :
    x ∈ (l.replaceF fun a => bif p a then some (k, f a) else none) → x.1 = k ∨ x ∈ l

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
c✝ : Bool
heq✝ : p a = false
⊢ x = a ∨
      x ∈
        List.replaceF
          (fun a =>
            match p a with
            | true => some (k, f a)
            | false => none)
          l →
    x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
intro
| .inl eq => exact .inr (.inl eq)
| .inr h => exact (ih h).imp_right .inr

Result:
no goals

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
z : Option (α × β)
c✝ : Bool
heq✝ : p a = false
⊢ none = z →
    (x ∈
        match z with
        | none =>
          a ::
            List.replaceF
              (fun a =>
                match p a with
                | true => some (k, f a)
                | false => none)
              l
        | some a => a :: l) →
      x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
intro h

Result:
case cons.h_2
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
z : Option (α × β)
c✝ : Bool
heq✝ : p a = false
h : none = z
⊢ (x ∈
      match z with
      | none =>
        a ::
          List.replaceF
            (fun a =>
              match p a with
              | true => some (k, f a)
              | false => none)
            l
      | some a => a :: l) →
    x.fst = k ∨ x = a ∨ x ∈ l

Proof state:
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
c✝ : Bool
heq✝ : p a = false
x✝ :
  x = a ∨
    x ∈
      List.replaceF
        (fun a =>
          match p a with
          | true => some (k, f a)
          | false => none)
        l
h :
  x ∈
    List.replaceF
      (fun a =>
        match p a with
        | true => some (k, f a)
        | false => none)
      l
⊢ x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
exact (ih h).imp_right .inr

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
z : Option (α × β)
⊢ (match p a with
      | true => some (k, f a)
      | false => none) =
      z →
    (x ∈
        match z with
        | none =>
          a ::
            List.replaceF
              (fun a =>
                match p a with
                | true => some (k, f a)
                | false => none)
              l
        | some a => a :: l) →
      x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
split <;> (intro h; subst h; simp)

Result:
case cons.h_1
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
c✝ : Bool
heq✝ : p a = true
⊢ x = (k, f a) ∨ x ∈ l → x.fst = k ∨ x = a ∨ x ∈ l

case cons.h_2
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
a : α × β
l : List (α × β)
ih : x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) l → x.fst = k ∨ x ∈ l
c✝ : Bool
heq✝ : p a = false
⊢ x = a ∨
      x ∈
        List.replaceF
          (fun a =>
            match p a with
            | true => some (k, f a)
            | false => none)
          l →
    x.fst = k ∨ x = a ∨ x ∈ l