Theorem: List.lookup_map_fun_of_mem (Logic/Vorspiel/OmegaRec.lean)

State before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
as : List α
h : a ∈ as
⊢ lookup a (map (fun x => (x, f x)) as) = some (f a)
Tactic:
induction' as with a' as ih
State after:
case nil
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)

case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

State before:
case nil
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)
Tactic:
simp at h
State after:
no goals

State before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a ∈ a' :: as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Tactic:
simp at h
State after:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

State before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Tactic:
have : a = a' ∨ (a ≠ a' ∧ a ∈ as) := by { by_cases ha : a = a'; { simp[ha] }; { simp[ha] at h; exact Or.inr ⟨ha, h⟩ } }
State after:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
this : a = a' ∨ a ≠ a' ∧ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)

State before:
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
this : a = a' ∨ a ≠ a' ∧ a ∈ as
⊢ lookup a (map (fun x => (x, f x)) (a' :: as)) = some (f a)
Tactic:
rcases this with (rfl | ⟨hne, hmem⟩) <;> simp[lookup]
State after:
case cons.inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
hne : a ≠ a'
hmem : a ∈ as
⊢ (match a == a' with
    | true => some (f a')
    | false => lookup a (map (fun x => (x, f x)) as)) =
    some (f a)

State before:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
by_cases ha : a = a'
State after:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

State before:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
{ simp[ha] }
State after:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

State before:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
{ simp[ha] at h; exact Or.inr ⟨ha, h⟩ }
State after:
no goals

State before:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
simp[ha]
State after:
no goals

State before:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
simp[ha] at h
State after:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
ha : ¬a = a'
h : a ∈ as
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as

State before:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
ha : ¬a = a'
h : a ∈ as
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
Tactic:
exact Or.inr ⟨ha, h⟩
State after:
no goals

State before:
case cons.inr.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
hne : a ≠ a'
hmem : a ∈ as
⊢ (match a == a' with
    | true => some (f a')
    | false => lookup a (map (fun x => (x, f x)) as)) =
    some (f a)
Tactic:
simp[beq_false_of_ne hne, ih hmem]
State after:
no goals