internlm/Lean-Github huggingface dataset:
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False
Tactic:
have h_range_size : (Array.range n).size = n := Array.range_size
Proof state after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False
Tactic:
simp only [Array.mkEmpty_eq, Array.range, flip] at h_range_size
Proof state after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
x_ge_n : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False
Tactic:
simp only [Array.mkEmpty_eq, h_range_size] at x_ge_n
Proof state after:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
x_ge_n : ¬x < n
⊢ False
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
h : x < n + 1
x_lt_n : x < n
ih : (Nat.fold (flip Array.push) n (Array.mkEmpty n))[x] = x
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
x_ge_n : ¬x < n
⊢ False
Tactic:
exact x_ge_n x_lt_n
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (Array.range (n + 1))[x] = x
Tactic:
simp only [Array.range, Nat.fold, flip, Array.get_push]
Proof state after:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Theorem: Misc.Array.range_idx
Proof state before:
case inr
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
⊢ (if h : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size then
      (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x]
    else n) =
    x
Tactic:
split
Proof state after:
case inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Theorem: Misc.Array.range_idx
Proof state before:
case inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x

case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. next x_lt_n =>
  exfalso
  have h_range_size : (Array.range n).size = n := Array.range_size
  simp only [Array.range, Array.mkEmpty_eq] at h_range_size
  simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
Proof state after:
case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Theorem: Misc.Array.range_idx
Proof state before:
case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
. rw [x_eq_n]
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case inr.isTrue
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x
Tactic:
next x_lt_n =>
exfalso
have h_range_size : (Array.range n).size = n := Array.range_size
simp only [Array.range, Array.mkEmpty_eq] at h_range_size
simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1)))[x] = x
Tactic:
exfalso
Proof state after:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ False
Tactic:
have h_range_size : (Array.range n).size = n := Array.range_size
Proof state after:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Array.range n).size = n
⊢ False
Tactic:
simp only [Array.range, Array.mkEmpty_eq] at h_range_size
Proof state after:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False
Theorem: Misc.Array.range_idx
Proof state before:
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
x_lt_n : x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
h_range_size : (Nat.fold (flip Array.push) n #[]).size = n
⊢ False
Tactic:
simp only [x_eq_n, Array.mkEmpty_eq, h_range_size, Nat.lt_irrefl] at x_lt_n
Proof state after:
no goals
Theorem: Misc.Array.range_idx
Proof state before:
case inr.isFalse
x n : Nat
ih : ∀ (h : x < n), (Array.range n)[x] = x
h : x < n + 1
x_eq_n : x = n
h✝ : ¬x < (Nat.fold (flip Array.push) n (Array.mkEmpty (n + 1))).size
⊢ n = x
Tactic:
rw [x_eq_n]
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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]
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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)
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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]
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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]
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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