Theorem: List.Perm.lookup_eq (Lean4Lean/Std/NodupKeys.lean)

State before:
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
h : l₁ ~ l₂
nd : NodupKeys l₁
⊢ lookup a l₁ = lookup a l₂
Tactic:
induction h with
| nil => rfl
| cons _ _ ih => simp [lookup]; split <;> [rfl; exact ih (pairwise_cons.1 nd).2]
| swap _ h ih =>
  simp at nd
  simp [lookup]; split <;> split <;> rename_i h1 _ h2 <;> try rfl
  simp at h1 h2; cases nd.1.1 (by rw [← h1, h2])
| trans h1 _ ih1 ih2 => exact (ih1 nd).trans (ih2 (h1.nodupKeys_iff.1 nd))
State after:
no goals

State before:
case nil
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
nd : NodupKeys []
⊢ lookup a [] = lookup a []
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ : α × β
l₁✝ l₂✝ : List (α × β)
a✝ : l₁✝ ~ l₂✝
ih : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
nd : NodupKeys (x✝ :: l₁✝)
⊢ lookup a (x✝ :: l₁✝) = lookup a (x✝ :: l₂✝)
Tactic:
simp [lookup]
State after:
case cons
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ : α × β
l₁✝ l₂✝ : List (α × β)
a✝ : l₁✝ ~ l₂✝
ih : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
nd : NodupKeys (x✝ :: l₁✝)
⊢ (match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₁✝) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₂✝

State before:
case cons
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ : α × β
l₁✝ l₂✝ : List (α × β)
a✝ : l₁✝ ~ l₂✝
ih : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
nd : NodupKeys (x✝ :: l₁✝)
⊢ (match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₁✝) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false => lookup a l₂✝
Tactic:
split <;> [rfl; exact ih (pairwise_cons.1 nd).2]
State after:
no goals

State before:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd : NodupKeys (h :: x✝ :: ih)
⊢ lookup a (h :: x✝ :: ih) = lookup a (x✝ :: h :: ih)
Tactic:
simp at nd
State after:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ lookup a (h :: x✝ :: ih) = lookup a (x✝ :: h :: ih)

State before:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ lookup a (h :: x✝ :: ih) = lookup a (x✝ :: h :: ih)
Tactic:
simp [lookup]
State after:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ (match a == h.fst with
    | true => some h.snd
    | false =>
      match a == x✝.fst with
      | true => some x✝.snd
      | false => lookup a ih) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false =>
      match a == h.fst with
      | true => some h.snd
      | false => lookup a ih

State before:
case swap
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝ h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝.fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝.fst = a'.fst) ∧ NodupKeys ih
⊢ (match a == h.fst with
    | true => some h.snd
    | false =>
      match a == x✝.fst with
      | true => some x✝.snd
      | false => lookup a ih) =
    match a == x✝.fst with
    | true => some x✝.snd
    | false =>
      match a == h.fst with
      | true => some h.snd
      | false => lookup a ih
Tactic:
split <;> split <;> rename_i h1 _ h2 <;> try rfl
State after:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ : Bool
h1 : (a == h.fst) = true
x✝ : Bool
h2 : (a == x✝².fst) = true
⊢ some h.snd = some x✝².snd

State before:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ : Bool
h1 : (a == h.fst) = true
x✝ : Bool
h2 : (a == x✝².fst) = true
⊢ some h.snd = some x✝².snd
Tactic:
simp at h1 h2
State after:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ x✝ : Bool
h1 : a = h.fst
h2 : a = x✝².fst
⊢ some h.snd = some x✝².snd

State before:
case swap.h_1.h_1
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ x✝ : Bool
h1 : a = h.fst
h2 : a = x✝².fst
⊢ some h.snd = some x✝².snd
Tactic:
cases nd.1.1 (by rw [← h1, h2])
State after:
no goals

State before:
case swap.h_2.h_2
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ : Bool
h1 : (a == h.fst) = false
x✝ : Bool
h2 : (a == x✝².fst) = false
⊢ lookup a ih = lookup a ih
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
x✝² h : α × β
ih : List (α × β)
nd :
  (¬h.fst = x✝².fst ∧ ∀ (a : α × β), a ∈ ih → ¬h.fst = a.fst) ∧
    (∀ (a' : α × β), a' ∈ ih → ¬x✝².fst = a'.fst) ∧ NodupKeys ih
x✝¹ x✝ : Bool
h1 : a = h.fst
h2 : a = x✝².fst
⊢ h.fst = x✝².fst
Tactic:
rw [← h1, h2]
State after:
no goals

State before:
case trans
α : Type u_1
β : Type u_2
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List (α × β)
l₁✝ l₂✝ l₃✝ : List (α × β)
h1 : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : NodupKeys l₁✝ → lookup a l₁✝ = lookup a l₂✝
ih2 : NodupKeys l₂✝ → lookup a l₂✝ = lookup a l₃✝
nd : NodupKeys l₁✝
⊢ lookup a l₁✝ = lookup a l₃✝
Tactic:
exact (ih1 nd).trans (ih2 (h1.nodupKeys_iff.1 nd))
State after:
no goals