[GOAL]
α : Type u
β : α → Type v
l₁ : List (Sigma β)
h₁ : NodupKeys l₁
l₂ : List (Sigma β)
nodupKeys✝ : NodupKeys l₂
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs = ys)
[PROOFSTEP]
rw [ext_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs.entries = ys.entries)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
⊢ keys s₁ ⊆ keys s₂
[PROOFSTEP]
intro k hk
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
⊢ k ∈ keys s₂
[PROOFSTEP]
letI : DecidableEq α := Classical.decEq α
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this : DecidableEq α := Classical.decEq α
⊢ k ∈ keys s₂
[PROOFSTEP]
have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this✝ : DecidableEq α := Classical.decEq α
this : { fst := k, snd := Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true) } ∈ s₂.entries
⊢ k ∈ keys s₂
[PROOFSTEP]
rw [← mem_lookup_iff, Option.mem_def] at this
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this✝¹ : DecidableEq α := Classical.decEq α
this✝ : { fst := k, snd := Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true) } ∈ s₂.entries
this : lookup k s₂ = some (Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true))
⊢ k ∈ keys s₂
[PROOFSTEP]
rw [← mem_keys, ← lookup_isSome, this]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ keys s₁
this✝¹ : DecidableEq α := Classical.decEq α
this✝ : { fst := k, snd := Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true) } ∈ s₂.entries
this : lookup k s₂ = some (Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true))
⊢ Option.isSome (some (Option.get (lookup k s₁) (_ : Option.isSome (lookup k s₁) = true))) = true
[PROOFSTEP]
exact Option.isSome_some
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s : AList β
⊢ a' ∈ replace a b s ↔ a' ∈ s
[PROOFSTEP]
rw [mem_keys, keys_replace, ← mem_keys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s
[PROOFSTEP]
rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert a b s).entries = { fst := a, snd := b } :: s.entries
[PROOFSTEP]
rw [insert_entries, kerase_of_not_mem_keys h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ keys (insert a b s) = a :: List.erase (keys s) a
[PROOFSTEP]
simp [insert, keys, keys_kerase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ (insert a b s₁).entries ~ (insert a b s₂).entries
[PROOFSTEP]
simp only [insert_entries]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ { fst := a, snd := b } :: kerase a s₁.entries ~ { fst := a, snd := b } :: kerase a s₂.entries
[PROOFSTEP]
exact p.kinsert s₁.nodupKeys
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ lookup a (insert a b s) = some b
[PROOFSTEP]
simp only [lookup, insert, dlookup_kinsert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a (toAList s) = dlookup a s
[PROOFSTEP]
rw [List.toAList, lookup, dlookup_dedupKeys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ insert a b' (insert a b s) = insert a b' s
[PROOFSTEP]
ext : 1
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
[PROOFSTEP]
simp only [AList.insert_entries, List.kerase_cons_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ (insert a' b' (insert a b s)).entries ~ (insert a b (insert a' b' s)).entries
[PROOFSTEP]
simp only [insert_entries]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ { fst := a', snd := b' } :: kerase a' ({ fst := a, snd := b } :: kerase a s.entries) ~
    { fst := a, snd := b } :: kerase a ({ fst := a', snd := b' } :: kerase a' s.entries)
[PROOFSTEP]
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;> [apply Perm.swap; exact h; exact h.symm]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ { fst := a', snd := b' } :: kerase a' ({ fst := a, snd := b } :: kerase a s.entries) ~
    { fst := a, snd := b } :: kerase a ({ fst := a', snd := b' } :: kerase a' s.entries)
[PROOFSTEP]
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ { fst := a', snd := b' } :: { fst := a, snd := b } :: kerase a (kerase a' s.entries) ~
    { fst := a, snd := b } :: { fst := a', snd := b' } :: kerase a (kerase a' s.entries)
[PROOFSTEP]
apply Perm.swap
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a ≠ { fst := a', snd := b' }.fst
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ a' ≠ { fst := a, snd := b }.fst
[PROOFSTEP]
exact h.symm
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ (insert a b (singleton a b')).entries = (singleton a b).entries
[PROOFSTEP]
simp only [AList.insert_entries, List.kerase_cons_eq, and_self_iff, AList.singleton_entries, heq_iff_eq,
  eq_self_iff_true]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : NodupKeys (c :: l)
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) }
[PROOFSTEP]
simpa [insert] using (kerase_of_not_mem_keys <| not_mem_keys_of_nodupKeys_cons h).symm
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
h : NodupKeys (c :: l)
⊢ C { entries := c :: l, nodupKeys := h }
[PROOFSTEP]
rw [mk_cons_eq_insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
h : NodupKeys (c :: l)
⊢ C (insert c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) })
[PROOFSTEP]
refine' IH _ _ _ _ (insertRec H0 IH _)
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
h : NodupKeys (c :: l)
⊢ ¬c.fst ∈ { entries := l, nodupKeys := (_ : NodupKeys l) }
[PROOFSTEP]
exact not_mem_keys_of_nodupKeys_cons h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
⊢ True
[PROOFSTEP]
induction l using AList.insertRec
[GOAL]
case H0
α : Type u
β : α → Type v
inst✝ : DecidableEq α
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case IH
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a✝² : α
b✝ : β a✝²
l✝ : AList β
a✝¹ : ¬a✝² ∈ l✝
a✝ : True
⊢ True
[PROOFSTEP]
trivial
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
⊢ insertRec H0 IH ∅ = H0
[PROOFSTEP]
change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
⊢ insertRec H0 IH { entries := [], nodupKeys := (_ : NodupKeys []) } = H0
[PROOFSTEP]
rw [insertRec]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : AList β
h : ¬c.fst ∈ l
⊢ insertRec H0 IH (insert c.fst c.snd l) = IH c.fst c.snd l h (insertRec H0 IH l)
[PROOFSTEP]
cases' l with l hl
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
[PROOFSTEP]
suffices
  HEq (@insertRec α β _ C H0 IH ⟨c :: l, nodupKeys_cons.2 ⟨h, hl⟩⟩)
    (IH c.1 c.2 ⟨l, hl⟩ h (@insertRec α β _ C H0 IH ⟨l, hl⟩))
  by
  cases c
  apply eq_of_heq
  convert this <;> rw [insert_of_neg h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq (insertRec H0 IH { entries := c :: l, nodupKeys := (_ : NodupKeys (c :: l)) })
    (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
[PROOFSTEP]
cases c
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ insertRec H0 IH
      (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }) =
    IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case mk.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ HEq
    (insertRec H0 IH
      (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }))
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
[PROOFSTEP]
convert this
[GOAL]
case h.e'_1.h.e'_1.h.e'_3.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
⊢ (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }).entries =
    { fst := fst✝, snd := snd✝ } :: l
[PROOFSTEP]
rw [insert_of_neg h]
[GOAL]
case h.e'_2.e'_7.h.e'_3.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
l : List (Sigma β)
hl : NodupKeys l
fst✝ : α
snd✝ : β fst✝
h : ¬{ fst := fst✝, snd := snd✝ }.fst ∈ { entries := l, nodupKeys := hl }
this :
  HEq
    (insertRec H0 IH
      { entries := { fst := fst✝, snd := snd✝ } :: l,
        nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) })
    (IH { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl }))
e_1✝ :
  C (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }) =
    C { entries := { fst := fst✝, snd := snd✝ } :: l, nodupKeys := (_ : NodupKeys ({ fst := fst✝, snd := snd✝ } :: l)) }
⊢ (insert { fst := fst✝, snd := snd✝ }.fst { fst := fst✝, snd := snd✝ }.snd { entries := l, nodupKeys := hl }).entries =
    { fst := fst✝, snd := snd✝ } :: l
[PROOFSTEP]
rw [insert_of_neg h]
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ HEq (insertRec H0 IH { entries := c :: l, nodupKeys := (_ : NodupKeys (c :: l)) })
    (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
[PROOFSTEP]
rw [insertRec]
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : NodupKeys l
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ HEq
    (Eq.mpr
      (_ :
        C { entries := c :: l, nodupKeys := (_ : NodupKeys (c :: l)) } =
          C (insert c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) }))
      (IH c.fst c.snd { entries := l, nodupKeys := (_ : NodupKeys l) }
        (_ : ¬c.fst ∈ List.keys { entries := l, nodupKeys := (_ : NodupKeys l) }.entries)
        (insertRec H0 IH { entries := l, nodupKeys := (_ : NodupKeys l) })))
    (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
[PROOFSTEP]
apply cast_heq
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ NodupKeys (kextract a s.entries).snd
[PROOFSTEP]
rw [kextract_eq_dlookup_kerase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ NodupKeys (dlookup a s.entries, kerase a s.entries).snd
[PROOFSTEP]
exact s.nodupKeys.kerase _
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)
[PROOFSTEP]
simp [extract]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧
    { entries := kerase a s.entries, nodupKeys := (_ : NodupKeys (kerase a s.entries)) } = erase a s
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s
[PROOFSTEP]
rfl
[GOAL]
case right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ { entries := kerase a s.entries, nodupKeys := (_ : NodupKeys (kerase a s.entries)) } = erase a s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries = s.entries
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ s₄ : AList β
p₁₂ : s₁.entries ~ s₂.entries
p₃₄ : s₃.entries ~ s₄.entries
⊢ (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries
[PROOFSTEP]
simp [p₁₂.kunion s₃.nodupKeys p₃₄]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂
[PROOFSTEP]
ext
[GOAL]
case a.a.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
n✝ : ℕ
a✝ : Sigma β
⊢ a✝ ∈ get? (insert a b (s₁ ∪ s₂)).entries n✝ ↔ a✝ ∈ get? (insert a b s₁ ∪ s₂).entries n✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : AList β
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂ ∪ s₃).entries ↔ y ∈ dlookup x (s₁ ∪ (s₂ ∪ s₃)).entries
[PROOFSTEP]
simp [not_or, or_assoc, and_or_left, and_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂).entries ↔ y ∈ dlookup x (s₂ ∪ s₁).entries
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝ →
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
intro h'
[GOAL]
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝ →
    dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
intro h'
[GOAL]
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
cases' h' with h' h'
[GOAL]
case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
right
[GOAL]
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
refine' ⟨_, h'⟩
[GOAL]
case mp.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₂.entries
[PROOFSTEP]
apply h
[GOAL]
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ x✝ ∈ keys s₁
[PROOFSTEP]
rw [keys, ← List.dlookup_isSome, h']
[GOAL]
case mp.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ Option.isSome (some y✝) = true
[PROOFSTEP]
exact rfl
[GOAL]
case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
left
[GOAL]
case mp.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
rw [h'.2]
[GOAL]
case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
cases' h' with h' h'
[GOAL]
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
right
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
refine' ⟨_, h'⟩
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ List.keys s₁.entries
[PROOFSTEP]
intro h''
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ False
[PROOFSTEP]
apply h _ h''
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ x✝ ∈ keys s₂
[PROOFSTEP]
rw [keys, ← List.dlookup_isSome, h']
[GOAL]
case mpr.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ List.keys s₁.entries
⊢ Option.isSome (some y✝) = true
[PROOFSTEP]
exact rfl
[GOAL]
case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ List.keys s₁.entries ∧ dlookup x✝ s₂.entries = some y✝
[PROOFSTEP]
left
[GOAL]
case mpr.inr.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : Disjoint s₁ s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ List.keys s₂.entries ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝
[PROOFSTEP]
rw [h'.2]


[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ (invImage (fun a => PSigma.casesOn a fun ts snd => (length ts + length snd, length ts))
        Prod.instWellFoundedRelationProd).1
    { fst := ts, snd := t :: is } { fst := t :: ts, snd := is }
[PROOFSTEP]
simp_wf
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length ts + succ (length is), length ts)
    (succ (length ts) + length is, succ (length ts))
[PROOFSTEP]
simp [Nat.succ_add]
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length ts + succ (length is), length ts)
    (succ (length ts + length is), succ (length ts))
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ (invImage (fun a => PSigma.casesOn a fun ts snd => (length ts + length snd, length ts))
        Prod.instWellFoundedRelationProd).1
    { fst := is, snd := [] } { fst := t :: ts, snd := is }
[PROOFSTEP]
simp_wf
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length is, length is)
    (succ (length ts) + length is, succ (length ts))
[PROOFSTEP]
simp [Nat.succ_add]
[GOAL]
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (length is, length is)
    (succ (length ts + length is), succ (length ts))
[PROOFSTEP]
decreasing_tactic
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
l : List α
⊢ Decidable (Chain R a l)
[PROOFSTEP]
induction l generalizing a with
| nil => simp only [List.Chain.nil]; infer_instance
| cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
l : List α
⊢ Decidable (Chain R a l)
[PROOFSTEP]
induction l generalizing a with
| nil => simp only [List.Chain.nil]; infer_instance
| cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Decidable (Chain R a [])
[PROOFSTEP]

| nil => simp only [List.Chain.nil]; infer_instance
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Decidable (Chain R a [])
[PROOFSTEP]
simp only [List.Chain.nil]
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
⊢ Decidable (Chain R a (a✝ :: as))
[PROOFSTEP]

| cons a as ih => haveI := ih; simp only [List.chain_cons]; infer_instance
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
⊢ Decidable (Chain R a (a✝ :: as))
[PROOFSTEP]
haveI := ih
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
this : (a : α) → Decidable (Chain R a as)
⊢ Decidable (Chain R a (a✝ :: as))
[PROOFSTEP]
simp only [List.chain_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
a✝ : α
as : List α
ih : (a : α) → Decidable (Chain R a as)
a : α
this : (a : α) → Decidable (Chain R a as)
⊢ Decidable (R a a✝ ∧ Chain R a✝ as)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
⊢ Decidable (Chain' R l)
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
⊢ Decidable (Chain' R [])
[PROOFSTEP]
dsimp only [List.Chain']
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
head✝ : α
tail✝ : List α
⊢ Decidable (Chain' R (head✝ :: tail✝))
[PROOFSTEP]
dsimp only [List.Chain']
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
⊢ Decidable True
[PROOFSTEP]
infer_instance
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
R : α → α → Prop
inst✝ : DecidableRel R
head✝ : α
tail✝ : List α
⊢ Decidable (Chain R head✝ tail✝)
[PROOFSTEP]
infer_instance


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h : Forall₂ R (a :: l₁) (b :: l₂)
⊢ R a b ∧ Forall₂ R l₁ l₂
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
a✝¹ : R a b
a✝ : Forall₂ R l₁ l₂
⊢ R a b ∧ Forall₂ R l₁ l₂
[PROOFSTEP]
constructor
[GOAL]
case cons.left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
a✝¹ : R a b
a✝ : Forall₂ R l₁ l₂
⊢ R a b
[PROOFSTEP]
assumption
[GOAL]
case cons.right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
b : β
l₁ : List α
l₂ : List β
a✝¹ : R a b
a✝ : Forall₂ R l₁ l₂
⊢ Forall₂ R l₁ l₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂
[PROOFSTEP]
induction h
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []
[PROOFSTEP]
constructor
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S (a✝² :: l₁✝) (b✝ :: l₂✝)
[PROOFSTEP]
constructor
[GOAL]
case cons.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝
[PROOFSTEP]
solve_by_elim
[GOAL]
case cons.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝
[PROOFSTEP]
solve_by_elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ Rₐ [] [] ↔ ∀ (x : α), x ∈ [] → Rₐ x x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : α
l : List α
⊢ Forall₂ Rₐ (a :: l) (a :: l) ↔ ∀ (x : α), x ∈ a :: l → Rₐ x x
[PROOFSTEP]
simp [@forall₂_same l]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ (Forall₂ fun x x_1 => x = x_1) = Eq
[PROOFSTEP]
funext a b
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b = (a = b)
[PROOFSTEP]
apply propext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b ↔ a = b
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a b → a = b
[PROOFSTEP]
intro h
[GOAL]
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
h : Forall₂ (fun x x_1 => x = x_1) a b
⊢ a = b
[PROOFSTEP]
induction h
[GOAL]
case h.h.a.mp.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ [] = []
[PROOFSTEP]
rfl
[GOAL]
case h.h.a.mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x x_1 => x = x_1) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝
[PROOFSTEP]
simp only [*]
[GOAL]
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a b : List α
⊢ a = b → Forall₂ (fun x x_1 => x = x_1) a b
[PROOFSTEP]
rintro rfl
[GOAL]
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a : List α
⊢ Forall₂ (fun x x_1 => x = x_1) a a
[PROOFSTEP]
exact forall₂_refl _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []
[PROOFSTEP]
cases H
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ [] = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List β
⊢ l = [] → Forall₂ R [] l
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ R [] []
[PROOFSTEP]
exact Forall₂.nil
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
H : Forall₂ R l []
⊢ l = []
[PROOFSTEP]
cases H
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ [] = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
⊢ l = [] → Forall₂ R l []
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
⊢ Forall₂ R [] []
[PROOFSTEP]
exact Forall₂.nil
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Prop
u : List β
⊢ Forall₂ (fun a b => p a ∧ R a b) [] u ↔ (∀ (a : α), a ∈ [] → p a) ∧ Forall₂ R [] u
[PROOFSTEP]
simp only [forall₂_nil_left_iff, forall_prop_of_false (not_mem_nil _), imp_true_iff, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ Forall₂ (fun a b => p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u
[PROOFSTEP]
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc, @and_comm _ (p a),
  @and_left_comm _ (p a), exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ (p a ∧ ∃ x, R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ x_1, Forall₂ R l x_1 ∧ u = x :: x_1) ↔
    p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ b, R a b ∧ ∃ x, Forall₂ R l x ∧ u = b :: x
[PROOFSTEP]
simp only [and_comm, and_assoc, and_left_comm, ← exists_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → α
x✝ : List β
⊢ Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝
[PROOFSTEP]
simp only [map, forall₂_nil_left_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → α
a : γ
l : List γ
x✝ : List β
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝
[PROOFSTEP]
simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → β
x✝ : List α
⊢ Forall₂ R x✝ (map f []) ↔ Forall₂ (fun a c => R a (f c)) x✝ []
[PROOFSTEP]
simp only [map, forall₂_nil_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : γ → β
x✝ : List α
b : γ
u : List γ
⊢ Forall₂ R x✝ (map f (b :: u)) ↔ Forall₂ (fun a c => R a (f c)) x✝ (b :: u)
[PROOFSTEP]
simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ zip (a✝ :: l₁✝) (b✝ :: l₂✝)
⊢ R x y
[PROOFSTEP]
rw [zip, zipWith, mem_cons] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
⊢ R x y
[PROOFSTEP]
match hx with
| Or.inl rfl => exact h₁
| Or.inr h₃ => exact forall₂_zip h₂ h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x y
⊢ R x y
[PROOFSTEP]
exact h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
x✝¹ : β
x✝ : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x✝ x✝¹
⊢ R x y
[PROOFSTEP]
exact forall₂_zip h₂ h₃
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : length l₁ = length l₂ ∧ ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
⊢ Forall₂ R l₁ l₂
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h₁ : length l₁ = length l₂
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
⊢ Forall₂ R l₁ l₂
[PROOFSTEP]
induction' l₁ with a l₁ IH generalizing l₂
[GOAL]
case intro.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂✝ : List β
h₁✝ : length l₁ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂✝ → R a b
l₂ : List β
h₁ : length [] = length l₂
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip [] l₂ → R a b
⊢ Forall₂ R [] l₂
[PROOFSTEP]
cases length_eq_zero.1 h₁.symm
[GOAL]
case intro.nil.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h₁✝ : length l₁ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b
h₁ : length [] = length []
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ zip [] [] → R a b
⊢ Forall₂ R [] []
[PROOFSTEP]
constructor
[GOAL]
case intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
l₂ : List β
h₁ : length (a :: l₁) = length l₂
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) l₂ → R a_1 b
⊢ Forall₂ R (a :: l₁) l₂
[PROOFSTEP]
cases' l₂ with b l₂
[GOAL]
case intro.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂ : List β
h₁✝ : length l₁✝ = length l₂
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
h₁ : length (a :: l₁) = length []
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ zip (a :: l₁) [] → R a_1 b
⊢ Forall₂ R (a :: l₁) []
[PROOFSTEP]
simp at h₁
[GOAL]
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : length (a :: l₁) = length (b :: l₂)
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
[PROOFSTEP]
simp only [length_cons, succ.injEq] at h₁
[GOAL]
case intro.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
⊢ Forall₂ R (a :: l₁) (b :: l₂)
[PROOFSTEP]
exact
  Forall₂.cons (h₂ <| by simp [zip])
    (IH h₁ <| fun h =>
      h₂ <| by
        simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]; right
        simpa [zip] using h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
⊢ (a, b) ∈ zip (a :: l₁) (b :: l₂)
[PROOFSTEP]
simp [zip]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ (a✝, b✝) ∈ zip (a :: l₁) (b :: l₂)
[PROOFSTEP]
simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
[PROOFSTEP]
right
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁✝ : List α
l₂✝ : List β
h₁✝ : length l₁✝ = length l₂✝
h₂✝ : ∀ {a : α} {b : β}, (a, b) ∈ zip l₁✝ l₂✝ → R a b
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, length l₁ = length l₂ → (∀ {a : α} {b : β}, (a, b) ∈ zip l₁ l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ zip (a :: l₁) (b :: l₂) → R a_1 b_1
h₁ : length l₁ = length l₂
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ zip l₁ l₂
⊢ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
[PROOFSTEP]
simpa [zip] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
x✝² : List α
x✝¹ : List β
x✝ : Forall₂ R x✝² x✝¹
⊢ Forall₂ R (take 0 x✝²) (take 0 x✝¹)
[PROOFSTEP]
simp only [Forall₂.nil, take]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n✝ : ℕ
⊢ Forall₂ R (take (n✝ + 1) []) (take (n✝ + 1) [])
[PROOFSTEP]
simp only [Forall₂.nil, take]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (take (n + 1) (a✝ :: l₁✝)) (take (n + 1) (b✝ :: l₂✝))
[PROOFSTEP]
simp [And.intro h₁ h₂, forall₂_take n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
x✝¹ : List α
x✝ : List β
h : Forall₂ R x✝¹ x✝
⊢ Forall₂ R (drop 0 x✝¹) (drop 0 x✝)
[PROOFSTEP]
simp only [drop, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n✝ : ℕ
⊢ Forall₂ R (drop (n✝ + 1) []) (drop (n✝ + 1) [])
[PROOFSTEP]
simp only [Forall₂.nil, drop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
n : ℕ
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (drop (n + 1) (a✝ :: l₁✝)) (drop (n + 1) (b✝ :: l₂✝))
[PROOFSTEP]
simp [And.intro h₁ h₂, forall₂_drop n]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take (length l₁) l) l₁
[PROOFSTEP]
have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) := forall₂_take (length l₁) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂))
⊢ Forall₂ R (take (length l₁) l) l₁
[PROOFSTEP]
rwa [take_left] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop (length l₁) l) l₂
[PROOFSTEP]
have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) := forall₂_drop (length l₁) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂))
⊢ Forall₂ R (drop (length l₁) l) l₂
[PROOFSTEP]
rwa [drop_left] at h'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
x✝ : R a b
⊢ (fun x x_1 => x ∈ x_1) a [] ↔ (fun x x_1 => x ∈ x_1) b []
[PROOFSTEP]
simp only [not_mem_nil]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun x x_1 => x ∈ x_1) a (a' :: as) ↔ (fun x x_1 => x ∈ x_1) b (b' :: bs)
[PROOFSTEP]
simp only [mem_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
[PROOFSTEP]
exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse (a✝ :: l₁✝)) (reverse (b✝ :: l₂✝))
[PROOFSTEP]
simp only [reverse_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse l₁✝ ++ [a✝]) (reverse l₂✝ ++ [b✝])
[PROOFSTEP]
exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R l₁ l₂
[PROOFSTEP]
rw [← reverse_reverse l₁, ← reverse_reverse l₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R (reverse (reverse l₁)) (reverse (reverse l₂))
[PROOFSTEP]
exact rel_reverse h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : (R ⇒ fun x x_1 => x ↔ x_1) (fun x => p x = true) fun x => q x = true
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
dsimp [LiftFun] at hpq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
have : q b := by rwa [← hpq h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ q b = true
[PROOFSTEP]
rwa [← hpq h₁]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
this : q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
simp only [filter_cons_of_pos _ h, filter_cons_of_pos _ this, forall₂_cons, h₁, true_and_iff, rel_filter hpq h₂]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
have : ¬q b := by rwa [← hpq h₁]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ ¬q b = true
[PROOFSTEP]
rwa [← hpq h₁]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
this : ¬q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
[PROOFSTEP]
simp only [filter_cons_of_neg _ h, filter_cons_of_neg _ this, rel_filter hpq h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))
[PROOFSTEP]
rw [filterMap_cons, filterMap_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)
[PROOFSTEP]
exact
  match f a, g b, hfg h₁ with
  | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
  | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ → ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
[PROOFSTEP]
induction' h with _ a b l1 l2 rab _ ih b l1 l2 _ ih
[GOAL]
case mp.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l✝ : List β
⊢ ∃ l, Forall₂ R [] l ∧ l <+ l✝
[PROOFSTEP]
exact ⟨nil, Forall₂.nil, nil_sublist _⟩
[GOAL]
case mp.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2
[PROOFSTEP]
obtain ⟨l, hl1, hl2⟩ := ih
[GOAL]
case mp.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
a✝ : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ l, Forall₂ R (a :: l1) l ∧ l <+ b :: l2
[PROOFSTEP]
refine' ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
[GOAL]
case mp.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
b : β
l1 : List α
l2 : List β
a✝ : SublistForall₂ R l1 l2
ih : ∃ l, Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ l, Forall₂ R l1 l ∧ l <+ b :: l2
[PROOFSTEP]
obtain ⟨l, hl1, hl2⟩ := ih
[GOAL]
case mp.cons_right.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
b : β
l1 : List α
l2 : List β
a✝ : SublistForall₂ R l1 l2
l : List β
hl1 : Forall₂ R l1 l
hl2 : l <+ l2
⊢ ∃ l, Forall₂ R l1 l ∧ l <+ b :: l2
[PROOFSTEP]
exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
[PROOFSTEP]
obtain ⟨l, hl1, hl2⟩ := h
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂
[PROOFSTEP]
revert l₁
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l → SublistForall₂ R l₁ l₂
[PROOFSTEP]
induction' hl2 with _ _ _ _ ih _ _ _ _ ih
[GOAL]
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ [] → SublistForall₂ R l₁ []
[PROOFSTEP]
intro l₁ hl1
[GOAL]
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
intro l₁ hl1
[GOAL]
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
intro l₁ hl1
[GOAL]
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []
[PROOFSTEP]
rw [forall₂_nil_right_iff.1 hl1]
[GOAL]
case mpr.intro.intro.slnil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []
[PROOFSTEP]
exact SublistForall₂.nil
[GOAL]
case mpr.intro.intro.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ l₁✝
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
exact SublistForall₂.cons_right (ih hl1)
[GOAL]
case mpr.intro.intro.cons₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ (a✝¹ :: l₁✝)
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
[PROOFSTEP]
cases' hl1 with _ _ _ _ hr hl _
[GOAL]
case mpr.intro.intro.cons₂.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₂ l l₁✝¹ l₂✝ : List β
a✝² : β
a✝¹ : l₁✝¹ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝¹ → SublistForall₂ R l₁ l₂✝
a✝ : α
l₁✝ : List α
hr : R a✝ a✝²
hl : Forall₂ R l₁✝ l₁✝¹
⊢ SublistForall₂ R (a✝ :: l₁✝) (a✝² :: l₂✝)
[PROOFSTEP]
exact SublistForall₂.cons hr (ih hl)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a b c : List α
⊢ SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
[PROOFSTEP]
revert a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
c : List α
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
[PROOFSTEP]
induction' c with _ _ ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b [] → SublistForall₂ Rₐ a []
[PROOFSTEP]
rintro _ _ h1 h2
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a✝ b✝ : List α
h1 : SublistForall₂ Rₐ a✝ b✝
h2 : SublistForall₂ Rₐ b✝ []
⊢ SublistForall₂ Rₐ a✝ []
[PROOFSTEP]
cases h2
[GOAL]
case nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
a✝ : List α
h1 : SublistForall₂ Rₐ a✝ []
⊢ SublistForall₂ Rₐ a✝ []
[PROOFSTEP]
exact h1
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b (head✝ :: tail✝) → SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
rintro a b h1 h2
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b (head✝ :: tail✝)
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
cases' h2 with _ _ _ _ _ hbc tbc _ _ y1 btc
[GOAL]
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
cases h1
[GOAL]
case cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.nil
[GOAL]
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
h1 : SublistForall₂ Rₐ a (a₁✝ :: l₁✝)
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
cases' h1 with _ _ _ _ _ hab tab _ _ _ atb
[GOAL]
case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.nil
[GOAL]
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
[GOAL]
case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.cons_right (ih _ _ atb tbc)
[GOAL]
case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
[PROOFSTEP]
exact SublistForall₂.cons_right (ih _ _ h1 btc)