no goals
case nil
α : Type u_1
β : Type u_2
k : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
f : α × β → β
H : List.Pairwise (fun a b => ¬(a.fst == b.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) [])
simp [H]
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)
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 : List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (a :: 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) (a :: l))
simp at H ⊢
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)
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)
generalize e : cond .. = z
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)
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)
unfold cond at e
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)
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)
revert e
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)
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)
split <;> (intro h; subst h; simp)
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)
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)
intro h
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
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (match none with
    | none => a :: List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
    | some a => a :: 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
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)
subst h
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)
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
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (match none with
    | none => a :: List.replaceF (fun a => bif a.fst == k then some (k, f a) else none) l
    | some a => a :: l)
simp
no goals
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)
next e =>
refine ⟨fun a h => ?_, ih H.2⟩
match mem_replaceF h with
| .inl eq => exact eq ▸ ne_true_of_eq_false e
| .inr h => exact H.1 a h
α : 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
α : 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)
refine ⟨fun a h => ?_, ih H.2⟩
no goals
α : 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
match mem_replaceF h with
| .inl eq => exact eq ▸ ne_true_of_eq_false e
| .inr h => exact H.1 a h
no goals
α : 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
exact eq ▸ ne_true_of_eq_false e
no goals
α : 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
h : a ∈ l
⊢ ¬(a✝.fst == a.fst) = true
exact H.1 a h