-- Mathlib/Data/List/Sigma.lean
theorem mem_dlookup_kunion {a} {b : β a} {l₁ l₂ : List (Sigma β)} :
    b ∈ dlookup a (kunion l₁ l₂) ↔ b ∈ dlookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ dlookup a l₂

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ : b ∈ dlookup a (tail✝.kunion (kerase a' l₂)) ↔
  b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a (kerase a' l₂) :=
  ih
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
simp only [Option.mem_def, ne_eq, h₁, not_false_eq_true, dlookup_kerase_ne] at h₂

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ :
  dlookup a (tail✝.kunion (kerase a' l₂)) = some b ↔ dlookup a tail✝ = some b ∨ a ∉ tail✝.keys ∧ dlookup a l₂ = some b
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ : b ∈ dlookup a (tail✝.kunion (kerase a' l₂)) ↔
  b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a (kerase a' l₂) :=
  ih
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
simp? [h₁] at h₂ says
  simp only [Option.mem_def, ne_eq, h₁, not_false_eq_true, dlookup_kerase_ne] at h₂

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ :
  dlookup a (tail✝.kunion (kerase a' l₂)) = some b ↔ dlookup a tail✝ = some b ∨ a ∉ tail✝.keys ∧ dlookup a l₂ = some b
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
by_cases h₁ : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : a = a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ :
  dlookup a (tail✝.kunion (kerase a' l₂)) = some b ↔ dlookup a tail✝ = some b ∨ a ∉ tail✝.keys ∧ dlookup a l₂ = some b
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
simp [h₁, h₂]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
⊢ b ∈ dlookup a ((s :: tail✝).kunion l₂) ↔ b ∈ dlookup a (s :: tail✝) ∨ a ∉ (s :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
obtain ⟨a'⟩ := s

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
let h₂ := @ih (kerase a' l₂)

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ : b ∈ dlookup a (tail✝.kunion (kerase a' l₂)) ↔
  b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a (kerase a' l₂) :=
  ih
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
snd✝ : β a
⊢ b ∈ dlookup a ((⟨a, snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a, snd✝⟩ :: tail✝) ∨ a ∉ (⟨a, snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : a = a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ a ∉ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
subst h₁

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ a ∉ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
snd✝ : β a
⊢ b ∈ dlookup a ((⟨a, snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a, snd✝⟩ :: tail✝) ∨ a ∉ (⟨a, snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₂ : List (Sigma β)
⊢ b ∈ dlookup a ([].kunion l₂) ↔ b ∈ dlookup a [] ∨ a ∉ [].keys ∧ b ∈ dlookup a l₂

Tactic:
simp

Result:
no goals