Theorem: SizedArray.mapM_cons (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ mapM f (cons a x) = do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold mapM; unfold mapM.loop
  rw [dif_pos n.zero_lt_succ, get_cons_zero a x]
  rhs; ext b; change mapM.loop f (cons a x) (0+1) (n.zero_lt_succ) (cons b empty)
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ (do
      let b ← f a
      mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty)) =
    do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ (do
      let b ← f a
      mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty)) =
    do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Tactic:
apply bind_congr
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β),
    mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons a_1 empty) = do
      let y ← mapM f x
      pure (cons a_1 y)

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β),
    mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons a_1 empty) = do
      let y ← mapM f x
      pure (cons a_1 y)
Tactic:
intro b
State after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
⊢ mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty) = do
    let y ← mapM f x
    pure (cons b y)

State before:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
⊢ mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty) = do
    let y ← mapM f x
    pure (cons b y)
Tactic:
exact mapM.loop_cons_succ f a x (hi₁:=n.zero_lt_succ) b empty
State after:
no goals