internlm/Lean-Github huggingface dataset:
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
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
Tactic:
have h := ih i i_in_bounds i_lt_idx pai
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
h : a[i] ∈ acc.data
⊢ 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
h : a[i] ∈ acc.data
⊢ a[i] ∈ (if p a[↑idx] = true then acc.push a[↑idx] else acc).data
Tactic:
split
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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]
Proof 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]
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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]
Proof 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
Theorem: Misc.Array.mem_filter
Proof 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
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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]
Proof state after:
no goals
Theorem: Misc.Array.mem_filter
Proof 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
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
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
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
i_eq_idx : i = ↑idx
pa_idx : ¬p a[i] = true
⊢ a[i] ∈ 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
i_eq_idx : i = ↑idx
pa_idx : ¬p a[i] = true
⊢ a[i] ∈ acc.data
Tactic:
exact False.elim $ pa_idx pai
Proof state after:
no goals
Theorem: Misc.Array.set!_preserves_size
Proof state before:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (a.set! i x).size = a.size
Tactic:
rw [Array.set!, Array.setD]
Proof state after:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (if h : i < a.size then a.set ⟨i, h⟩ x else a).size = a.size
Theorem: Misc.Array.set!_preserves_size
Proof state before:
α : Type u_1
a : Array α
i : Nat
x : α
⊢ (if h : i < a.size then a.set ⟨i, h⟩ x else a).size = a.size
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : i < a.size
⊢ (a.set ⟨i, h✝⟩ x).size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : ¬i < a.size
⊢ a.size = a.size
Theorem: Misc.Array.set!_preserves_size
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : i < a.size
⊢ (a.set ⟨i, h✝⟩ x).size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
. simp only [Array.size_set]
Proof state after:
case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : ¬i < a.size
⊢ a.size = a.size
Theorem: Misc.Array.set!_preserves_size
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
. rfl
Proof state after:
no goals
Theorem: Misc.Array.set!_preserves_size
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : i < a.size
⊢ (a.set ⟨i, h✝⟩ x).size = a.size
Tactic:
simp only [Array.size_set]
Proof state after:
no goals
Theorem: Misc.Array.set!_preserves_size
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
x : α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
rfl
Proof state after:
no goals
Theorem: Misc.Array.modify_preserves_size
Proof state before:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ (a.modify i f).size = a.size
Tactic:
simp only [Array.modify, Array.modifyM, Id.bind_eq, Id.pure_eq, Id.run]
Proof state after:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a) = a.size
Theorem: Misc.Array.modify_preserves_size
Proof state before:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a) = a.size
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Theorem: Misc.Array.modify_preserves_size
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).size = a.size

case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
. simp only [Array.size_set]
Proof state after:
case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Theorem: Misc.Array.modify_preserves_size
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
. rfl
Proof state after:
no goals
Theorem: Misc.Array.modify_preserves_size
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).size = a.size
Tactic:
simp only [Array.size_set]
Proof state after:
no goals
Theorem: Misc.Array.modify_preserves_size
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
f : α → α
h✝ : ¬i < a.size
⊢ a.size = a.size
Tactic:
rfl
Proof state after:
no goals
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < (a.modify i f).size
Tactic:
rw [Array.modify_preserves_size]
Proof state after:
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < a.size
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < a.size
Tactic:
exact i_in_bounds
Proof state after:
no goals
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ (a.modify i f)[i] = f a[i]
Tactic:
simp only [Array.modify, Array.modifyM, Id.bind_eq, Id.pure_eq, Id.run]
Proof state after:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[i] = f a[i]
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[i] = f a[i]
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
. simp only [getElem]
  have lhs_rw := Array.get_set a ⟨i, i_in_bounds⟩ i i_in_bounds (f (Array.get a ⟨i, i_in_bounds⟩))
  simp only [getElem] at lhs_rw
  rw [lhs_rw]
  simp only [Array.get_eq_getElem, ite_true]
Proof state after:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Theorem: Misc.Array.get_modify_at_idx
Proof state before:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
. next i_out_of_bounds =>
  exfalso
  exact i_out_of_bounds i_in_bounds
Proof state after:
no goals