internlm/Lean-Github huggingface dataset:
Theorem: Fin.all_zero
Proof state before:
p : Fin 0 → Bool
⊢ Fin.all p = true
Tactic:
simp [Fin.all]
Proof state after:
no goals
Theorem: Fin.all_succ
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
⊢ Fin.all p = (p 0 && Fin.all (p ∘ succ))
Tactic:
simp [Fin.all, Fin.foldr_succ]
Proof state after:
no goals
Theorem: Fin.forall_eq_true_of_all_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.all p = true
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = true
Tactic:
rw [Fin.all, Fin.foldr_succ, Bool.and_eq_true] at h
Proof state after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∧ foldr n (fun i v => p i.succ && v) true = true
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = true
Theorem: Fin.forall_eq_true_of_all_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∧ foldr n (fun i v => p i.succ && v) true = true
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = true
Tactic:
exact h.left
Proof state after:
no goals
Theorem: Fin.forall_eq_true_of_all_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.all p = true
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = true
Tactic:
rw [Fin.all, Fin.foldr_succ, Bool.and_eq_true] at h
Proof state after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∧ foldr n (fun i v => p i.succ && v) true = true
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = true
Theorem: Fin.forall_eq_true_of_all_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∧ foldr n (fun i v => p i.succ && v) true = true
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = true
Tactic:
exact forall_eq_true_of_all_eq_true h.right ⟨i, Nat.lt_of_succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_false_of_all_eq_false
Proof state before:
p : Fin 0 → Bool
h : Fin.all p = false
⊢ ∃ i, p i = false
Tactic:
simp at h
Proof state after:
no goals
Theorem: Fin.exists_eq_false_of_all_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.all p = false
⊢ ∃ i, p i = false
Tactic:
rw [Fin.all, Fin.foldr_succ, Bool.and_eq_false_iff] at h
Proof state after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∨ foldr n (fun i v => p i.succ && v) true = false
⊢ ∃ i, p i = false
Theorem: Fin.exists_eq_false_of_all_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∨ foldr n (fun i v => p i.succ && v) true = false
⊢ ∃ i, p i = false
Tactic:
match h with
| .inl h => exists ⟨0, Nat.zero_lt_succ n⟩
| .inr h => match exists_eq_false_of_all_eq_false h with
  | ⟨⟨i,hi⟩,hp⟩ => exists ⟨i+1, Nat.succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_false_of_all_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = false ∨ foldr n (fun i v => p i.succ && v) true = false
h : p 0 = false
⊢ ∃ i, p i = false
Tactic:
exists ⟨0, Nat.zero_lt_succ n⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_false_of_all_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = false ∨ foldr n (fun i v => p i.succ && v) true = false
h : foldr n (fun i v => p i.succ && v) true = false
⊢ ∃ i, p i = false
Tactic:
match exists_eq_false_of_all_eq_false h with
| ⟨⟨i,hi⟩,hp⟩ => exists ⟨i+1, Nat.succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_false_of_all_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = false ∨ foldr n (fun i v => p i.succ && v) true = false
h : foldr n (fun i v => p i.succ && v) true = false
i : Nat
hi : i < n
hp : p ⟨i, hi⟩.succ = false
⊢ ∃ i, p i = false
Tactic:
exists ⟨i+1, Nat.succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.decide_forall_eq_all
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
⊢ decide (∀ (i : Fin n), p i) = Fin.all fun i => decide (p i)
Tactic:
match h : Fin.all fun i => decide (p i) with
| true =>
  have h := forall_eq_true_of_all_eq_true h
  apply decide_eq_true
  intro i
  apply of_decide_eq_true
  exact h i
| false =>
  match exists_eq_false_of_all_eq_false h with
  | ⟨i, hi⟩ =>
    have hi := of_decide_eq_false hi
    apply decide_eq_false
    intro h
    apply hi
    exact h i
