def tacticCompare : Lean.ParserDescr

Equations

• tacticCompare = Lean.ParserDescr.node `tacticCompare 1024 (Lean.ParserDescr.nonReservedSymbol "compare" false)

Venn diagram lemmas

theorem inter_eq_empty_of_subset {α : Type u_1} [Fintype α] [DecidableEq α] {A X Y : Finset α} (h₀ : Y ⊆ X) (h₁ : X ∩ A = ∅) : Y ∩ A = ∅

theorem inter_subset_restrict {α : Type u_1} [Fintype α] [DecidableEq α] {B X Y Z : Finset α} (h₀ : Y ⊆ X) (h₁ : X ∩ B ⊆ X ∩ Z) : Y ∩ B ⊆ Y ∩ Z

theorem inter_eq_restrict {α : Type u_1} [Fintype α] [DecidableEq α] {B X Y Z : Finset α} (h₀ : Y ⊆ X) (h₁ : X ∩ B = X ∩ Z) : Y ∩ B = Y ∩ Z

theorem eq_inter_inter {α : Type u_1} [Fintype α] [DecidableEq α] {U X Y Z : Finset α} (h₀ : U = X ∩ Y) (h₁ : U = X ∩ Z) : U = X ∩ (Y ∩ Z)

theorem inter_empty_of_restrict {α : Type u_1} [Fintype α] [DecidableEq α] {B X Y Z : Finset α} (h₀ : Y ⊆ X) (h₃ : Y ∩ B = ∅) (h₁ : X ∩ B = X ∩ Z) : Y ∩ Z = ∅

theorem inter_empty_of_restrict₂ {α : Type u_1} [Fintype α] [DecidableEq α] {A B : Finset α} (hAB : A ⊆ B) {X Y Z : Finset α} (hYX : Y ⊆ X) (h₀ : Y ∩ B = ∅) (h₁ : X ∩ Z ⊆ X ∩ A) : Y ∩ Z = ∅

theorem subset_same {α : Type u_1} [Fintype α] [DecidableEq α] {B X Y Z : Finset α} (h₀ : Y ∩ X = Z ∩ X) : X ∩ B ⊆ Y ↔ X ∩ B ⊆ Z

theorem eq_inter_inter_of_inter₀ {α : Type u_1} [Fintype α] [DecidableEq α] {B X Y Z : Finset α} (h₀ : X ∩ B = X ∩ Y) (h₁ : Y ∩ B = Y ∩ Z) : X ∩ Y ⊆ Z

theorem eq_inter_inter_of_inter {α : Type u_1} [Fintype α] [DecidableEq α] {B X Y Z : Finset α} (h₀ : X ∩ B = X ∩ Y) (h₁ : Y ∩ B = Y ∩ Z) : X ∩ Y = X ∩ (Y ∩ Z)

theorem inter_eq_empty₀ {α : Type u_1} [Fintype α] [DecidableEq α] {A X Y : Finset α} (h₁ : Y ∩ A = ∅) (h₀ : X ∩ A = X ∩ Y) : X ∩ Y = ∅

theorem inter_inter_eq_empty {α : Type u_1} [Fintype α] [DecidableEq α] {A X Y Z : Finset α} (h₁ : Y ∩ A = ∅) (h₀ : X ∩ A = X ∩ Y) : X ∩ (Y ∩ Z) = ∅

theorem inter_inter_eq_empty' {α : Type u_1} [Fintype α] [DecidableEq α] {A B y z x : Finset α} (h₂ : A ∩ y = ∅) (h₀ : y ∩ B = y ∩ z) (h₁ : z ∩ A = z ∩ x) : y ∩ (z ∩ x) = ∅

theorem subset_inter_within {α : Type u_1} [Fintype α] [DecidableEq α] {A X Y Z : Finset α} (h₀ : X ∩ A ⊆ Y) (h₁ : Y ∩ A ⊆ Z) : X ∩ A ⊆ Y ∩ Z

theorem inter_empty_of_inter_union_empty {α : Type u_1} [Fintype α] [DecidableEq α] {B Y Z : Finset α} (h₂ : (Y ∪ Z) ∩ B = ∅) : Y ∩ B = ∅

theorem forall_or_right_mem {α : Type u_1} (β : Set α) (F : α → Prop) (Q : Prop) : (∀ x ∈ β, F x ∨ Q) ↔ (∀ x ∈ β, F x) ∨ Q

theorem forall_or_right_union {U : Type u_1} {β : Set (Set U)} {X : Set U} : ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} = ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z = x} ∪ X

theorem exists_mem_of_ne_empty {U : Type u_1} {β : Set (Set U)} (h2 : β ≠ ∅) : ∃ (B : Set U), B ∈ β

theorem in_union_yet_in_none {U : Type u_1} {β : Set (Set U)} (h2 : β ≠ ∅) : ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z = x} = ∅

An element cannot belong to ⋃β, while for each particular Z ∈ β, not belonging to that one.

theorem in_union_yet_in_none' {U : Type u_1} {β : Set (Set U)} (X : Set U) (h2 : β ≠ ∅) : X = ⋂₀ {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x}

theorem not_empty {U : Type u_1} {β : Set (Set U)} (X : Set U) (h2 : β ≠ ∅) : {x : Set U | ∃ Z ∈ β, ⋃₀ β \ Z ∪ X = x} ≠ ∅

theorem eq_of_sdiff_empty {n : ℕ} {A B : Finset (Fin n)} (H₀ : Aᶜ ∩ B = ∅) (H₁ : Bᶜ ∩ A = ∅) : B = A

theorem some_like_given'' {n : ℕ} {A : Finset (Fin n)} {P : Finset (Fin n) → Prop} [DecidablePred P] (h : P A) : {Y : Finset (Fin n) | P Y} ≠ ∅

theorem some_like_given {n : ℕ} {A : Finset (Fin n)} {P : Finset (Fin n) → Finset (Fin n)} : ∅ ≠ {Y : Finset (Fin n) | P Y = P A}

theorem in_neither {n : ℕ} {A B : Finset (Fin n)} (h₂ : Bᶜ ∩ Aᶜ ≠ ∅) : ¬Aᶜ ∩ B = Aᶜ ∩ Bᶜ

def my₀ : Finset (Fin 0) → Finset (Finset (Fin 0))

Equations

• my₀ x✝ = ∅

def my₁ : Finset (Fin 0) → Finset (Finset (Fin 0))

Equations

• my₁ x✝ = {∅}

theorem all_are_my (ob : Finset (Fin 0) → Finset (Finset (Fin 0))) : ob = my₀ ∨ ob = my₁

theorem nonemptyFin1 {Q : Finset (Fin 1)} (h : Q ≠ ∅) : Q = {0}

def mutually_generic {U : Type u_1} [Fintype U] (X Y : Finset U) : Prop

Equations

• mutually_generic X Y = (X ∩ Y ≠ ∅ ∧ X \ Y ≠ ∅ ∧ Y \ X ≠ ∅ ∧ (X ∪ Y)ᶜ ≠ ∅)

def weakly_mutually_generic {U : Type u_1} [Fintype U] (X Y : Finset U) : Prop

Equations

• weakly_mutually_generic X Y = (X ≠ ∅ ∧ Y \ X ≠ ∅)

theorem implies_weakly {U : Type u_1} [Fintype U] {A B : Finset U} (h₁ : mutually_generic A B) : weakly_mutually_generic A B

theorem gen₀₀ {U : Type u_1} [Fintype U] {A B : Finset U} (h₁ : weakly_mutually_generic A B) : Aᶜ ∩ (A ∪ B) ≠ ∅

theorem gen₁₁ {U : Type u_1} [Fintype U] {A B : Finset U} (hg : weakly_mutually_generic A B) : (A ∪ Bᶜ) ∩ A ≠ ∅

theorem differenceCap {U : Type u_1} [Fintype U] (A B : Finset U) : B ∩ Aᶜ = (A ∪ B) ∩ Aᶜ

theorem union_diff_singleton {n : ℕ} (X Y : Finset (Fin n)) {a : Fin n} (ha : a ∈ X) : (X ∪ Y) \ {a} = (X ∪ Y) \ X ∪ X \ {a}

theorem pair_venn {n : ℕ} (X Y : Finset (Fin n)) (a : Fin n) (ha : a ∈ X) (b : Fin n) (hb : b ∈ Y) : {a, b} = (X ∪ Y) \ ((X ∪ Y) \ {a} ∩ ((X ∪ Y) \ {b}))

theorem union_sdiff_singleton {n : ℕ} {X Y : Finset (Fin n)} {a : Fin n} (ha : a ∈ X) : (X ∪ Y) \ {a} = (X ∪ Y) \ X ∪ X \ {a}

theorem two_in_sdiff {n : ℕ} (X Y : Finset (Fin n)) (a i : Fin n) (ha : a ∈ X \ Y) (hi₀ : i ∈ X) (hi₁ : ¬i = a) (H₀ : i ∉ Y) : ¬(X \ (X ∩ Y)).card ≤ 1

theorem two_in_sdiff' {n : ℕ} (X Y : Finset (Fin n)) (a i : Fin n) (ha : a ∈ X \ Y) (hi₀ : i ∈ X) (hi₁ : ¬i = a) (H₀ : i ∉ Y) : ¬(X \ Y).card ≤ 1

theorem all_or_almost {n : ℕ} {a : Fin n} {X Y : Finset (Fin n)} (h₁ : X \ {a} ⊆ X ∩ Y) : X ∩ Y = X ∨ X ∩ Y = X \ {a}

A simple Venn diagram lemma.

theorem venn_singleton {n : ℕ} (a : Fin n) (Y : Finset (Fin n)) : a ∈ Y ↔ ¬{a} ∩ Y = ∅