internlm/Lean-Github huggingface dataset:
Theorem: List.mapM'_eq_none_iff
Proof 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)
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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 }
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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)
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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) }
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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 }
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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)
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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)
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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] }
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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] }
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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]
Proof state after:
no goals
Theorem: List.mapM'_eq_none_iff
Proof 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
Proof 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
Theorem: List.mapM'_eq_none_iff
Proof 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]
Proof state after:
no goals
Theorem: List.length_mapM'
Proof state before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
bs : List β
f : α → Option β
as : List α
⊢ mapM' f as = some bs → bs.length = as.length
Tactic:
induction' as with a as ih generalizing bs
Proof state after:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
bs : List β
⊢ mapM' f [] = some bs → bs.length = [].length

case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → bs.length = as.length
bs : List β
⊢ mapM' f (a :: as) = some bs → bs.length = (a :: as).length
Theorem: List.length_mapM'
Proof state before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
bs : List β
⊢ mapM' f [] = some bs → bs.length = [].length
Tactic:
simp only [mapM', Option.pure_eq_some, Option.some.injEq, length_nil]
Proof state after:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
bs : List β
⊢ [] = bs → bs.length = 0
Theorem: List.length_mapM'
Proof state before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
bs : List β
⊢ [] = bs → bs.length = 0
Tactic:
rintro rfl
Proof state after:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
⊢ [].length = 0
Theorem: List.length_mapM'
Proof state before:
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
⊢ [].length = 0
Tactic:
simp
Proof state after:
no goals
Theorem: List.length_mapM'
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → bs.length = as.length
bs : List β
⊢ mapM' f (a :: as) = some bs → bs.length = (a :: as).length
Tactic:
simp only [mapM', Option.pure_eq_some, Option.bind_eq_bind, Option.bind_eq_some,
Option.some.injEq, length_cons, forall_exists_index, and_imp]
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → bs.length = as.length
bs : List β
⊢ ∀ (x : β), f a = some x → ∀ (x_1 : List β), mapM' f as = some x_1 → x :: x_1 = bs → bs.length = as.length.succ
Theorem: List.length_mapM'
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → bs.length = as.length
bs : List β
⊢ ∀ (x : β), f a = some x → ∀ (x_1 : List β), mapM' f as = some x_1 → x :: x_1 = bs → bs.length = as.length.succ
Tactic:
rintro b _ bs hbs rfl
Proof state after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → bs.length = as.length
b : β
a✝ : f a = some b
bs : List β
hbs : mapM' f as = some bs
⊢ (b :: bs).length = as.length.succ
Theorem: List.length_mapM'
Proof state before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.156032 → Type ?u.156034
α : Type u_2
β : Type u_1
inst✝ : Monad m
f : α → Option β
a : α
as : List α
ih : ∀ {bs : List β}, mapM' f as = some bs → bs.length = as.length
b : β
a✝ : f a = some b
bs : List β
hbs : mapM' f as = some bs
⊢ (b :: bs).length = as.length.succ
Tactic:
simpa using ih hbs
Proof state after:
no goals
Theorem: List.mapM'_mem_inversion
Proof 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
Proof 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
Theorem: List.mapM'_mem_inversion
Proof 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
Proof 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
Theorem: List.mapM'_mem_inversion
Proof 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
Proof 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
Theorem: List.mapM'_mem_inversion
Proof 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
Proof state after:
no goals
Theorem: List.mapM'_mem_inversion
Proof 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
Proof 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
Theorem: List.mapM'_mem_inversion
Proof 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⟩
Proof 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
Theorem: List.mapM'_mem_inversion
Proof 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
Proof 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
Theorem: List.mapM'_mem_inversion
Proof 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)
Proof 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