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

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
⊢ loop f (cons a x) (i + 1) h₁ b = loop (fun i b => f (i + 1) b) x i h₂ b
Tactic:
unfold loop
State after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
if h : i = n then
  cases h; rw [dif_pos rfl, dif_pos rfl]
else
  have : i < n := Nat.lt_of_le_of_ne h₂ h
  simp only [dif_neg (Nat.ne_of_lt this), dif_neg (Nat.ne_of_lt (Nat.succ_lt_succ this))]
  rw [get_cons_succ]
  exact bind_congr λ b => foldlMIdx.loop_cons_succ f a x (i+1) (Nat.succ_lt_succ this) this b
State after:
no goals

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : i = n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
cases h
State after:
case refl
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
h₁ : n + 1 ≤ n + 1
h₂ : n ≤ n
b : β (n + 1)
⊢ (if h : n + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f (n + 1) b (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) this __do_lift) =
    if h : n = n then pure (h ▸ b)
    else
      let_fun this := (_ : n < n);
      do
      let __do_lift ← f (n + 1) b x[n]
      loop (fun i b => f (i + 1) b) x (n + 1) this __do_lift

State before:
case refl
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
h₁ : n + 1 ≤ n + 1
h₂ : n ≤ n
b : β (n + 1)
⊢ (if h : n + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : n + 1 < n + 1);
      do
      let __do_lift ← f (n + 1) b (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) this __do_lift) =
    if h : n = n then pure (h ▸ b)
    else
      let_fun this := (_ : n < n);
      do
      let __do_lift ← f (n + 1) b x[n]
      loop (fun i b => f (i + 1) b) x (n + 1) this __do_lift
Tactic:
rw [dif_pos rfl, dif_pos rfl]
State after:
no goals

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
have : i < n := Nat.lt_of_le_of_ne h₂ h
State after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
Tactic:
simp only [dif_neg (Nat.ne_of_lt this), dif_neg (Nat.ne_of_lt (Nat.succ_lt_succ this))]
State after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift
Tactic:
rw [get_cons_succ]
State after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b x[i]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift

case hi₂
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ i < n

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b x[i]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift

case hi₂
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ i < n
Tactic:
exact bind_congr λ b => foldlMIdx.loop_cons_succ f a x (i+1) (Nat.succ_lt_succ this) this b
State after:
no goals