Theorem: Matrix.getM_pure (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
β : Fin n → Type u
v : (i : Fin n) → β i
⊢ (getM fun i => pure (v i)) = pure v
Tactic:
induction' n with n ih <;> simp[empty_eq, getM]
State after:
case zero
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ pure finZeroElim = pure v

case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (Seq.seq (pure fun succ i => cases (v 0) succ i) fun x => getM fun x => pure (v x.succ)) = pure v

State before:
case zero
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ pure finZeroElim = pure v
Tactic:
congr
State after:
case zero.e_a
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ finZeroElim = v

State before:
case zero.e_a
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ finZeroElim = v
Tactic:
funext x
State after:
case zero.e_a.h
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
x : Fin 0
⊢ finZeroElim x = v x

State before:
case zero.e_a.h
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
x : Fin 0
⊢ finZeroElim x = v x
Tactic:
exact x.elim0
State after:
no goals

State before:
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (Seq.seq (pure fun succ i => cases (v 0) succ i) fun x => getM fun x => pure (v x.succ)) = pure v
Tactic:
simp[vecHead, vecTail, Function.comp, seq_eq_bind, ih]
State after:
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (pure fun i => cases (v 0) (fun i => v i.succ) i) = pure v

State before:
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (pure fun i => cases (v 0) (fun i => v i.succ) i) = pure v
Tactic:
exact congr_arg _ (funext $ Fin.cases rfl (fun i => rfl))
State after:
no goals