-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem pairwise_replaceF [BEq α] [PartialEquivBEq α]
    {l : List (α × β)} {f : α × β → β}
    (H : l.Pairwise fun a b => ¬(a.fst == b.fst)) :
    (l.replaceF fun a => bif a.fst == k then some (k, f a) else none)
      |>.Pairwise fun a b => ¬(a.fst == b.fst)

Proof state:
case cons
α : Type u_1
β : Type u_2
k : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
f : α × β → β
a : α × β
l : List (α × β)
ih :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l →
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)
H : (∀ (a' : α × β), a' ∈ l → ¬(a.fst == a'.fst) = true) ∧ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (match bif a.fst == k then some (k, f a) else none with
    | none => a :: List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
    | some a => a :: l)

Tactic:
generalize e : cond .. = z

Result:
case cons
α : Type u_1
β : Type u_2
k : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
f : α × β → β
a : α × β
l : List (α × β)
ih :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l →
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)
H : (∀ (a' : α × β), a' ∈ l → ¬(a.fst == a'.fst) = true) ∧ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l
z : Option (α × β)
e : (bif a.fst == k then some (k, f a) else none) = z
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (match z with
    | none => a :: List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
    | some a => a :: l)

Proof state:
case cons
α : Type u_1
β : Type u_2
k : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
f : α × β → β
a : α × β
l : List (α × β)
ih :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l →
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)
H : (∀ (a' : α × β), a' ∈ l → ¬(a.fst == a'.fst) = true) ∧ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l
z : Option (α × β)
⊢ (match a.fst == k with
      | true => some (k, f a)
      | false => none) =
      z →
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (match z with
      | none => a :: List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
      | some a => a :: l)

Tactic:
split <;> (intro h; subst h; simp only [List.pairwise_cons])

Result:
case cons.h_1
α : Type u_1
β : Type u_2
k : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
f : α × β → β
a : α × β
l : List (α × β)
ih :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l →
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)
H : (∀ (a' : α × β), a' ∈ l → ¬(a.fst == a'.fst) = true) ∧ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l
c✝ : Bool
heq✝ : (a.fst == k) = true
⊢ (∀ (a' : α × β), a' ∈ l → ¬(k == a'.fst) = true) ∧ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l

case cons.h_2
α : Type u_1
β : Type u_2
k : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
f : α × β → β
a : α × β
l : List (α × β)
ih :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l →
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)
H : (∀ (a' : α × β), a' ∈ l → ¬(a.fst == a'.fst) = true) ∧ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l
c✝ : Bool
heq✝ : (a.fst == k) = false
⊢ (∀ (a' : α × β),
      a' ∈ List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l → ¬(a.fst == a'.fst) = true) ∧
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
      (List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l)