α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
⊢ sizeOf a < sizeOf as
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h : a ∈ as
⊢ sizeOf a < sizeOf as
simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
no goals
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
⊢ sizeOf a < sizeOf as
apply aux 0 h
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h :
  (if hlt : j < size as then
      let_fun this := (_ : j < size as);
      do
      let __do_lift ← decide (a = as[j])
      if __do_lift = true then pure true
        else anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1)
    else pure false) =
    true
⊢ sizeOf a < sizeOf as
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) j = true
⊢ sizeOf a < sizeOf as
unfold anyM.loop at h
case inl
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : j < size as
h :
  (let_fun this := (_ : j < size as);
    do
    let __do_lift ← decide (a = as[j])
    if __do_lift = true then pure true
      else anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1)) =
    true
⊢ sizeOf a < sizeOf as

case inr
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : ¬j < size as
h : False
⊢ sizeOf a < sizeOf as
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h :
  (if hlt : j < size as then
      let_fun this := (_ : j < size as);
      do
      let __do_lift ← decide (a = as[j])
      if __do_lift = true then pure true
        else anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1)
    else pure false) =
    true
⊢ sizeOf a < sizeOf as
split at h
case inl
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : j < size as
h :
  (if a = as[j] then true else anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1)) = true
⊢ sizeOf a < sizeOf as
case inl
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : j < size as
h :
  (let_fun this := (_ : j < size as);
    do
    let __do_lift ← decide (a = as[j])
    if __do_lift = true then pure true
      else anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1)) =
    true
⊢ sizeOf a < sizeOf as
simp [Bind.bind, pure] at h
case inl.inl
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : a = as[j]
h : true = true
⊢ sizeOf a < sizeOf as

case inl.inr
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
⊢ sizeOf a < sizeOf as
case inl
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : j < size as
h :
  (if a = as[j] then true else anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1)) = true
⊢ sizeOf a < sizeOf as
split at h
case inl.inr
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
⊢ sizeOf a < sizeOf as
case inl.inl
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : a = as[j]
h : true = true
⊢ sizeOf a < sizeOf as

case inl.inr
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
⊢ sizeOf a < sizeOf as
next he => subst a; apply sizeOf_get_lt
no goals
case inl.inr
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
⊢ sizeOf a < sizeOf as
next => have ih := aux (j+1) h; assumption
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
j : Nat
h✝¹ : j < size as
h✝ : true = true
h : anyM.loop (fun b => decide (as[j] = b)) as (size as) (_ : size as ≤ size as) 0 = true
⊢ sizeOf as[j] < sizeOf as
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : j < size as
he : a = as[j]
h : true = true
⊢ sizeOf a < sizeOf as
subst a
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
j : Nat
h✝¹ : j < size as
h✝ : true = true
h : anyM.loop (fun b => decide (as[j] = b)) as (size as) (_ : size as ≤ size as) 0 = true
⊢ sizeOf as[j] < sizeOf as
apply sizeOf_get_lt
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
ih : sizeOf a < sizeOf as
⊢ sizeOf a < sizeOf as
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
⊢ sizeOf a < sizeOf as
have ih := aux (j+1) h
no goals
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝² : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝¹ : j < size as
h✝ : ¬a = as[j]
h : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) (j + 1) = true
ih : sizeOf a < sizeOf as
⊢ sizeOf a < sizeOf as
assumption
no goals
case inr
α : Type u_1
a : α
inst✝¹ : DecidableEq α
inst✝ : SizeOf α
as : Array α
h✝¹ : anyM.loop (fun b => decide (a = b)) as (size as) (_ : size as ≤ size as) 0 = true
j : Nat
h✝ : ¬j < size as
h : False
⊢ sizeOf a < sizeOf as
contradiction