ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>NeZero n<VAR>x : ZMod n<GOAL>x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n
<VAR>n : ℕ<VAR>NeZero n<VAR>x : ZMod n<VAR>y : ℤ<GOAL>x.valMinAbs = y ↔ x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
<VAR>n : ℕ<VAR>NeZero n<VAR>x : ZMod n<GOAL>x.valMinAbs.natAbs ≤ n / 2
<VAR>n : ℕ<GOAL>ZMod.valMinAbs 0 = 0
<VAR>n : ℕ<VAR>x : ZMod n<GOAL>x.valMinAbs = 0 ↔ x = 0
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a
<VAR>n : ℕ<VAR>a : ZMod n<VAR>ha : 2 * a.val ≠ n<GOAL>(-a).valMinAbs = -a.valMinAbs
<VAR>n : ℕ<VAR>a : ZMod n<GOAL>(-a).valMinAbs.natAbs = a.valMinAbs.natAbs
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ZMod n<GOAL>↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>hpq : p ≠ q<GOAL>↑q ≠ 0
<VAR>n : ℕ<VAR>hpos : NeZero n<VAR>a : ZMod n<GOAL>a.valMinAbs.natAbs = min a.val (n - a.val)
<VAR>n a : ℕ<VAR>ha : a ≤ n / 2<GOAL>(↑a).valMinAbs = ↑a
<VAR>n a : ℕ<VAR>ha : n / 2 < a<VAR>ha' : a < n<GOAL>(↑a).valMinAbs = ↑a - ↑n
<VAR>n a : ℕ<VAR>NeZero n<GOAL>(↑a).valMinAbs = ↑a ↔ a ≤ n / 2
<VAR>n : ℕ<VAR>x y : ℤ<VAR>he : ↑x = ↑y<VAR>hl : x.natAbs ≤ n / 2<GOAL>x.natAbs ≤ y.natAbs
<VAR>n : ℕ<VAR>a b : ZMod n<GOAL>(a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>h : a ≠ 0<GOAL>a * a⁻¹ = 1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : ZMod n →+* R<GOAL>f = g
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>f : R →+* ZMod n<VAR>k : ZMod n<GOAL>f k.cast = k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>f : R →+* ZMod n<GOAL>Function.RightInverse ZMod.cast ⇑f
<VAR>n : ℕ<VAR>R : Type u_1<VAR>Ring R<VAR>f : R →+* ZMod n<GOAL>Function.Surjective ⇑f
<VAR>n : ℕ<GOAL>ZMod.castHom ⋯ (ZMod n) = RingHom.id (ZMod n)
<VAR>n m d : ℕ<VAR>hm : n ∣ m<VAR>hd : m ∣ d<GOAL>(ZMod.castHom hm (ZMod n)).comp (ZMod.castHom hd (ZMod m)) = ZMod.castHom ⋯ (ZMod n)
<VAR>n : ℕ<VAR>A : Type u_2<VAR>AddGroup A<VAR>f : { f // f ↑n = 0 }<VAR>x : ℤ<GOAL>((ZMod.lift n) f) ↑x = ↑f x
<VAR>n : ℕ<VAR>A : Type u_2<VAR>AddGroup A<VAR>f : { f // f ↑n = 0 }<VAR>x : ℤ<GOAL>((ZMod.lift n) f) ((Int.castAddHom (ZMod n)) x) = ↑f x
<VAR>n : ℕ<VAR>A : Type u_2<VAR>AddGroup A<VAR>f : { f // f ↑n = 0 }<GOAL>⇑((ZMod.lift n) f) ∘ Int.cast = ⇑↑f
<VAR>n : ℕ<VAR>A : Type u_2<VAR>AddGroup A<VAR>f : { f // f ↑n = 0 }<GOAL>((ZMod.lift n) f).comp (Int.castAddHom (ZMod n)) = ↑f
<VAR>n : ℕ<VAR>A : Type u_2<VAR>AddGroup A<VAR>f : { f // f ↑n = 0 }<GOAL>Function.Injective ⇑((ZMod.lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0
<VAR>α : Type u_1<VAR>AddGroup α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>n • (↑n)⁻¹.val • a = a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>(↑n)⁻¹.val • n • a = a
<VAR>α : Type u_1<VAR>Group α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>(a ^ (↑n)⁻¹.val) ^ n = a
<VAR>α : Type u_1<VAR>Group α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>(a ^ n) ^ (↑n)⁻¹.val = a
<VAR>m k : ℕ<GOAL>(Set.range fun n => m * n + k) = {n | ↑n = ↑k ∧ k ≤ n}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<VAR>c : α<GOAL>c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>↑(s ⊻ t) = ↑s ⊻ ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(s ⊻ t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(s ⊻ t).card = s.card * t.card ↔ Set.InjOn (fun x => x.1 ⊔ x.2) (↑s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s ⊻ t₁ ⊆ s ⊻ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁ ⊻ t ⊆ s₂ ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<VAR>b : α<GOAL>b ∈ t → Finset.image (fun x => x ⊔ b) s ⊆ s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s → Finset.image (fun x => a ⊔ x) t ⊆ s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<VAR>p : α → Prop<GOAL>(∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t u : Finset α<GOAL>s ⊻ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊔ b ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(s ⊻ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(s ⊻ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(s ⊻ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>t : Finset α<GOAL>∅ ⊻ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s : Finset α<GOAL>s ⊻ ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>s ⊻ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>t : Finset α<VAR>a : α<GOAL>{a} ⊻ t = Finset.image (fun x => a ⊔ x) t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s : Finset α<VAR>b : α<GOAL>s ⊻ {b} = Finset.image (fun x => x ⊔ b) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>a b : α<GOAL>{a} ⊻ {b} = {a ⊔ b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t₁ t₂ : Finset α<GOAL>s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∩ s₂) ⊻ t ⊆ s₁ ⊻ t ∩ s₂ ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t₁ t₂ : Finset α<GOAL>s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>u : Finset α<VAR>s t : Set α<GOAL>↑u ⊆ s ⊻ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊻ t'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>FunLike F α β<VAR>SupHomClass F α β<VAR>f : F<VAR>s t : Finset α<GOAL>Finset.image (⇑f) (s ⊻ t) = Finset.image (⇑f) s ⊻ Finset.image (⇑f) t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>FunLike F α β<VAR>SupHomClass F α β<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>s t : Finset α<GOAL>Finset.map { toFun := ⇑f, inj' := hf } (s ⊻ t) = Finset.map { toFun := ⇑f, inj' := hf } s ⊻ Finset.map { toFun := ⇑f, inj' := hf } t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s : Finset α<GOAL>s ⊆ s ⊻ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s : Finset α<GOAL>s ⊻ s ⊆ s ↔ SupClosed ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s : Finset α<GOAL>s ⊻ s = s ↔ SupClosed ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>Fintype α<GOAL>Finset.univ ⊻ Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<GOAL>Finset.filter (fun x => x ≤ a) (s ⊻ t) = Finset.filter (fun x => x ≤ a) s ⊻ Finset.filter (fun x => x ≤ a) t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(s.biUnion fun a => Finset.image (fun x => a ⊔ x) t) = s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>(t.biUnion fun b => Finset.image (fun x => x ⊔ b) s) = s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>Finset.image (Function.uncurry fun x x_1 => x ⊔ x_1) (s ×ˢ t) = s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t u : Finset α<GOAL>s ⊻ t ⊻ u = s ⊻ (t ⊻ u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t : Finset α<GOAL>s ⊻ t = t ⊻ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t u : Finset α<GOAL>s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t u : Finset α<GOAL>s ⊻ t ⊻ u = s ⊻ u ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>s t u v : Finset α<GOAL>s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<VAR>c : α<GOAL>c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>↑(s ⊼ t) = ↑s ⊼ ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(s ⊼ t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(s ⊼ t).card = s.card * t.card ↔ Set.InjOn (fun x => x.1 ⊓ x.2) (↑s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a ⊓ b ∈ s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<VAR>b : α<GOAL>b ∈ t → Finset.image (fun x => x ⊓ b) s ⊆ s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s → Finset.image (fun x => a ⊓ x) t ⊆ s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<VAR>p : α → Prop<GOAL>(∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t u : Finset α<GOAL>s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(s ⊼ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s ⊼ t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(s ⊼ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(s ⊼ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>t : Finset α<GOAL>∅ ⊼ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s : Finset α<GOAL>s ⊼ ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>t : Finset α<VAR>a : α<GOAL>{a} ⊼ t = Finset.image (fun x => a ⊓ x) t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s : Finset α<VAR>b : α<GOAL>s ⊼ {b} = Finset.image (fun x => x ⊓ b) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>a b : α<GOAL>{a} ⊼ {b} = {a ⊓ b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂) ⊼ t = s₁ ⊼ t ∪ s₂ ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t₁ t₂ : Finset α<GOAL>s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∩ s₂) ⊼ t ⊆ s₁ ⊼ t ∩ s₂ ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t₁ t₂ : Finset α<GOAL>s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>u : Finset α<VAR>s t : Set α<GOAL>↑u ⊆ s ⊼ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' ⊼ t'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>FunLike F α β<VAR>InfHomClass F α β<VAR>f : F<VAR>s t : Finset α<GOAL>Finset.image (⇑f) (s ⊼ t) = Finset.image (⇑f) s ⊼ Finset.image (⇑f) t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>FunLike F α β<VAR>InfHomClass F α β<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>s t : Finset α<GOAL>Finset.map { toFun := ⇑f, inj' := hf } (s ⊼ t) = Finset.map { toFun := ⇑f, inj' := hf } s ⊼ Finset.map { toFun := ⇑f, inj' := hf } t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s : Finset α<GOAL>s ⊆ s ⊼ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s : Finset α<GOAL>s ⊼ s ⊆ s ↔ InfClosed ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s : Finset α<GOAL>s ⊼ s = s ↔ InfClosed ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>Fintype α<GOAL>Finset.univ ⊼ Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<GOAL>Finset.filter (fun x => a ≤ x) (s ⊼ t) = Finset.filter (fun x => a ≤ x) s ⊼ Finset.filter (fun x => a ≤ x) t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(s.biUnion fun a => Finset.image (fun x => a ⊓ x) t) = s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>(t.biUnion fun b => Finset.image (fun x => x ⊓ b) s) = s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>Finset.image (Function.uncurry fun x x_1 => x ⊓ x_1) (s ×ˢ t) = s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t u : Finset α<GOAL>s ⊼ t ⊼ u = s ⊼ (t ⊼ u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t : Finset α<GOAL>s ⊼ t = t ⊼ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t u : Finset α<GOAL>s ⊼ (t ⊼ u) = t ⊼ (s ⊼ u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t u : Finset α<GOAL>s ⊼ t ⊼ u = s ⊼ u ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeInf α<VAR>s t u v : Finset α<GOAL>s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>s t u : Finset α<GOAL>s ⊻ t ⊼ u ⊆ (s ⊻ t) ⊼ (s ⊻ u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>s t u : Finset α<GOAL>t ⊼ u ⊻ s ⊆ (t ⊻ s) ⊼ (u ⊻ s)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>s t u : Finset α<GOAL>s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>s t u : Finset α<GOAL>(t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).powerset = s.powerset ⊻ t.powerset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).powerset = s.powerset ⊼ t.powerset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.powerset ⊻ s.powerset = s.powerset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.powerset ⊼ s.powerset = s.powerset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<GOAL>s ∈ 𝒜 → t ∈ ℬ → s ∪ t ∈ 𝒜 ⊻ ℬ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<GOAL>s ∈ 𝒜 → t ∈ ℬ → s ∩ t ∈ 𝒜 ⊼ ℬ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<VAR>c : α<GOAL>c ∈ s.disjSups t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<GOAL>s.disjSups t ⊆ s ⊻ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<GOAL>(s.disjSups t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s₁ s₂ t₁ t₂ : Finset α<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₁ ⊆ t₂<GOAL>s₁.disjSups t₁ ⊆ s₂.disjSups t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t₁ t₂ : Finset α<VAR>ht : t₁ ⊆ t₂<GOAL>s.disjSups t₁ ⊆ s.disjSups t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s₁ s₂ t : Finset α<VAR>hs : s₁ ⊆ s₂<GOAL>s₁.disjSups t ⊆ s₂.disjSups t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<VAR>p : α → Prop<GOAL>(∀ c ∈ s.disjSups t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t u : Finset α<GOAL>s.disjSups t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → a ⊔ b ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<GOAL>(s.disjSups t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<GOAL>(s.disjSups t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>t : Finset α<GOAL>∅.disjSups t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s : Finset α<GOAL>s.disjSups ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>a b : α<GOAL>{a}.disjSups {b} = if Disjoint a b then {a ⊔ b} else ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂).disjSups t = s₁.disjSups t ∪ s₂.disjSups t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t₁ t₂ : Finset α<GOAL>s.disjSups (t₁ ∪ t₂) = s.disjSups t₁ ∪ s.disjSups t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∩ s₂).disjSups t ⊆ s₁.disjSups t ∩ s₂.disjSups t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t₁ t₂ : Finset α<GOAL>s.disjSups (t₁ ∩ t₂) ⊆ s.disjSups t₁ ∩ s.disjSups t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t : Finset α<GOAL>s.disjSups t = t.disjSups s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t u : Finset α<GOAL>(s.disjSups t).disjSups u = s.disjSups (t.disjSups u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t u : Finset α<GOAL>s.disjSups (t.disjSups u) = t.disjSups (s.disjSups u)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t u : Finset α<GOAL>(s.disjSups t).disjSups u = (s.disjSups u).disjSups t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>(s.disjSups t).disjSups (u.disjSups v) = (s.disjSups u).disjSups (t.disjSups v)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<VAR>c : α<GOAL>c ∈ s.diffs t ↔ ∃ a ∈ s, ∃ b ∈ t, a \ b = c
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>↑(s.diffs t) = Set.image2 (fun x x_1 => x \ x_1) ↑s ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(s.diffs t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(s.diffs t).card = s.card * t.card ↔ Set.InjOn (fun x => x.1 \ x.2) (↑s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a \ b ∈ s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁.diffs t₁ ⊆ s₂.diffs t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s.diffs t₁ ⊆ s.diffs t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁.diffs t ⊆ s₂.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<VAR>b : α<GOAL>b ∈ t → Finset.image (fun x => x \ b) s ⊆ s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s → Finset.image (fun x => a \ x) t ⊆ s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<VAR>p : α → Prop<GOAL>(∀ c ∈ s.diffs t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a \ b)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t u : Finset α<GOAL>s.diffs t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a \ b ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(s.diffs t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s.diffs t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(s.diffs t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(s.diffs t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>t : Finset α<GOAL>∅.diffs t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s : Finset α<GOAL>s.diffs ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>s.diffs t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>t : Finset α<VAR>a : α<GOAL>{a}.diffs t = Finset.image (fun x => a \ x) t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s : Finset α<VAR>b : α<GOAL>s.diffs {b} = Finset.image (fun x => x \ b) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>{a}.diffs {b} = {a \ b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂).diffs t = s₁.diffs t ∪ s₂.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t₁ t₂ : Finset α<GOAL>s.diffs (t₁ ∪ t₂) = s.diffs t₁ ∪ s.diffs t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∩ s₂).diffs t ⊆ s₁.diffs t ∩ s₂.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t₁ t₂ : Finset α<GOAL>s.diffs (t₁ ∩ t₂) ⊆ s.diffs t₁ ∩ s.diffs t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>u : Finset α<VAR>s t : Set α<GOAL>↑u ⊆ Set.image2 (fun x x_1 => x \ x_1) s t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s'.diffs t'
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(s.biUnion fun a => Finset.image (fun x => a \ x) t) = s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>(t.biUnion fun b => Finset.image (fun x => x \ b) s) = s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>Finset.image (Function.uncurry fun x x_1 => x \ x_1) (s ×ˢ t) = s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GeneralizedBooleanAlgebra α<VAR>s t u : Finset α<GOAL>(s.diffs t).diffs u = (s.diffs u).diffs t
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ s.compls ↔ aᶜ ∈ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s : Finset α<GOAL>Finset.image compl s = s.compls
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<GOAL>↑s.compls = compl '' ↑s
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<GOAL>s.compls.card = s.card
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ s → aᶜ ∈ s.compls
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s₁ s₂ : Finset α<GOAL>s₁.compls ⊆ s₂.compls ↔ s₁ ⊆ s₂
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<VAR>p : α → Prop<GOAL>(∀ a ∈ s.compls, p a) ↔ ∀ a ∈ s, p aᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<VAR>p : α → Prop<GOAL>(∃ a ∈ s.compls, p a) ↔ ∃ a ∈ s, p aᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<GOAL>s.compls.compls = s
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>s.compls ⊆ t ↔ s ⊆ t.compls
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<GOAL>s.compls.Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>BooleanAlgebra α<GOAL>∅.compls = ∅