Theorem: Array.mapM.map_cons_succ (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ map f (cons a x) (i + 1) (cons b y) = do
    let y ← map f x i y
    pure (cons b y)
Tactic:
unfold map
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < size (cons a x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < size (cons a x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
simp only [size_cons]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
if h : i < x.size then
  rw [dif_pos (Nat.succ_lt_succ h), dif_pos h, bind_assoc]
  apply bind_congr; intro b'
  exact mapM.map_cons_succ f a x (i+1) b (push y b')
else
  rw [dif_neg h, dif_neg (h ∘ Nat.lt_of_succ_lt_succ)]
  rw [pure_bind]
State after:
no goals

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
rw [dif_pos (Nat.succ_lt_succ h), dif_pos h, bind_assoc]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ (do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f x[i]
    let y ← map f x (i + 1) (push y x_1)
    pure (cons b y)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ (do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)) =
    do
    let x_1 ← f x[i]
    let y ← map f x (i + 1) (push y x_1)
    pure (cons b y)
Tactic:
apply bind_congr
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ ∀ (a_1 : β),
    map f (cons a x) (i + 1 + 1) (push (cons b y) a_1) = do
      let y ← map f x (i + 1) (push y a_1)
      pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
⊢ ∀ (a_1 : β),
    map f (cons a x) (i + 1 + 1) (push (cons b y) a_1) = do
      let y ← map f x (i + 1) (push y a_1)
      pure (cons b y)
Tactic:
intro b'
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
b' : β
⊢ map f (cons a x) (i + 1 + 1) (push (cons b y) b') = do
    let y ← map f x (i + 1) (push y b')
    pure (cons b y)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : i < size x
b' : β
⊢ map f (cons a x) (i + 1 + 1) (push (cons b y) b') = do
    let y ← map f x (i + 1) (push y b')
    pure (cons b y)
Tactic:
exact mapM.map_cons_succ f a x (i+1) b (push y b')
State after:
no goals

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ (if hlt : i + 1 < Nat.succ (size x) then do
      let __do_lift ← f (cons a x)[i + 1]
      map f (cons a x) (i + 1 + 1) (push (cons b y) __do_lift)
    else pure (cons b y)) =
    do
    let y ←
      if hlt : i < size x then do
          let __do_lift ← f x[i]
          map f x (i + 1) (push y __do_lift)
        else pure y
    pure (cons b y)
Tactic:
rw [dif_neg h, dif_neg (h ∘ Nat.lt_of_succ_lt_succ)]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
a : α
x : Array α
i : Nat
b : β
y : Array β
h : ¬i < size x
⊢ pure (cons b y) = do
    let y ← pure y
    pure (cons b y)
Tactic:
rw [pure_bind]
State after:
no goals