-- 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
z : Option (α × β)
e :
  (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:
revert e

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 (α × β)
⊢ (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)

Proof state:
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
z : Option (α × β)
c✝ : Bool
heq✝ : (a.fst == k) = 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:
intro h

Result:
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
z : Option (α × β)
c✝ : Bool
heq✝ : (a.fst == k) = false
h : 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 (α × β)
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)

Tactic:
unfold cond at e

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 :
  (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)

Proof state:
α : 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
e : (a✝.fst == k) = false
a : α × β
h : a ∈ List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
eq : a.fst = k
⊢ ¬(a✝.fst == a.fst) = true

Tactic:
exact eq ▸ ne_true_of_eq_false e

Result:
no goals

Proof state:
α : 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
e : (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)

Tactic:
refine ⟨fun a h => ?_, ih H.2⟩

Result:
α : 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
e : (a✝.fst == k) = false
a : α × β
h : a ∈ List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
⊢ ¬(a✝.fst == a.fst) = true