Theorem: SizedArray.mapMIdx.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 : Fin (n + 1) → α → 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 ∘ Fin.succ) 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 [dif_pos]; rw [pure_bind]
| inr hlt =>
  unfold loop
  simp only [Nat.ne_of_lt hlt, Nat.ne_of_lt (Nat.succ_lt_succ hlt), dif_neg]
  rw [bind_assoc]
  apply bind_congr; intro b'
  rw [push_cons_eq_cons_push]
  exact mapMIdx.loop_cons_succ f a x (i+1) b (push r b')
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 : Fin (n + 1) → α → 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 ∘ Fin.succ) 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 : Fin (n + 1) → α → 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 ∘ Fin.succ) 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 : Fin (n + 1) → α → 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 ∘ Fin.succ) 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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if h : n + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f { val := n + 1, isLt := this } (cons a x)[n + 1]
      let r : SizedArray β (n + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (n + 1 + 1) this r) =
    do
    let y ←
      if h : n = n then pure (h ▸ r)
        else
          let_fun this := (_ : n < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := n, isLt := this } x[n]
          let r : SizedArray β (n + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (n + 1) 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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if h : n + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f { val := n + 1, isLt := this } (cons a x)[n + 1]
      let r : SizedArray β (n + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (n + 1 + 1) this r) =
    do
    let y ←
      if h : n = n then pure (h ▸ r)
        else
          let_fun this := (_ : n < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := n, isLt := this } x[n]
          let r : SizedArray β (n + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (n + 1) this r
    pure (cons b y)
Tactic:
simp only [dif_pos]
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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ pure (cons b r) = do
    let y ← pure 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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ pure (cons b r) = do
    let y ← pure r
    pure (cons b y)
Tactic:
rw [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 : Fin (n + 1) → α → 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 ∘ Fin.succ) x i hi₂ r
    pure (cons b y)
Tactic:
unfold loop
State after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f { val := i + 1, isLt := this } (cons a x)[i + 1]
      let r : SizedArray β (i + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (i + 1 + 1) this r) =
    do
    let y ←
      if h : i = n then pure (h ▸ r)
        else
          let_fun this := (_ : i < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := this } x[i]
          let r : SizedArray β (i + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (i + 1) this 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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f { val := i + 1, isLt := this } (cons a x)[i + 1]
      let r : SizedArray β (i + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (i + 1 + 1) this r) =
    do
    let y ←
      if h : i = n then pure (h ▸ r)
        else
          let_fun this := (_ : i < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := this } x[i]
          let r : SizedArray β (i + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (i + 1) this r
    pure (cons b y)
Tactic:
simp only [Nat.ne_of_lt hlt, Nat.ne_of_lt (Nat.succ_lt_succ hlt), dif_neg]
State after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
        loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r __do_lift)
    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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
        loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r __do_lift)
    pure (cons b y)
Tactic:
rw [bind_assoc]
State after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let x_1 ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r x_1)
    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 : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let x_1 ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r x_1)
    pure (cons b y)
Tactic:
apply bind_congr
State after:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ ∀ (a_1 : β),
    loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) a_1) = do
      let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r a_1)
      pure (cons b y)

State before:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ ∀ (a_1 : β),
    loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) a_1) = do
      let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r a_1)
      pure (cons b y)
Tactic:
intro b'
State after:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) b') = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)

State before:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) b') = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)
Tactic:
rw [push_cons_eq_cons_push]
State after:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (cons b (push r b')) = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)

State before:
case inr.h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
b' : β
⊢ loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (cons b (push r b')) = do
    let y ← loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r b')
    pure (cons b y)
Tactic:
exact mapMIdx.loop_cons_succ f a x (i+1) b (push r b')
State after:
no goals