ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<VAR>h : s ⊆ t<GOAL>s -ᵥ s ⊆ t -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s₁ s₂ t : Set β<GOAL>s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t₁ t₂ : Set β<GOAL>s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s₁ s₂ t : Set β<GOAL>s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t₁ t₂ : Set β<GOAL>s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s₁ s₂ t₁ t₂ : Set β<GOAL>s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂) ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s₁ s₂ t₁ t₂ : Set β<GOAL>s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>⋃ a ∈ s, (fun x => a -ᵥ x) '' t = s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>⋃ a ∈ t, (fun x => x -ᵥ a) '' s = s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VSub α β<VAR>s : ι → Set β<VAR>t : Set β<GOAL>(⋃ i, s i) -ᵥ t = ⋃ i, s i -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VSub α β<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s -ᵥ ⋃ i, t i = ⋃ i, s -ᵥ t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VSub α β<VAR>s : (i : ι) → κ i → Set β<VAR>t : Set β<GOAL>(⋃ i, ⋃ j, s i j) -ᵥ t = ⋃ i, ⋃ j, s i j -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VSub α β<VAR>s : Set β<VAR>t : (i : ι) → κ i → Set β<GOAL>s -ᵥ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s -ᵥ t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VSub α β<VAR>s : ι → Set β<VAR>t : Set β<GOAL>(⋂ i, s i) -ᵥ t ⊆ ⋂ i, s i -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VSub α β<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s -ᵥ ⋂ i, t i ⊆ ⋂ i, s -ᵥ t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VSub α β<VAR>s : (i : ι) → κ i → Set β<VAR>t : Set β<GOAL>(⋂ i, ⋂ j, s i j) -ᵥ t ⊆ ⋂ i, ⋂ j, s i j -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VSub α β<VAR>s : Set β<VAR>t : (i : ι) → κ i → Set β<GOAL>s -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>VAdd α β<VAR>VAdd α γ<VAR>f : β → γ<VAR>a : α<VAR>s : Set β<GOAL>(∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → f '' (a +ᵥ s) = a +ᵥ f '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>a : α<VAR>s : Set β<GOAL>(∀ (b : β), f (a • b) = a • f b) → f '' (a • s) = a • f '' s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>a : α<VAR>s : Set α<GOAL>⇑f '' (a +ᵥ s) = f a +ᵥ ⇑f '' s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MulOneClass α<VAR>MulOneClass β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>a : α<VAR>s : Set α<GOAL>⇑f '' (a • s) = f a • ⇑f '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>VAdd αᵃᵒᵖ β<VAR>VAdd β γ<VAR>VAdd α γ<VAR>a : α<VAR>s : Set β<VAR>t : Set γ<VAR>h : ∀ (a : α) (b : β) (c : γ), AddOpposite.op a +ᵥ b +ᵥ c = b +ᵥ (a +ᵥ c)<GOAL>AddOpposite.op a +ᵥ s +ᵥ t = s +ᵥ (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SMul αᵐᵒᵖ β<VAR>SMul β γ<VAR>SMul α γ<VAR>a : α<VAR>s : Set β<VAR>t : Set γ<VAR>h : ∀ (a : α) (b : β) (c : γ), (MulOpposite.op a • b) • c = b • a • c<GOAL>(MulOpposite.op a • s) • t = s • a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>s : Set α<GOAL>s • 0 ⊆ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s • 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>t : Set β<VAR>a : α<VAR>h : 0 ∈ t<GOAL>0 ∈ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>t : Set β<VAR>a : α<VAR>Zero α<VAR>NoZeroSMulDivisors α β<VAR>ha : a ≠ 0<GOAL>0 ∈ a • t ↔ 0 ∈ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>t : Set β<GOAL>0 • t ⊆ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>t : Set β<VAR>ht : t.Nonempty<GOAL>0 • t = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>s : Set β<VAR>h : s.Nonempty<GOAL>0 • s = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>s : Set β<GOAL>0 • s ⊆ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>s : Set β<GOAL>(0 • s).Subsingleton
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>s : Set α<VAR>t : Set β<VAR>NoZeroSMulDivisors α β<GOAL>0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
<VAR>α : Type u_2<VAR>AddSemigroup α<VAR>a : α<VAR>s t : Set α<GOAL>AddOpposite.op a +ᵥ s + t = s + (a +ᵥ t)
<VAR>α : Type u_2<VAR>Semigroup α<VAR>a : α<VAR>s t : Set α<GOAL>MulOpposite.op a • s * t = s * a • t
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>s t : Set α<GOAL>(s.PairwiseDisjoint fun x => x +ᵥ t) ↔ Set.InjOn (fun p => p.1 + p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>s t : Set α<GOAL>(s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 * p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s : Set β<VAR>a : α<VAR>x : β<GOAL>a • x ∈ a • s ↔ x ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Set β<VAR>a : α<VAR>x : β<GOAL>a +ᵥ x ∈ a +ᵥ s ↔ x ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>A : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>A : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ a • A ↔ a⁻¹ • x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>A : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ -a +ᵥ A ↔ a +ᵥ x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>A : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ a⁻¹ • A ↔ a • x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>t : Set β<GOAL>(fun x => a • x) ⁻¹' t = a⁻¹ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>t : Set β<GOAL>(fun x => a +ᵥ x) ⁻¹' t = -a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>t : Set β<GOAL>(fun x => a⁻¹ • x) ⁻¹' t = a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>t : Set β<GOAL>(fun x => -a +ᵥ x) ⁻¹' t = a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>A B : Set β<VAR>a : α<GOAL>a • A ⊆ a • B ↔ A ⊆ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>A B : Set β<VAR>a : α<GOAL>a +ᵥ A ⊆ a +ᵥ B ↔ A ⊆ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>A B : Set β<VAR>a : α<GOAL>a • A ⊆ B ↔ A ⊆ a⁻¹ • B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>A B : Set β<VAR>a : α<GOAL>a +ᵥ A ⊆ B ↔ A ⊆ -a +ᵥ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>A B : Set β<VAR>a : α<GOAL>A ⊆ a +ᵥ B ↔ -a +ᵥ A ⊆ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>A B : Set β<VAR>a : α<GOAL>A ⊆ a • B ↔ a⁻¹ • A ⊆ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Set β<VAR>a : α<GOAL>a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<GOAL>a • (s ∩ t) = a • s ∩ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>ι : Type u_5<VAR>a : α<VAR>t : ι → Set β<GOAL>a • ⋂ i, t i = ⋂ i, a • t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>ι : Type u_5<VAR>a : α<VAR>t : ι → Set β<GOAL>a +ᵥ ⋂ i, t i = ⋂ i, a +ᵥ t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Set β<VAR>a : α<GOAL>a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<GOAL>a • (s \ t) = a • s \ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<GOAL>a • symmDiff s t = symmDiff (a • s) (a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Set β<VAR>a : α<GOAL>a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>a : α<GOAL>a • Set.univ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<GOAL>a +ᵥ Set.univ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s • Set.univ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s +ᵥ Set.univ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Set β<VAR>a : α<GOAL>a +ᵥ sᶜ = (a +ᵥ s)ᶜ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s : Set β<VAR>a : α<GOAL>a • sᶜ = (a • s)ᶜ
<VAR>α : Type u_2<VAR>Group α<VAR>s t : Set α<VAR>x : α<GOAL>x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s t : Set α<VAR>x : α<GOAL>(x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a + -b = x
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s t : Set α<VAR>x : α<GOAL>(x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a - b = x
<VAR>α : Type u_2<VAR>Group α<VAR>s t : Set α<VAR>x : α<GOAL>x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
<VAR>α : Type u_2<VAR>AddGroup α<VAR>s t : Set α<VAR>x : αᵃᵒᵖ<GOAL>(x +ᵥ s) ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ -a + b = AddOpposite.unop x
<VAR>α : Type u_2<VAR>Group α<VAR>s t : Set α<VAR>x : αᵐᵒᵖ<GOAL>x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Set β<GOAL>⋃ g, -g +ᵥ s = ⋃ g, g +ᵥ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s : Set β<GOAL>⋃ g, g⁻¹ • s = ⋃ g, g • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s : Set β<GOAL>⋃ g, g • s = {a | ∃ g, g • a ∈ s}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Set β<GOAL>⋃ g, g +ᵥ s = {a | ∃ g, g +ᵥ a ∈ s}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<VAR>s : Set α<GOAL>-(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<VAR>s : Set α<GOAL>(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<VAR>s : Set α<GOAL>-(AddOpposite.op a +ᵥ s) = -a +ᵥ -s
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<VAR>s : Set α<GOAL>(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<GOAL>Disjoint (a • s) (a • t) ↔ Disjoint s t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Set β<VAR>a : α<GOAL>Disjoint (a +ᵥ s) (a +ᵥ t) ↔ Disjoint s t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>A : Set β<VAR>x : β<GOAL>a • x ∈ a • A ↔ x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>A : Set β<VAR>x : β<GOAL>x ∈ a • A ↔ a⁻¹ • x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>A : Set β<VAR>x : β<GOAL>x ∈ a⁻¹ • A ↔ a • x ∈ A
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>t : Set β<GOAL>(fun x => a • x) ⁻¹' t = a⁻¹ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>t : Set β<GOAL>(fun x => a⁻¹ • x) ⁻¹' t = a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>A B : Set β<GOAL>a • A ⊆ a • B ↔ A ⊆ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>A B : Set β<GOAL>a • A ⊆ B ↔ A ⊆ a⁻¹ • B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<VAR>A B : Set β<GOAL>A ⊆ a • B ↔ a⁻¹ • A ⊆ B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • (s ∩ t) = a • s ∩ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • (s \ t) = a • s \ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Set β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • symmDiff s t = symmDiff (a • s) (a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • Set.univ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s : Set α<VAR>hs : ¬s ⊆ 0<GOAL>s • Set.univ = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s • Set.univ = Set.univ
<VAR>α : Type u_2<VAR>GroupWithZero α<GOAL>0⁻¹ = 0
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>a : α<VAR>s : Set α<GOAL>(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>a : α<VAR>s : Set α<GOAL>(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid α<VAR>AddGroup β<VAR>DistribMulAction α β<VAR>a : α<VAR>t : Set β<GOAL>a • -t = -(a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid α<VAR>AddGroup β<VAR>DistribMulAction α β<VAR>s : Set α<VAR>t : Set β<GOAL>s • -t = -(s • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring α<VAR>AddCommMonoid β<VAR>Module α β<VAR>a b : α<VAR>s : Set β<GOAL>(a + b) • s ⊆ a • s + b • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>a : α<VAR>t : Set β<GOAL>-a • t = -(a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>s : Set α<VAR>t : Set β<GOAL>-s • t = -(s • t)
<VAR>α : Type u<VAR>x : Tree α<GOAL>x.height ≤ x.numNodes
<VAR>x : Tree Unit<VAR>_hx : x ≠ Tree.nil<GOAL>Tree.node () x.left x.right = x
<VAR>α : Type u_2<VAR>A B : Set α<VAR>h : A ⊆ B<GOAL>Subtype.val ⁻¹' B = Set.univ
<VAR>α : Type u_2<VAR>A : Set α<VAR>S : Set (Set α)<GOAL>Subtype.val ⁻¹' ⋃₀ S = ⋃₀ {x | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A : Set α<VAR>s : ι → Set α<GOAL>Subtype.val ⁻¹' ⋂ i, s i = ⋂ i, Subtype.val ⁻¹' s i
<VAR>α : Type u_2<VAR>A : Set α<VAR>S : Set (Set α)<GOAL>Subtype.val ⁻¹' ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
<VAR>α : Type u_2<VAR>A : Set α<VAR>S : Set (Set α)<GOAL>Subtype.val ⁻¹' ⋂₀ S = ⋂₀ ((fun x => Subtype.val ⁻¹' x) '' S)
<VAR>α : Type u_2<VAR>A B C : Set α<VAR>hB : B ⊆ A<VAR>hC : C ⊆ A<VAR>h : Subtype.val ⁻¹' B = Subtype.val ⁻¹' C<GOAL>B = C
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<GOAL>Subtype.val '' (D ∪ E) = Subtype.val '' D ∪ Subtype.val '' E
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<GOAL>Subtype.val '' (D ∩ E) = Subtype.val '' D ∩ Subtype.val '' E
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<GOAL>Subtype.val '' (D \ E) = Subtype.val '' D \ Subtype.val '' E
<VAR>α : Type u_2<VAR>A : Set α<VAR>D : Set ↑A<GOAL>Subtype.val '' Dᶜ = A \ Subtype.val '' D
<VAR>α : Type u_2<VAR>A : Set α<VAR>T : Set (Set ↑A)<GOAL>Subtype.val '' ⋃₀ T = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A : Set α<VAR>t : ι → Set ↑A<GOAL>Subtype.val '' ⋃ i, t i = ⋃ i, Subtype.val '' t i
<VAR>α : Type u_2<VAR>A : Set α<VAR>T : Set (Set ↑A)<VAR>hT : T.Nonempty<GOAL>Subtype.val '' ⋂₀ T = ⋂₀ {x | ∃ B ∈ T, Subtype.val '' B = x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A : Set α<VAR>t : ι → Set ↑A<VAR>Nonempty ι<GOAL>Subtype.val '' ⋂ i, t i = ⋂ i, Subtype.val '' t i
<VAR>α : Type u_2<VAR>A : Set α<VAR>D : Set ↑A<GOAL>A ∪ Subtype.val '' D = A
<VAR>α : Type u_2<VAR>A : Set α<VAR>D : Set ↑A<GOAL>Subtype.val '' D ∪ A = A
<VAR>α : Type u_2<VAR>A : Set α<VAR>D : Set ↑A<GOAL>A ∩ Subtype.val '' D = Subtype.val '' D
<VAR>α : Type u_2<VAR>A : Set α<VAR>D : Set ↑A<GOAL>Subtype.val '' D ∩ A = Subtype.val '' D
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<GOAL>D ⊆ Subtype.val ⁻¹' (Subtype.val '' E) ↔ D ⊆ E
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<GOAL>Subtype.val '' D = Subtype.val '' E ↔ D = E
<VAR>α : Type u_2<VAR>A : Set α<GOAL>Function.Injective (Set.image Subtype.val)
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<VAR>h : Subtype.val '' D ⊆ Subtype.val '' E<GOAL>D ⊆ E
<VAR>α : Type u_2<VAR>A : Set α<VAR>D E : Set ↑A<VAR>h : D ⊆ E<GOAL>Subtype.val '' D ⊆ Subtype.val '' E
<VAR>α : Type u_2<VAR>A B : Set α<GOAL>Subtype.val '' (Subtype.val ⁻¹' B) ⊆ B
<VAR>α : Type u_2<VAR>A : Set α<VAR>D : Set ↑A<GOAL>Subtype.val ⁻¹' (Subtype.val '' D) = D
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>LE α<VAR>x : α<GOAL>Set.Accumulate s x = ⋃ y, ⋃ (_ : y ≤ x), s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>LE α<VAR>x : α<VAR>z : β<GOAL>z ∈ Set.Accumulate s x ↔ ∃ y ≤ x, z ∈ s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>Preorder α<VAR>x : α<GOAL>s x ⊆ Set.Accumulate s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>Preorder α<VAR>x : α<GOAL>Set.Accumulate s x ⊆ ⋃ i, s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>Preorder α<GOAL>Monotone (Set.Accumulate s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>Preorder α<VAR>x y : α<VAR>h : x ≤ y<GOAL>Set.Accumulate s x ⊆ Set.Accumulate s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>Preorder α<VAR>x : α<GOAL>⋃ y, ⋃ (_ : y ≤ x), Set.Accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : α → Set β<VAR>Preorder α<GOAL>⋃ x, Set.Accumulate s x = ⋃ x, s x
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ Set.iUnion S<VAR>i : ι<VAR>x : ↑(S i)<VAR>hx : ↑x ∈ T<GOAL>Set.iUnionLift S f hf T hT ⟨↑x, hx⟩ = f i x
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ Set.iUnion S<VAR>i : ι<VAR>x : ↑(S i)<VAR>h : S i ⊆ T<GOAL>Set.iUnionLift S f hf T hT (Set.inclusion h x) = f i x
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ Set.iUnion S<VAR>x : ↑T<VAR>i : ι<VAR>hx : ↑x ∈ S i<GOAL>Set.iUnionLift S f hf T hT x = f i ⟨↑x, hx⟩
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Type u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ Set.iUnion S<VAR>t : Set β<GOAL>Set.iUnionLift S f hf T hT ⁻¹' t = Set.inclusion hT ⁻¹' ⋃ i, Set.inclusion ⋯ '' (f i ⁻¹' t)
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ Set.iUnion S<VAR>c : ↑T<VAR>ci : (i : ι) → ↑(S i)<VAR>hci : ∀ (i : ι), ↑(ci i) = ↑c<VAR>cβ : β<VAR>h : ∀ (i : ι), f i (ci i) = cβ<GOAL>Set.iUnionLift S f hf T hT c = cβ
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT' : T = Set.iUnion S<VAR>u : ↑T → ↑T<VAR>ui : (i : ι) → ↑(S i) → ↑(S i)<VAR>hui : ∀ (i : ι) (x : ↑(S i)), u (Set.inclusion ⋯ x) = Set.inclusion ⋯ (ui i x)<VAR>uβ : β → β<VAR>h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)<VAR>x : ↑T<GOAL>Set.iUnionLift S f hf T ⋯ (u x) = uβ (Set.iUnionLift S f hf T ⋯ x)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT' : T = Set.iUnion S<VAR>dir : Directed (fun x x_1 => x ≤ x_1) S<VAR>op : ↑T → ↑T → ↑T<VAR>opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)<VAR>hopi : ∀ (i : ι) (x y : ↑(S i)), Set.inclusion ⋯ (opi i x y) = op (Set.inclusion ⋯ x) (Set.inclusion ⋯ y)<VAR>opβ : β → β → β<VAR>h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)<VAR>x y : ↑T<GOAL>Set.iUnionLift S f hf T ⋯ (op x y) = opβ (Set.iUnionLift S f hf T ⋯ x) (Set.iUnionLift S f hf T ⋯ y)
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>hS : Set.iUnion S = Set.univ<VAR>i : ι<VAR>x : ↑(S i)<GOAL>Set.liftCover S f hf hS ↑x = f i x
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>hS : Set.iUnion S = Set.univ<VAR>i : ι<VAR>x : α<VAR>hx : x ∈ S i<GOAL>Set.liftCover S f hf hS x = f i ⟨x, hx⟩
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Type u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>hS : Set.iUnion S = Set.univ<VAR>t : Set β<GOAL>Set.liftCover S f hf hS ⁻¹' t = ⋃ i, Subtype.val '' (f i ⁻¹' t)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : Symmetric r<VAR>a b : α<GOAL>Pairwise (r on fun c => bif c then a else b) ↔ r a b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun c => bif c then a else b) ↔ Disjoint a b
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : α → α → Prop<VAR>LinearOrder ι<VAR>hr : Symmetric r<VAR>f : ι → α<GOAL>Pairwise (r on f) ↔ ∀ ⦃m n : ι⦄, m < n → r (f m) (f n)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>LinearOrder ι<VAR>f : ι → α<GOAL>Pairwise (Disjoint on f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f g : ι → α<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>hs : Pairwise (Disjoint on f)<VAR>h : g ≤ f<GOAL>Pairwise (Disjoint on g)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>hs : s.Pairwise r<GOAL>t.Pairwise r
<VAR>α : Type u_1<VAR>r p : α → α → Prop<VAR>s : Set α<VAR>H : r ≤ p<VAR>hr : s.Pairwise r<GOAL>s.Pairwise p
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.Pairwise ⊤
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : s.Subsingleton<VAR>r : α → α → Prop<GOAL>s.Pairwise r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>∅.Pairwise r
<VAR>α : Type u_1<VAR>a : α<VAR>r : α → α → Prop<GOAL>{a}.Pairwise r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<GOAL>s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : α → α → Prop<VAR>f : ι → α<VAR>IsEquiv α r<VAR>s : Set ι<VAR>hs : s.Nonempty<GOAL>s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>f : α → ι<GOAL>(s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>s : Set α<VAR>f : α → ι<VAR>r : ι → ι → Prop<VAR>IsEquiv ι r<GOAL>s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>s : Set α<VAR>f : α → ι<GOAL>(s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>(s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>hr : Symmetric r<GOAL>(s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>ha : a ∉ s<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : s.Pairwise r<VAR>h : ∀ b ∈ s, a ≠ b → r a b ∧ r b a<GOAL>(insert a s).Pairwise r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>ha : a ∉ s<VAR>hs : s.Pairwise r<VAR>h : ∀ b ∈ s, r a b ∧ r b a<GOAL>(insert a s).Pairwise r