Theorem: List.length_mapM' (Logic/Vorspiel/Vorspiel.lean)

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
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

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]
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

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
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

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
State after:
no goals

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]
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

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
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

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
State after:
no goals