-- 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_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

Tactic:
intro
| .inl eq => exact eq ▸ .inl rfl
| .inr h => exact .inr (.inr h)

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 (α × β)
⊢ (bif p a then some (k, f a) else none) = z →
    (x ∈
        match z with
        | none => a :: List.replaceF (fun a => bif p a then some (k, f a) else none) l
        | some a => a :: l) →
      x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
unfold cond

Result:
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

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
⊢ x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) (a :: l) → x.fst = k ∨ x ∈ a :: l

Tactic:
simp only [List.replaceF, List.mem_cons]

Result:
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
⊢ (x ∈
      match bif p a then some (k, f a) else none with
      | none => a :: List.replaceF (fun a => bif p a then some (k, f a) else 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 = true
x✝ : x = (k, f a) ∨ x ∈ l
eq : x = (k, f a)
⊢ x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
exact eq ▸ .inl rfl

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
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

Tactic:
subst 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
c✝ : Bool
heq✝ : p a = false
⊢ (x ∈
      match none 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
eq : x = a
⊢ x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
exact .inr (.inl eq)

Result:
no goals

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 = true
x✝ : x = (k, f a) ∨ x ∈ l
h : x ∈ l
⊢ x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
exact .inr (.inr h)

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 (α × β)
e : (bif p a then some (k, f a) else none) = z
⊢ (x ∈
      match z with
      | none => a :: List.replaceF (fun a => bif p a then some (k, f a) else none) l
      | some a => a :: l) →
    x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
revert e

Result:
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 (α × β)
⊢ (bif p a then some (k, f a) else none) = z →
    (x ∈
        match z with
        | none => a :: List.replaceF (fun a => bif p a then some (k, f a) else none) l
        | some a => a :: l) →
      x.fst = k ∨ x = a ∨ 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 ∈
      match none 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:
simp

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
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

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
⊢ (x ∈
      match bif p a then some (k, f a) else none with
      | none => a :: List.replaceF (fun a => bif p a then some (k, f a) else none) l
      | some a => a :: l) →
    x.fst = k ∨ x = a ∨ x ∈ l

Tactic:
generalize e : cond .. = z

Result:
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 (α × β)
e : (bif p a then some (k, f a) else none) = z
⊢ (x ∈
      match z with
      | none => a :: List.replaceF (fun a => bif p a then some (k, f a) else none) l
      | some a => a :: l) →
    x.fst = k ∨ x = a ∨ x ∈ l

Proof state:
case nil
α : Type u_1
β : Type u_2
k : α
x : α × β
p : α × β → Bool
f : α × β → β
⊢ x ∈ List.replaceF (fun a => bif p a then some (k, f a) else none) [] → x.fst = k ∨ x ∈ []

Tactic:
exact .inr

Result:
no goals