internlm/Lean-Github huggingface dataset:
Theorem: FreeCMonoid.degree_mul
Proof state before:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }
Tactic:
rw [KVChain.cons_mergeWith_cons_flip hy₁x₁]
Proof state after:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.cons y₁ y₂ (KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys)
            (_ :
              KVChain.boundLeft y₁
                (KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys)) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }
Theorem: FreeCMonoid.degree_mul
Proof state before:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.cons y₁ y₂ (KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys)
            (_ :
              KVChain.boundLeft y₁
                (KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys)) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }
Tactic:
rw [degree_cons y₁ y₂, degree_cons y₁ y₂]
Proof state after:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ deg y₁ * y₂.val +
      degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + (deg y₁ * y₂.val + degree deg { vars := ys })
Theorem: FreeCMonoid.degree_mul
Proof state before:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ deg y₁ * y₂.val +
      degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + (deg y₁ * y₂.val + degree deg { vars := ys })
Tactic:
rw [h_ind_ys]
Proof state after:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ deg y₁ * y₂.val + (degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }) =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + (deg y₁ * y₂.val + degree deg { vars := ys })
Theorem: FreeCMonoid.degree_mul
Proof state before:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ deg y₁ * y₂.val + (degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }) =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + (deg y₁ * y₂.val + degree deg { vars := ys })
Tactic:
conv =>
  lhs; rw [←Nat.add_assoc, Nat.add_comm (deg y₁ * y₂.val), Nat.add_assoc]
Proof state after:
no goals
Theorem: Array.push_cons_eq_cons_push
Proof state before:
α : Type u
β : Type v
a b : α
as : Array α
⊢ push (cons a as) b = cons a (push as b)
Tactic:
dsimp [push, cons, List.concat]
Proof state after:
no goals
Theorem: Array.back'_eq_data_getLast
Proof state before:
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
l : List α
h : List.length l > 0
hc : l = []
⊢ False
Tactic:
cases hc
Proof state after:
case refl
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
h : List.length [] > 0
⊢ False
Theorem: Array.back'_eq_data_getLast
Proof state before:
case refl
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
h : List.length [] > 0
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: Array.back'_eq_data_getLast
Proof state before:
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h = List.getLast as.data (_ : as.data ≠ [])
Tactic:
rw [List.getLast_eq_get]
Proof state after:
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h =
    List.get as.data { val := List.length as.data - 1, isLt := (_ : List.length as.data - 1 < List.length as.data) }
Theorem: Array.back'_eq_data_getLast
Proof state before:
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h =
    List.get as.data { val := List.length as.data - 1, isLt := (_ : List.length as.data - 1 < List.length as.data) }
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.anyPairM_loop_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
stop : Nat
h : stop ≤ 0
i j : Nat
hij : i < j
⊢ anyPairM.loop #[] p stop h i j hij = pure false
Tactic:
cases Nat.eq_zero_of_le_zero h
Proof state after:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ anyPairM.loop #[] p 0 h i j hij = pure false
Theorem: Array.anyPairM_loop_empty
Proof state before:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ anyPairM.loop #[] p 0 h i j hij = pure false
Tactic:
unfold anyPairM.loop
Proof state after:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ (if hj : j < 0 then
      let_fun this := (_ : i < size #[]);
      let_fun this_1 := (_ : j < size #[]);
      do
      let __do_lift ← p #[][i] #[][j]
      if __do_lift = true then pure true else anyPairM.loop #[] p 0 h i (j + 1) (_ : i < Nat.succ j)
    else if i < 0 then anyPairM.loop #[] p 0 h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false) =
    pure false
Theorem: Array.anyPairM_loop_empty
Proof state before:
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ (if hj : j < 0 then
      let_fun this := (_ : i < size #[]);
      let_fun this_1 := (_ : j < size #[]);
      do
      let __do_lift ← p #[][i] #[][j]
      if __do_lift = true then pure true else anyPairM.loop #[] p 0 h i (j + 1) (_ : i < Nat.succ j)
    else if i < 0 then anyPairM.loop #[] p 0 h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false) =
    pure false
Tactic:
rw [dif_neg j.not_lt_zero, if_neg i.not_lt_zero]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1)
      (_ : Nat.succ i < Nat.succ j) =
    anyPairM.loop x p stop h i j hij
Tactic:
unfold anyPairM.loop
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
if hj : j < stop then
  rewrite [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
  apply bind_congr; intro b
  match b with
  | true => rfl
  | false =>
    simp only [ite_false]
    exact anyPairM_loop_cons_succ a x p h (.step hij)
else
  rewrite [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
  if hi : i < stop then
    rewrite [if_pos (Nat.succ_lt_succ hi), if_pos hi]
    exact anyPairM_loop_cons_succ a x p h (i+1).lt_succ_self
  else
    rw [if_neg (fun h' => hi (Nat.lt_of_succ_lt_succ h')), if_neg hi]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rewrite [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ (let_fun this := (_ : i + 1 < size (cons a x));
    let_fun this_1 := (_ : j + 1 < size (cons a x));
    do
    let __do_lift ← p (cons a x)[i + 1] (cons a x)[j + 1]
    if __do_lift = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
    let_fun this := (_ : i < size x);
    let_fun this_1 := (_ : j < size x);
    do
    let __do_lift ← p x[i] x[j]
    if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ (let_fun this := (_ : i + 1 < size (cons a x));
    let_fun this_1 := (_ : j + 1 < size (cons a x));
    do
    let __do_lift ← p (cons a x)[i + 1] (cons a x)[j + 1]
    if __do_lift = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
    let_fun this := (_ : i < size x);
    let_fun this_1 := (_ : j < size x);
    do
    let __do_lift ← p x[i] x[j]
    if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ ∀ (a_1 : Bool),
    (if a_1 = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
      if a_1 = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
⊢ ∀ (a_1 : Bool),
    (if a_1 = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
          (_ : i + 1 < Nat.succ (j + 1))) =
      if a_1 = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
intro b
Proof state after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ (if b = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if b = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ (if b = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if b = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
match b with
| true => rfl
| false =>
  simp only [ite_false]
  exact anyPairM_loop_cons_succ a x p h (.step hij)
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ (if true = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if true = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ (if false = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
        (_ : i + 1 < Nat.succ (j + 1))) =
    if false = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
simp only [ite_false]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
      (_ : i + 1 < Nat.succ (j + 1)) =
    anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
      (_ : i + 1 < Nat.succ (j + 1)) =
    anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
Tactic:
exact anyPairM_loop_cons_succ a x p h (.step hij)
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rewrite [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false