Proof state after:
no goals
Theorem: Fin.decide_forall_eq_all
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = true
⊢ decide (∀ (i : Fin n), p i) = true
Tactic:
have h := forall_eq_true_of_all_eq_true h
Proof state after:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
⊢ decide (∀ (i : Fin n), p i) = true
Theorem: Fin.decide_forall_eq_all
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
⊢ decide (∀ (i : Fin n), p i) = true
Tactic:
apply decide_eq_true
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
⊢ ∀ (i : Fin n), p i
Theorem: Fin.decide_forall_eq_all
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
⊢ ∀ (i : Fin n), p i
Tactic:
intro i
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
i : Fin n
⊢ p i
Theorem: Fin.decide_forall_eq_all
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
i : Fin n
⊢ p i
Tactic:
apply of_decide_eq_true
Proof state after:
case a.a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
i : Fin n
⊢ decide (p i) = true
Theorem: Fin.decide_forall_eq_all
Proof state before:
case a.a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = true
h : ∀ (i : Fin n), decide (p i) = true
i : Fin n
⊢ decide (p i) = true
Tactic:
exact h i
Proof state after:
no goals
Theorem: Fin.decide_forall_eq_all
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
⊢ decide (∀ (i : Fin n), p i) = false
Tactic:
match exists_eq_false_of_all_eq_false h with
| ⟨i, hi⟩ =>
  have hi := of_decide_eq_false hi
  apply decide_eq_false
  intro h
  apply hi
  exact h i
Proof state after:
no goals
Theorem: Fin.decide_forall_eq_all
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi : decide (p i) = false
⊢ decide (∀ (i : Fin n), p i) = false
Tactic:
have hi := of_decide_eq_false hi
Proof state after:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
⊢ decide (∀ (i : Fin n), p i) = false
Theorem: Fin.decide_forall_eq_all
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
⊢ decide (∀ (i : Fin n), p i) = false
Tactic:
apply decide_eq_false
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
⊢ ¬∀ (i : Fin n), p i
Theorem: Fin.decide_forall_eq_all
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
⊢ ¬∀ (i : Fin n), p i
Tactic:
intro h
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
h : ∀ (i : Fin n), p i
⊢ False
Theorem: Fin.decide_forall_eq_all
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
h : ∀ (i : Fin n), p i
⊢ False
Tactic:
apply hi
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
h : ∀ (i : Fin n), p i
⊢ p i
Theorem: Fin.decide_forall_eq_all
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∀ (i : Fin n), p i)
h✝ : (Fin.all fun i => decide (p i)) = false
i : Fin n
hi✝ : decide (p i) = false
hi : ¬p i
h : ∀ (i : Fin n), p i
⊢ p i
Tactic:
exact h i
Proof state after:
no goals
Theorem: Fin.any_zero
Proof state before:
p : Fin 0 → Bool
⊢ Fin.any p = false
Tactic:
simp [Fin.any]
Proof state after:
no goals
Theorem: Fin.any_succ
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
⊢ Fin.any p = (p 0 || Fin.any (p ∘ succ))
Tactic:
simp [Fin.any, Fin.foldr_succ]
Proof state after:
no goals
Theorem: Fin.exists_eq_true_of_any_eq_true
Proof state before:
x✝ : Fin 0 → Bool
h : Fin.any x✝ = true
⊢ ∃ i, x✝ i = true
Tactic:
simp at h
Proof state after:
no goals
Theorem: Fin.exists_eq_true_of_any_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.any p = true
⊢ ∃ i, p i = true
Tactic:
rw [Fin.any, Fin.foldr_succ, Bool.or_eq_true] at h
Proof state after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
⊢ ∃ i, p i = true
Theorem: Fin.exists_eq_true_of_any_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
⊢ ∃ i, p i = true
Tactic:
match h with
| .inl h => exists ⟨0, Nat.zero_lt_succ n⟩
| .inr h => match exists_eq_true_of_any_eq_true h with
  | ⟨⟨i,hi⟩,hp⟩ => exists ⟨i+1, Nat.succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_true_of_any_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
