Theorem: List.nodupkeys_eq_of_fst_eq (LeanSAT/Util/Nodupkeys.lean)

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
⊢ s.fst = s'.fst → s = s'
Tactic:
intro keys_eq
State after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ s = s'

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ s = s'
Tactic:
have goal_rw : (s = s') = (s.1 = s'.1 ∧ s.2 = s'.2) := by
  have s_rw : s = (s.1, s.2) := rfl
  have s'_rw : s' = (s'.1, s'.2) := rfl
  rw [s_rw, s'_rw]
  simp only [Prod.mk.injEq]
State after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s = s'

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s = s'
Tactic:
rw [goal_rw]
State after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst ∧ s.snd = s'.snd

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst ∧ s.snd = s'.snd
Tactic:
constructor
State after:
case left
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst

case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd

State before:
case left
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst

case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Tactic:
. exact keys_eq
State after:
case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd

State before:
case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Tactic:
. induction l with
  | nil => exact False.elim $ List.not_mem_nil s h
  | cons hd tl ih =>
    rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
    simp only [List.map_eq_nil, ne_eq] at nd
    rcases nd with l_eq_nil | ⟨a, l', nd⟩
    . exact False.elim l_eq_nil
    . rw [List.Nodupkeys, List.Nodup] at ih
      rcases nd with ⟨nd1, nd2, nd3⟩
      rw [List.map_cons] at nd3
      simp only [List.cons.injEq] at nd3
      rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
      rw [← nd3] at nd2
      specialize ih nd2
      rw [List.mem_cons] at h h'
      rcases h with s_eq_hd | s_in_tl
      . rcases h' with s'_eq_hd | s'_in_tl
        . rw [s_eq_hd, s'_eq_hd]
        . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
          specialize nd1 s'.1
          simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
            forall_exists_index] at nd1
          specialize nd1 s'.2 s'_in_tl
          exfalso
          exact nd1 keys_eq
      . rcases h' with s'_eq_hd | s'_in_tl
        . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
          specialize nd1 s.1
          simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
            forall_exists_index] at nd1
          specialize nd1 s.2 s_in_tl
          exfalso
          exact nd1 keys_eq.symm
        . exact ih s_in_tl s'_in_tl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Tactic:
have s_rw : s = (s.1, s.2) := rfl
State after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Tactic:
have s'_rw : s' = (s'.1, s'.2) := rfl
State after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Tactic:
rw [s_rw, s'_rw]
State after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ ((s.fst, s.snd) = (s'.fst, s'.snd)) =
    ((s.fst, s.snd).fst = (s'.fst, s'.snd).fst ∧ (s.fst, s.snd).snd = (s'.fst, s'.snd).snd)

State before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ ((s.fst, s.snd) = (s'.fst, s'.snd)) =
    ((s.fst, s.snd).fst = (s'.fst, s'.snd).fst ∧ (s.fst, s.snd).snd = (s'.fst, s'.snd).snd)
Tactic:
simp only [Prod.mk.injEq]
State after:
no goals

State before:
case left
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst
Tactic:
exact keys_eq
State after:
no goals

State before:
case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Tactic:
induction l with
| nil => exact False.elim $ List.not_mem_nil s h
| cons hd tl ih =>
  rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
  simp only [List.map_eq_nil, ne_eq] at nd
  rcases nd with l_eq_nil | ⟨a, l', nd⟩
  . exact False.elim l_eq_nil
  . rw [List.Nodupkeys, List.Nodup] at ih
    rcases nd with ⟨nd1, nd2, nd3⟩
    rw [List.map_cons] at nd3
    simp only [List.cons.injEq] at nd3
    rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
    rw [← nd3] at nd2
    specialize ih nd2
    rw [List.mem_cons] at h h'
    rcases h with s_eq_hd | s_in_tl
    . rcases h' with s'_eq_hd | s'_in_tl
      . rw [s_eq_hd, s'_eq_hd]
      . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
        specialize nd1 s'.1
        simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
          forall_exists_index] at nd1
        specialize nd1 s'.2 s'_in_tl
        exfalso
        exact nd1 keys_eq
    . rcases h' with s'_eq_hd | s'_in_tl
      . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
        specialize nd1 s.1
        simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
          forall_exists_index] at nd1
        specialize nd1 s.2 s_in_tl
        exfalso
        exact nd1 keys_eq.symm
      . exact ih s_in_tl s'_in_tl
State after:
no goals

State before:
case right.nil
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
nd : [].Nodupkeys
h : s ∈ []
h' : s' ∈ []
⊢ s.snd = s'.snd
Tactic:
exact False.elim $ List.not_mem_nil s h
State after:
no goals

State before:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
nd : (hd :: tl).Nodupkeys
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
⊢ s.snd = s'.snd
Tactic:
rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
State after:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
nd :
  map (fun x => x.fst) (hd :: tl) = [] ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → a ≠ a') ∧ Pairwise (fun x x_1 => x ≠ x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
⊢ s.snd = s'.snd

State before:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
nd :
  map (fun x => x.fst) (hd :: tl) = [] ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → a ≠ a') ∧ Pairwise (fun x x_1 => x ≠ x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
⊢ s.snd = s'.snd
Tactic:
simp only [List.map_eq_nil, ne_eq] at nd
State after:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
nd :
  False ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → ¬a = a') ∧
          Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd

State before:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
nd :
  False ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → ¬a = a') ∧
          Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
rcases nd with l_eq_nil | ⟨a, l', nd⟩
State after:
case right.cons.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
l_eq_nil : False
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd

State before:
case right.cons.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
l_eq_nil : False
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
. exact False.elim l_eq_nil
State after:
case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
. rw [List.Nodupkeys, List.Nodup] at ih
  rcases nd with ⟨nd1, nd2, nd3⟩
  rw [List.map_cons] at nd3
  simp only [List.cons.injEq] at nd3
  rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
  rw [← nd3] at nd2
  specialize ih nd2
  rw [List.mem_cons] at h h'
  rcases h with s_eq_hd | s_in_tl
  . rcases h' with s'_eq_hd | s'_in_tl
    . rw [s_eq_hd, s'_eq_hd]
    . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
      specialize nd1 s'.1
      simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
        forall_exists_index] at nd1
      specialize nd1 s'.2 s'_in_tl
      exfalso
      exact nd1 keys_eq
  . rcases h' with s'_eq_hd | s'_in_tl
    . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
      specialize nd1 s.1
      simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
        forall_exists_index] at nd1
      specialize nd1 s.2 s_in_tl
      exfalso
      exact nd1 keys_eq.symm
    . exact ih s_in_tl s'_in_tl
