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

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
l : List α
⊢ mapM' f l = none ↔ ∃ a ∈ l, f a = none
Tactic:
induction' l with a l ih <;> simp[Option.bind_eq_bind]
State after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) ↔ f a = none ∨ ∃ a ∈ l, f a = none

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) ↔ f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
{ constructor
  { intros H
    rcases hb : f a with (_ | b); { simp }
    rcases hbs : mapM' f l with (_ | bs)
    { exact Or.inr (ih.mp hbs) }
    { have : False := by simpa[Option.pure_eq_some] using (H b hb) bs hbs
      contradiction } }
  { rintro (h | h)
    { simp[h] }
    { have := ih.mpr h; simp[this] } } }
State after:
no goals

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) ↔ f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
constructor
State after:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) → f a = none ∨ ∃ a ∈ l, f a = none

case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a

State before:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) → f a = none ∨ ∃ a ∈ l, f a = none

case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
{ intros H
  rcases hb : f a with (_ | b); { simp }
  rcases hbs : mapM' f l with (_ | bs)
  { exact Or.inr (ih.mp hbs) }
  { have : False := by simpa[Option.pure_eq_some] using (H b hb) bs hbs
    contradiction } }
State after:
case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a

State before:
case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
{ rintro (h | h)
  { simp[h] }
  { have := ih.mpr h; simp[this] } }
State after:
no goals

State before:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a) → f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
intros H
State after:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
⊢ f a = none ∨ ∃ a ∈ l, f a = none

State before:
case cons.mp
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
⊢ f a = none ∨ ∃ a ∈ l, f a = none
Tactic:
rcases hb : f a with (_ | b)
State after:
case cons.mp.none
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
hb : f a = none
⊢ none = none ∨ ∃ a ∈ l, f a = none

case cons.mp.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
⊢ some b = none ∨ ∃ a ∈ l, f a = none

State before:
case cons.mp.none
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
hb : f a = none
⊢ none = none ∨ ∃ a ∈ l, f a = none

case cons.mp.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
{ simp }
State after:
case cons.mp.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
⊢ some b = none ∨ ∃ a ∈ l, f a = none

State before:
case cons.mp.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
rcases hbs : mapM' f l with (_ | bs)
State after:
case cons.mp.some.none
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
hbs : mapM' f l = none
⊢ some b = none ∨ ∃ a ∈ l, f a = none

case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
⊢ some b = none ∨ ∃ a ∈ l, f a = none

State before:
case cons.mp.some.none
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
hbs : mapM' f l = none
⊢ some b = none ∨ ∃ a ∈ l, f a = none

case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
{ exact Or.inr (ih.mp hbs) }
State after:
case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
⊢ some b = none ∨ ∃ a ∈ l, f a = none

State before:
case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
{ have : False := by simpa[Option.pure_eq_some] using (H b hb) bs hbs
  contradiction }
State after:
no goals

State before:
case cons.mp.none
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
hb : f a = none
⊢ none = none ∨ ∃ a ∈ l, f a = none
Tactic:
simp
State after:
no goals

State before:
case cons.mp.some.none
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
hbs : mapM' f l = none
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
exact Or.inr (ih.mp hbs)
State after:
no goals

State before:
case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
have : False := by simpa[Option.pure_eq_some] using (H b hb) bs hbs
State after:
case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
this : False
⊢ some b = none ∨ ∃ a ∈ l, f a = none

State before:
case cons.mp.some.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
this : False
⊢ some b = none ∨ ∃ a ∈ l, f a = none
Tactic:
contradiction
State after:
no goals

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
H : ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
b : β
hb : f a = some b
bs : List β
hbs : mapM' f l = some bs
⊢ False
Tactic:
simpa[Option.pure_eq_some] using (H b hb) bs hbs
State after:
no goals

State before:
case cons.mpr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
⊢ (f a = none ∨ ∃ a ∈ l, f a = none) → ∀ (a_2 : β), f a = some a_2 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
rintro (h | h)
State after:
case cons.mpr.inl
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a

case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a

State before:
case cons.mpr.inl
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a

case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
{ simp[h] }
State after:
case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a

State before:
case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
{ have := ih.mpr h; simp[this] }
State after:
no goals

State before:
case cons.mpr.inl
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
simp[h]
State after:
no goals

State before:
case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
have := ih.mpr h
State after:
case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
this : mapM' f l = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a

State before:
case cons.mpr.inr
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.146799 → Type ?u.146801
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
l : List α
ih : mapM' f l = none ↔ ∃ a ∈ l, f a = none
h : ∃ a ∈ l, f a = none
this : mapM' f l = none
⊢ ∀ (a_1 : β), f a = some a_1 → ∀ (a : List β), ¬mapM' f l = some a
Tactic:
simp[this]
State after:
no goals