h : p 0 = true
⊢ ∃ i, p i = true
Tactic:
exists ⟨0, Nat.zero_lt_succ n⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_true_of_any_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
h : foldr n (fun i v => p i.succ || v) false = true
⊢ ∃ i, p i = true
Tactic:
match exists_eq_true_of_any_eq_true h with
| ⟨⟨i,hi⟩,hp⟩ => exists ⟨i+1, Nat.succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.exists_eq_true_of_any_eq_true
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h✝ : p 0 = true ∨ foldr n (fun i v => p i.succ || v) false = true
h : foldr n (fun i v => p i.succ || v) false = true
i : Nat
hi : i < n
hp : p ⟨i, hi⟩.succ = true
⊢ ∃ i, p i = true
Tactic:
exists ⟨i+1, Nat.succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.forall_eq_false_of_any_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.any p = false
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = false
Tactic:
rw [Fin.any, Fin.foldr_succ, Bool.or_eq_false_iff] at h
Proof state after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∧ foldr n (fun i v => p i.succ || v) false = false
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = false
Theorem: Fin.forall_eq_false_of_any_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∧ foldr n (fun i v => p i.succ || v) false = false
isLt✝ : 0 < n + 1
⊢ p ⟨0, isLt✝⟩ = false
Tactic:
exact h.left
Proof state after:
no goals
Theorem: Fin.forall_eq_false_of_any_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : Fin.any p = false
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = false
Tactic:
rw [Fin.any, Fin.foldr_succ, Bool.or_eq_false_iff] at h
Proof state after:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∧ foldr n (fun i v => p i.succ || v) false = false
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = false
Theorem: Fin.forall_eq_false_of_any_eq_false
Proof state before:
n : Nat
p : Fin (n + 1) → Bool
h : p 0 = false ∧ foldr n (fun i v => p i.succ || v) false = false
i : Nat
hi : i + 1 < n + 1
⊢ p ⟨i + 1, hi⟩ = false
Tactic:
exact forall_eq_false_of_any_eq_false h.right ⟨i, Nat.lt_of_succ_lt_succ hi⟩
Proof state after:
no goals
Theorem: Fin.decide_exists_eq_any
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
⊢ decide (∃ i, p i) = Fin.any fun i => decide (p i)
Tactic:
match h : Fin.any fun i => decide (p i) with
| true =>
  match exists_eq_true_of_any_eq_true h with
  | ⟨i, hi⟩ =>
    have hi := of_decide_eq_true hi
    apply decide_eq_true
    exists i
| false =>
  have h := forall_eq_false_of_any_eq_false h
  apply decide_eq_false
  intro ⟨i, hi⟩
  absurd hi
  apply of_decide_eq_false
  exact h i
Proof state after:
no goals
Theorem: Fin.decide_exists_eq_any
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
⊢ decide (∃ i, p i) = true
Tactic:
match exists_eq_true_of_any_eq_true h with
| ⟨i, hi⟩ =>
  have hi := of_decide_eq_true hi
  apply decide_eq_true
  exists i
