Theorem: List.mapM'_mem_inversion (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
bs : List β
b : β
f : α → Option β
as : List α
h : mapM' f as = some bs
hb : b ∈ bs
⊢ ∃ a, f a = some b
Tactic:
induction' as with a as ih generalizing bs
State after:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
bs : List β
h : mapM' f [] = some bs
hb : b ∈ bs
⊢ ∃ a, f a = some b

case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs : List β
h : mapM' f (a :: as) = some bs
hb : b ∈ bs
⊢ ∃ a, f a = some b

State before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
bs : List β
h : mapM' f [] = some bs
hb : b ∈ bs
⊢ ∃ a, f a = some b
Tactic:
simp only [mapM', Option.pure_eq_some, Option.some.injEq] at h
State after:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
bs : List β
hb : b ∈ bs
h : [] = bs
⊢ ∃ a, f a = some b

State before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
bs : List β
hb : b ∈ bs
h : [] = bs
⊢ ∃ a, f a = some b
Tactic:
rcases h with rfl
State after:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
hb : b ∈ []
⊢ ∃ a, f a = some b

State before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
hb : b ∈ []
⊢ ∃ a, f a = some b
Tactic:
simp at hb
State after:
no goals

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs : List β
h : mapM' f (a :: as) = some bs
hb : b ∈ bs
⊢ ∃ a, f a = some b
Tactic:
simp only [mapM', Option.pure_eq_some, Option.bind_eq_bind, Option.bind_eq_some,
Option.some.injEq] at h
State after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs : List β
hb : b ∈ bs
h : ∃ a_1, f a = some a_1 ∧ ∃ a, mapM' f as = some a ∧ a_1 :: a = bs
⊢ ∃ a, f a = some b

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs : List β
hb : b ∈ bs
h : ∃ a_1, f a = some a_1 ∧ ∃ a, mapM' f as = some a ∧ a_1 :: a = bs
⊢ ∃ a, f a = some b
Tactic:
rcases h with ⟨b', hb', bs', hbs', rfl⟩
State after:
case cons.intro.intro.intro.intro
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb : b ∈ b' :: bs'
⊢ ∃ a, f a = some b

State before:
case cons.intro.intro.intro.intro
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb : b ∈ b' :: bs'
⊢ ∃ a, f a = some b
Tactic:
have : b = b' ∨ b ∈ bs' := by simpa using hb
State after:
case cons.intro.intro.intro.intro
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb : b ∈ b' :: bs'
this : b = b' ∨ b ∈ bs'
⊢ ∃ a, f a = some b

State before:
case cons.intro.intro.intro.intro
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb : b ∈ b' :: bs'
this : b = b' ∨ b ∈ bs'
⊢ ∃ a, f a = some b
Tactic:
rcases this with (rfl | hb)
State after:
case cons.intro.intro.intro.intro.inl
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs' : List β
hbs' : mapM' f as = some bs'
hb' : f a = some b
hb : b ∈ b :: bs'
⊢ ∃ a, f a = some b

case cons.intro.intro.intro.intro.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb✝ : b ∈ b' :: bs'
hb : b ∈ bs'
⊢ ∃ a, f a = some b

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb : b ∈ b' :: bs'
⊢ b = b' ∨ b ∈ bs'
Tactic:
simpa using hb
State after:
no goals

State before:
case cons.intro.intro.intro.intro.inl
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
bs' : List β
hbs' : mapM' f as = some bs'
hb' : f a = some b
hb : b ∈ b :: bs'
⊢ ∃ a, f a = some b
Tactic:
exact ⟨a, hb'⟩
State after:
no goals

State before:
case cons.intro.intro.intro.intro.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.157952 → Type ?u.157954
α : Type u_2
β : Type u_1
inst✝ : Monad m
b : β
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → b ∈ bs → ∃ a, f a = some b
b' : β
hb' : f a = some b'
bs' : List β
hbs' : mapM' f as = some bs'
hb✝ : b ∈ b' :: bs'
hb : b ∈ bs'
⊢ ∃ a, f a = some b
Tactic:
exact ih hbs' hb
State after:
no goals