<commit_before>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>
-/
import data.list.basic

namespace list

/--
tfae: The Following (propositions) Are Equivalent.

The `tfae_have` and `tfae_finish` tactics can be useful in proofs with `tfae` goals.
-/
def tfae (l : list Prop) : Prop := ∀ x ∈ l, ∀ y ∈ l, x ↔ y

theorem tfae_nil : tfae [] := forall_mem_nil _
theorem tfae_singleton (p) : tfae [p] := by simp [tfae, -eq_iff_iff]<commit_msg>docs(data/list/tfae): add module docstring (#8040)<commit_after>/-
Copyright (c) 2018 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>, <NAME>
-/
import data.list.basic

/-!
# The Following Are Equivalent

This file allows to state that all propositions in a list are equivalent. It is used by
`tactic.tfae`.
`tfae l` means `∀ x ∈ l, ∀ y ∈ l, x ↔ y`. This is equivalent to `pairwise (↔) l`.
-/

namespace list

/--
tfae: The Following (propositions) Are Equivalent.

The `tfae_have` and `tfae_finish` tactics can be useful in proofs with `tfae` goals.
-/
def tfae (l : list Prop) : Prop := ∀ x ∈ l, ∀ y ∈ l, x ↔ y

theorem tfae_nil : tfae [] := forall_mem_nil _
theorem tfae_singleton (p) : tfae [p] := by simp [tfae, -eq_iff_iff]
{'fraction_non_alphanumeric': 0.13046757164404224, 'fraction_numerical': 0.012066365007541479, 'mean_word_length': 3.7392857142857143, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4976129', 'n_tokens_mistral': 513, 'n_tokens_neox': 480, 'n_words': 196}