Theorem: SizedArray.mapM.loop_cons_succ (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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
cases Nat.eq_or_lt_of_le hi₂ with
| inl heq =>
  cases heq; unfold loop; simp only [Nat.lt_irrefl, dif_neg, pure_bind]
| inr hlt =>
  conv =>
    lhs; unfold loop
    rw [dif_pos (Nat.succ_lt_succ hlt)]
    rw [get_cons_succ a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt)]
    rhs; ext b'; rw [push_cons_eq_cons_push]
    rw [mapM.loop_cons_succ f a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt) b (r.push b')]
  conv =>
    rhs; unfold loop; rw [dif_pos hlt, bind_assoc]
State after:
no goals

State before:
case inl
α : 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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
heq : i = n
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
cases heq
State after:
case inl.refl
α : 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 : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ loop f (cons a x) (n + 1) hi₁ (cons b r) = do
    let y ← loop f x n hi₂ r
    pure (cons b y)

State before:
case inl.refl
α : 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 : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ loop f (cons a x) (n + 1) hi₁ (cons b r) = do
    let y ← loop f x n hi₂ r
    pure (cons b y)
Tactic:
unfold loop
State after:
case inl.refl
α : 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 : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if hlt : n + 1 < n + 1 then do
      let __do_lift ← f (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) hlt (push (cons b r) __do_lift)
    else
      let_fun this := (_ : n + 1 = n + 1);
      pure (this ▸ cons b r)) =
    do
    let y ←
      if hlt : n < n then do
          let __do_lift ← f x[n]
          loop f x (n + 1) hlt (push r __do_lift)
        else
          let_fun this := (_ : n = n);
          pure (this ▸ r)
    pure (cons b y)

State before:
case inl.refl
α : 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 : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if hlt : n + 1 < n + 1 then do
      let __do_lift ← f (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) hlt (push (cons b r) __do_lift)
    else
      let_fun this := (_ : n + 1 = n + 1);
      pure (this ▸ cons b r)) =
    do
    let y ←
      if hlt : n < n then do
          let __do_lift ← f x[n]
          loop f x (n + 1) hlt (push r __do_lift)
        else
          let_fun this := (_ : n = n);
          pure (this ▸ r)
    pure (cons b y)
Tactic:
simp only [Nat.lt_irrefl, dif_neg, pure_bind]
State after:
no goals

State before:
case inr
α : 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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold loop
  rw [dif_pos (Nat.succ_lt_succ hlt)]
  rw [get_cons_succ a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt)]
  rhs; ext b'; rw [push_cons_eq_cons_push]
  rw [mapM.loop_cons_succ f a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt) b (r.push b')]
State after:
case inr
α : 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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let b' ← f x[i]
      let y ← loop f x (i + 1) hlt (push r b')
      pure (cons b y)) =
    do
    let y ← loop f x i hi₂ r
    pure (cons b y)

State before:
case inr
α : 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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let b' ← f x[i]
      let y ← loop f x (i + 1) hlt (push r b')
      pure (cons b y)) =
    do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
conv =>
  rhs; unfold loop; rw [dif_pos hlt, bind_assoc]
State after:
no goals