Theorem: Misc.Array.mem_filter (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
a : Array α
p : α → Bool
⊢ ∀ (i : Nat) (i_in_bounds : i < a.size), p a[i] = true → a[i] ∈ (Array.filter p a 0).data
Tactic:
intro i i_in_bounds pai
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.filter p a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.filter p a 0).data
Tactic:
simp only [Array.filter]
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
Tactic:
let motive (idx : Nat) (acc : Array α) : Prop :=
  ∀ i : Nat, ∀ i_in_bounds : i < a.size, i < idx → p (a[i]'i_in_bounds) → (a[i]'i_in_bounds) ∈ acc.data
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
Tactic:
have h_base : motive 0 #[] := by
  intro i i_in_bounds i_lt_zero
  exact False.elim $ Nat.not_lt_zero i i_lt_zero
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
Tactic:
let f := (fun acc x => if p x = true then Array.push acc x else acc)
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
Tactic:
have f_def : f = (fun acc x => if p x = true then Array.push acc x else acc) := rfl
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
Tactic:
have h_inductive (idx : Fin a.size) (acc : Array α) (ih : motive idx.1 acc) : motive (idx.1 + 1) (f acc a[idx]) := by
  intro i i_in_bounds i_lt_idx_add_one
  rw [f_def]
  simp only [Fin.getElem_fin]
  intro pai
  rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
  . have h := ih i i_in_bounds i_lt_idx pai
    split
    . simp only [Array.push_data, mem_append, mem_singleton]
      exact Or.inl h
    . exact h
  . split
    . simp only [i_eq_idx, Array.push_data, mem_append, mem_singleton, or_true]
    . next pa_idx =>
      simp only [← i_eq_idx] at pa_idx
      exact False.elim $ pa_idx pai
State after:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
h_inductive : ∀ (idx : Fin a.size) (acc : Array α), motive (↑idx) acc → motive (↑idx + 1) (f acc a[idx])
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
h_inductive : ∀ (idx : Fin a.size) (acc : Array α), motive (↑idx) acc → motive (↑idx + 1) (f acc a[idx])
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
Tactic:
exact Array.foldl_induction motive h_base h_inductive i i_in_bounds i_in_bounds pai
State after:
no goals

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
⊢ motive 0 #[]
Tactic:
intro i i_in_bounds i_lt_zero
State after:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
i : Nat
i_in_bounds : i < a.size
i_lt_zero : i < 0
⊢ p a[i] = true → a[i] ∈ #[].data

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
i : Nat
i_in_bounds : i < a.size
i_lt_zero : i < 0
⊢ p a[i] = true → a[i] ∈ #[].data
Tactic:
exact False.elim $ Nat.not_lt_zero i i_lt_zero
State after:
no goals

State before:
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
⊢ motive (↑idx + 1) (f acc a[idx])
Tactic:
intro i i_in_bounds i_lt_idx_add_one
State after:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
⊢ p a[i] = true → a[i] ∈ (f acc a[idx]).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
⊢ p a[i] = true → a[i] ∈ (f acc a[idx]).data
Tactic:
rw [f_def]
State after:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
⊢ p a[i] = true → a[i] ∈ ((fun acc x => if p x = true then acc.push x else acc) acc a[idx]).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
⊢ p a[i] = true → a[i] ∈ ((fun acc x => if p x = true then acc.push x else acc) acc a[idx]).data
Tactic:
simp only [Fin.getElem_fin]
State after:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
⊢ p a[i] = true → a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
⊢ p a[i] = true → a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
intro pai
State after:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ i_lt_idx_add_one with i_lt_idx | i_eq_idx
State after:
case inl
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

case inr
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

State before:
case inl
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

case inr
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
. have h := ih i i_in_bounds i_lt_idx pai
  split
  . simp only [Array.push_data, mem_append, mem_singleton]
    exact Or.inl h
  . exact h
State after:
case inr
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

State before:
case inr
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
. split
  . simp only [i_eq_idx, Array.push_data, mem_append, mem_singleton, or_true]
  . next pa_idx =>
    simp only [← i_eq_idx] at pa_idx
    exact False.elim $ pa_idx pai
State after:
no goals

State before:
case inl
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
have h := ih i i_in_bounds i_lt_idx pai
State after:
case inl
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data

State before:
case inl
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
split
State after:
case inl.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : p a[↑idx] = true
⊢ a[i] ∈ (acc.push a[↑idx]).data

case inl.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data

State before:
case inl.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : p a[↑idx] = true
⊢ a[i] ∈ (acc.push a[↑idx]).data

case inl.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
. simp only [Array.push_data, mem_append, mem_singleton]
  exact Or.inl h
State after:
case inl.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data

State before:
case inl.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
. exact h
State after:
no goals

State before:
case inl.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : p a[↑idx] = true
⊢ a[i] ∈ (acc.push a[↑idx]).data
Tactic:
simp only [Array.push_data, mem_append, mem_singleton]
State after:
case inl.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : p a[↑idx] = true
⊢ a[i] ∈ acc.data ∨ a[i] = a[↑idx]

State before:
case inl.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : p a[↑idx] = true
⊢ a[i] ∈ acc.data ∨ a[i] = a[↑idx]
Tactic:
exact Or.inl h
State after:
no goals

State before:
case inl.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_lt_idx : i < ↑idx
h : a[i] ∈ acc.data
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
exact h
State after:
no goals

State before:
case inr
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
split
State after:
case inr.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : p a[↑idx] = true
⊢ a[i] ∈ (acc.push a[↑idx]).data

case inr.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data

State before:
case inr.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : p a[↑idx] = true
⊢ a[i] ∈ (acc.push a[↑idx]).data

case inr.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
. simp only [i_eq_idx, Array.push_data, mem_append, mem_singleton, or_true]
State after:
case inr.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data

State before:
case inr.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
. next pa_idx =>
  simp only [← i_eq_idx] at pa_idx
  exact False.elim $ pa_idx pai
State after:
no goals

State before:
case inr.isTrue
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : p a[↑idx] = true
⊢ a[i] ∈ (acc.push a[↑idx]).data
Tactic:
simp only [i_eq_idx, Array.push_data, mem_append, mem_singleton, or_true]
State after:
no goals

State before:
case inr.isFalse
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
next pa_idx =>
simp only [← i_eq_idx] at pa_idx
exact False.elim $ pa_idx pai
State after:
no goals

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
pa_idx : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
Tactic:
simp only [← i_eq_idx] at pa_idx
State after:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
pa_idx : ¬p a[i] = true
⊢ a[i] ∈ acc.data

State before:
α : Type u_1
a : Array α
p : α → Bool
i✝ : Nat
i_in_bounds✝ : i✝ < a.size
pai✝ : p a[i✝] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
pa_idx : ¬p a[i] = true
⊢ a[i] ∈ acc.data
Tactic:
exact False.elim $ pa_idx pai
State after:
no goals