Proof state after:
no goals
Theorem: Fin.decide_exists_eq_any
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi : decide (p i) = true
⊢ decide (∃ i, p i) = true
Tactic:
have hi := of_decide_eq_true hi
Proof state after:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ decide (∃ i, p i) = true
Theorem: Fin.decide_exists_eq_any
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ decide (∃ i, p i) = true
Tactic:
apply decide_eq_true
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ ∃ i, p i
Theorem: Fin.decide_exists_eq_any
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = true
i : Fin n
hi✝ : decide (p i) = true
hi : p i
⊢ ∃ i, p i
Tactic:
exists i
Proof state after:
no goals
Theorem: Fin.decide_exists_eq_any
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h : (Fin.any fun i => decide (p i)) = false
⊢ decide (∃ i, p i) = false
Tactic:
have h := forall_eq_false_of_any_eq_false h
Proof state after:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ decide (∃ i, p i) = false
Theorem: Fin.decide_exists_eq_any
Proof state before:
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ decide (∃ i, p i) = false
Tactic:
apply decide_eq_false
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ ¬∃ i, p i
Theorem: Fin.decide_exists_eq_any
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
⊢ ¬∃ i, p i
Tactic:
intro ⟨i, hi⟩
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ False
Theorem: Fin.decide_exists_eq_any
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ False
Tactic:
absurd hi
Proof state after:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ ¬p i
Theorem: Fin.decide_exists_eq_any
Proof state before:
case a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ ¬p i
Tactic:
apply of_decide_eq_false
Proof state after:
case a.a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ decide (p i) = false
Theorem: Fin.decide_exists_eq_any
Proof state before:
case a.a
n : Nat
p : Fin n → Prop
inst✝¹ : DecidablePred p
inst✝ : Decidable (∃ i, p i)
h✝ : (Fin.any fun i => decide (p i)) = false
h : ∀ (i : Fin n), decide (p i) = false
i : Fin n
hi : p i
⊢ decide (p i) = false
Tactic:
exact h i
Proof state after:
no goals
Theorem: List.Index.find_some
Proof state before:
case nil
α✝ : Type u_1
p : [].Index → Bool
i : [].Index
⊢ Index.find? p = some i → p i = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.find_some
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
⊢ Index.find? p = some i → p i = true
Tactic:
intro heq
Proof state after:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = some i
⊢ p i = true
Theorem: List.Index.find_some
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = some i
h : p head = true
⊢ p i = true
Tactic:
simp only [Index.find?, h, cond] at heq
Proof state after:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = true
heq : some head = some i
⊢ p i = true
Theorem: List.Index.find_some
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = true
heq : some head = some i
⊢ p i = true
Tactic:
rw [←Option.some.inj heq, h]
Proof state after:
no goals
Theorem: List.Index.find_some
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = some i
h : p head = false
⊢ p i = true
Tactic:
simp only [Index.find?, h, cond, Option.map] at heq
Proof state after:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    some i
⊢ p i = true
Theorem: List.Index.find_some
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
heq :
  (match Index.find? fun i => p i.tail with
    | some x_1 => some x_1.tail
    | none => none) =
    some i
⊢ p i = true
Tactic:
split at heq
Proof state after:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = some i
⊢ p i = true

case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
opt✝ : Option xs.Index
heq✝ : (Index.find? fun i => p i.tail) = none
heq : none = some i
⊢ p i = true
Theorem: List.Index.find_some
Proof state before:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
opt✝ : Option xs.Index
x✝ : xs.Index
heq✝ : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = some i
⊢ p i = true
Tactic:
next h => rw [←Option.some.inj heq, ih _ h]
Proof state after:
no goals
Theorem: List.Index.find_some
Proof state before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h✝ : p head = false
opt✝ : Option xs.Index
x✝ : xs.Index
h : (Index.find? fun i => p i.tail) = some x✝
heq : some x✝.tail = some i
⊢ p i = true
Tactic:
rw [←Option.some.inj heq, ih _ h]
Proof state after:
no goals
Theorem: List.Index.find_some
Proof state before:
case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = some i → p i = true
p : (x :: xs).Index → Bool
i : (x :: xs).Index
h : p head = false
opt✝ : Option xs.Index
heq✝ : (Index.find? fun i => p i.tail) = none
heq : none = some i
⊢ p i = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.find_none
Proof state before:
case nil
α✝ : Type u_1
p : [].Index → Bool
i : [].Index
⊢ Index.find? p = none → p i = false
Tactic:
cases i
Proof state after:
no goals
Theorem: List.Index.find_none
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
⊢ Index.find? p = none → p i = false
Tactic:
intro heq
Proof state after:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = none
⊢ p i = false
Theorem: List.Index.find_none
Proof state before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq : Index.find? p = none
⊢ p i = false
Tactic:
simp only [Index.find?, cond, Option.map] at heq
Proof state after:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {p : xs.Index → Bool} (i : xs.Index), Index.find? p = none → p i = false
p : (x :: xs).Index → Bool
i : (x :: xs).Index
heq :
  (match p head with
    | true => some head
    | false =>
      match Index.find? fun i => p i.tail with
      | some x_1 => some x_1.tail
      | none => none) =
    none
⊢ p i = false