Theorem: List.mapGraph_graph (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 : α → β
as as' : List α
has : as' ⊆ as
⊢ (map (fun x => (x, f x)) as).mapGraph as' = map f as'
Tactic:
induction' as' with a as' ih <;> simp[mapGraph]
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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'

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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Tactic:
have : a ∈ as ∧ as' ⊆ as := by simpa using has
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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
this : a ∈ as ∧ as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'

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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
this : a ∈ as ∧ as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Tactic:
rcases this with ⟨ha, has'⟩
State after:
case cons.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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'

State before:
case cons.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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ ((lookup a (map (fun x => (x, f x)) as)).toList ++ as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) =
    f a :: map f as'
Tactic:
simp[lookup_map_fun_of_mem f ha]
State after:
case cons.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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ (as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) = map f as'

State before:
case cons.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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
ha : a ∈ as
has' : as' ⊆ as
⊢ (as'.bind fun x => (lookup x (map (fun x => (x, f x)) as)).toList) = map f as'
Tactic:
exact ih has'
State after:
no goals

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 : α → β
as : List α
a : α
as' : List α
ih : as' ⊆ as → (map (fun x => (x, f x)) as).mapGraph as' = map f as'
has : a :: as' ⊆ as
⊢ a ∈ as ∧ as' ⊆ as
Tactic:
simpa using has
State after:
no goals