State after:
no goals

State before:
case right.cons.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
l_eq_nil : False
⊢ s.snd = s'.snd
Tactic:
exact False.elim l_eq_nil
State after:
no goals

State before:
case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
rw [List.Nodupkeys, List.Nodup] at ih
State after:
case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
rcases nd with ⟨nd1, nd2, nd3⟩
State after:
case right.cons.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
nd3 : map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
nd3 : map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
rw [List.map_cons] at nd3
State after:
case right.cons.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
nd3 : hd.fst :: map (fun x => x.fst) tl = a :: l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
nd3 : hd.fst :: map (fun x => x.fst) tl = a :: l'
⊢ s.snd = s'.snd
Tactic:
simp only [List.cons.injEq] at nd3
State after:
case right.cons.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
nd3 : hd.fst = a ∧ map (fun x => x.fst) tl = l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
nd3 : hd.fst = a ∧ map (fun x => x.fst) tl = l'
⊢ s.snd = s'.snd
Tactic:
rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
State after:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) l'
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
⊢ s.snd = s'.snd
Tactic:
rw [← nd3] at nd2
State after:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : Pairwise (fun x x_1 => x ≠ x_1) (map (fun x => x.fst) tl) → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
⊢ s.snd = s'.snd
Tactic:
specialize ih nd2
State after:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
⊢ s.snd = s'.snd
Tactic:
rw [List.mem_cons] at h h'
State after:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h : s = hd ∨ s ∈ tl
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h : s = hd ∨ s ∈ tl
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
⊢ s.snd = s'.snd
Tactic:
rcases h with s_eq_hd | s_in_tl
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
⊢ s.snd = s'.snd
Tactic:
. rcases h' with s'_eq_hd | s'_in_tl
  . rw [s_eq_hd, s'_eq_hd]
  . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
    specialize nd1 s'.1
    simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
      forall_exists_index] at nd1
    specialize nd1 s'.2 s'_in_tl
    exfalso
    exact nd1 keys_eq
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
⊢ s.snd = s'.snd
Tactic:
. rcases h' with s'_eq_hd | s'_in_tl
  . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
    specialize nd1 s.1
    simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
      forall_exists_index] at nd1
    specialize nd1 s.2 s_in_tl
    exfalso
    exact nd1 keys_eq.symm
  . exact ih s_in_tl s'_in_tl
State after:
no goals

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
⊢ s.snd = s'.snd
Tactic:
rcases h' with s'_eq_hd | s'_in_tl
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
. rw [s_eq_hd, s'_eq_hd]
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
. rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
  specialize nd1 s'.1
  simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
    forall_exists_index] at nd1
  specialize nd1 s'.2 s'_in_tl
  exfalso
  exact nd1 keys_eq
State after:
no goals

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd
Tactic:
rw [s_eq_hd, s'_eq_hd]
State after:
no goals

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
specialize nd1 s'.1
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : s'.fst ∈ map (fun x => x.fst) tl → ¬s.fst = s'.fst
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : s'.fst ∈ map (fun x => x.fst) tl → ¬s.fst = s'.fst
⊢ s.snd = s'.snd
Tactic:
simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
  forall_exists_index] at nd1
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ∀ (x : β), (s'.fst, x) ∈ tl → ¬s.fst = s'.fst
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ∀ (x : β), (s'.fst, x) ∈ tl → ¬s.fst = s'.fst
⊢ s.snd = s'.snd
Tactic:
specialize nd1 s'.2 s'_in_tl
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ s.snd = s'.snd
Tactic:
exfalso
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ False

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ False
Tactic:
exact nd1 keys_eq
State after:
no goals

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
⊢ s.snd = s'.snd
Tactic:
rcases h' with s'_eq_hd | s'_in_tl
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
. rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
  specialize nd1 s.1
  simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
    forall_exists_index] at nd1
  specialize nd1 s.2 s_in_tl
  exfalso
  exact nd1 keys_eq.symm
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
. exact ih s_in_tl s'_in_tl
State after:
no goals

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd
Tactic:
rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s'.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s'.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd
Tactic:
specialize nd1 s.1
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : s.fst ∈ map (fun x => x.fst) tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : s.fst ∈ map (fun x => x.fst) tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Tactic:
simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
  forall_exists_index] at nd1
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ∀ (x : β), (s.fst, x) ∈ tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ∀ (x : β), (s.fst, x) ∈ tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Tactic:
specialize nd1 s.2 s_in_tl
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ s.snd = s'.snd

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Tactic:
exfalso
State after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ False

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ False
Tactic:
exact nd1 keys_eq.symm
State after:
no goals

State before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
exact ih s_in_tl s'_in_tl
State after:
no goals