ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hr : Symmetric r<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hr : Symmetric r<VAR>ha : a ∉ s<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : s.Pairwise r<VAR>hr : Symmetric r<VAR>h : ∀ b ∈ s, a ≠ b → r a b<GOAL>(insert a s).Pairwise r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : s.Pairwise r<VAR>hr : Symmetric r<VAR>ha : a ∉ s<VAR>h : ∀ b ∈ s, r a b<GOAL>(insert a s).Pairwise r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>{a, b}.Pairwise r ↔ a ≠ b → r a b ∧ r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>hr : Symmetric r<GOAL>{a, b}.Pairwise r ↔ a ≠ b → r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Set.univ.Pairwise r ↔ Pairwise r
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.Pairwise ⊥ ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → α<VAR>s : Set ι<GOAL>Set.InjOn f s ↔ s.Pairwise fun x x_1 => f x ≠ f x_1
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : α → α → Prop<VAR>f : ι → α<VAR>s : Set ι<VAR>h : s.Pairwise (r on f)<GOAL>(f '' s).Pairwise r
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : α → α → Prop<VAR>f : ι → α<VAR>s : Set ι<VAR>h : Set.InjOn f s<GOAL>(f '' s).Pairwise r ↔ s.Pairwise (r on f)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>r : α → α → Prop<VAR>f : ι → α<VAR>hr : Pairwise (r on f)<GOAL>(Set.range f).Pairwise r
<VAR>α : Type u_1<VAR>s : Set α<VAR>r : α → α → Prop<GOAL>(Pairwise fun x y => r ↑x ↑y) ↔ s.Pairwise r
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s t : Set ι<VAR>f : ι → α<VAR>ht : t.PairwiseDisjoint f<VAR>h : s ⊆ t<GOAL>s.PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f g : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i<GOAL>s.PairwiseDisjoint g
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f g : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>h : g ≤ f<GOAL>s.PairwiseDisjoint g
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>f : ι → α<GOAL>∅.PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>i : ι<VAR>f : ι → α<GOAL>{i}.PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>i : ι<GOAL>(insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>i : ι<VAR>hi : i ∉ s<GOAL>(insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>i : ι<VAR>h : ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)<GOAL>(insert i s).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∉ s<VAR>h : ∀ j ∈ s, Disjoint (f i) (f j)<GOAL>(insert i s).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>g : ι → ι<VAR>hg : f ∘ g ≤ f<GOAL>(g '' s).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>PartialOrder α<VAR>OrderBot α<VAR>f : ι → α<VAR>g : ι' → ι<VAR>s : Set ι'<VAR>h : Set.InjOn g s<GOAL>(g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ↑s → ι<VAR>hg : ∀ (i : ↑s), f (g i) ≤ f ↑i<VAR>ht : s.PairwiseDisjoint f<GOAL>(Set.range g).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s t : Set ι<VAR>f : ι → α<GOAL>(s ∪ t).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ t.PairwiseDisjoint f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s t : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>ht : t.PairwiseDisjoint f<VAR>h : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)<GOAL>(s ∪ t).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>h : ¬Disjoint (f i) (f j)<GOAL>i = j
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>i = j ∨ Disjoint (f i) (f j)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>f : α → Set β<GOAL>(Set.range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x = f y ∨ Disjoint (f x) (f y)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>f : ι → α<VAR>h : Pairwise (Disjoint on f)<VAR>s : Set ι<GOAL>s.PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>h : f i ⊓ f j ≠ ⊥<GOAL>i = j
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>s : Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hf : f i ≠ ⊥<VAR>hij : f i ≤ f j<GOAL>i = j
<VAR>ι : Type u_4<GOAL>(Set.range singleton).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → α<VAR>s : Set α<GOAL>s.PairwiseDisjoint fun a => f ⁻¹' {a}
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : Set ι<VAR>f : ι → Set α<VAR>hs : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>a : α<VAR>hai : a ∈ f i<VAR>haj : a ∈ f j<GOAL>i = j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι → Set α<VAR>g : ι' → Set β<VAR>hs : s.PairwiseDisjoint f<VAR>ht : t.PairwiseDisjoint g<GOAL>(s ×ˢ t).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2
<VAR>ι : Type u_4<VAR>ι' : ι → Type u_6<VAR>α : ι → Type u_7<VAR>s : (i : ι) → Set (ι' i)<VAR>f : (i : ι) → ι' i → Set (α i)<VAR>hs : ∀ (i : ι), (s i).PairwiseDisjoint (f i)<GOAL>(Set.univ.pi s).PairwiseDisjoint fun I => Set.univ.pi fun i => f i (I i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>hf : ∀ a ∈ s, Function.Injective (f a)<GOAL>(s.PairwiseDisjoint fun a => f a '' t) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>hf : ∀ b ∈ t, Function.Injective fun a => f a b<GOAL>(t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t)
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : Set ι<VAR>f : ι → Set α<VAR>h : ¬s.PairwiseDisjoint f<GOAL>∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : Set ι<VAR>LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬s.PairwiseDisjoint f<GOAL>∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → Set α<VAR>h : ¬Pairwise (Disjoint on f)<GOAL>∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬Pairwise (Disjoint on f)<GOAL>∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → α<GOAL>Pairwise (Disjoint on fun a => f ⁻¹' {a})
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → Set α<GOAL>(∀ (a : α), {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f)
<VAR>α : Type u_1<VAR>f : ℕ → Set α<GOAL>memPartition f 0 = {Set.univ}
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<GOAL>memPartition f (n + 1) = {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>u v : Set α<VAR>hu : u ∈ memPartition f n<VAR>hv : v ∈ memPartition f n<VAR>huv : u ≠ v<GOAL>Disjoint u v
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<GOAL>⋃₀ memPartition f n = Set.univ
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>a : α<GOAL>memPartitionSet f 0 a = Set.univ
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>Decidable (a ∈ f n)<GOAL>memPartitionSet f (n + 1) a = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ memPartition f n<VAR>ha : a ∈ s<GOAL>memPartitionSet f n a = s
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>SMul G P<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>x : G × P<GOAL>x ∈ s.smulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>VAdd G P<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>x : G × P<GOAL>x ∈ s.vaddAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>SMul G P<VAR>s₁ s₂ : Set G<VAR>t : Set P<VAR>a : P<VAR>h : s₁ ⊆ s₂<GOAL>s₁.smulAntidiagonal t a ⊆ s₂.smulAntidiagonal t a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>VAdd G P<VAR>s₁ s₂ : Set G<VAR>t : Set P<VAR>a : P<VAR>h : s₁ ⊆ s₂<GOAL>s₁.vaddAntidiagonal t a ⊆ s₂.vaddAntidiagonal t a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>VAdd G P<VAR>s : Set G<VAR>t₁ t₂ : Set P<VAR>a : P<VAR>h : t₁ ⊆ t₂<GOAL>s.vaddAntidiagonal t₁ a ⊆ s.vaddAntidiagonal t₂ a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>SMul G P<VAR>s : Set G<VAR>t₁ t₂ : Set P<VAR>a : P<VAR>h : t₁ ⊆ t₂<GOAL>s.smulAntidiagonal t₁ a ⊆ s.smulAntidiagonal t₂ a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>VAdd G P<VAR>IsCancelVAdd G P<VAR>x y : ↑(s.vaddAntidiagonal t a)<GOAL>(↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>SMul G P<VAR>IsCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a)<GOAL>(↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>SMul G P<VAR>IsCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a)<VAR>h : (↑x).1 = (↑y).1<GOAL>x = y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>VAdd G P<VAR>IsCancelVAdd G P<VAR>x y : ↑(s.vaddAntidiagonal t a)<VAR>h : (↑x).1 = (↑y).1<GOAL>x = y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>VAdd G P<VAR>IsCancelVAdd G P<VAR>x y : ↑(s.vaddAntidiagonal t a)<VAR>h : (↑x).2 = (↑y).2<GOAL>x = y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>SMul G P<VAR>IsCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a)<VAR>h : (↑x).2 = (↑y).2<GOAL>x = y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>x y : ↑(s.vaddAntidiagonal t a)<VAR>h₁ : (↑x).1 ≤ (↑y).1<VAR>h₂ : (↑x).2 ≤ (↑y).2<GOAL>x = y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a)<VAR>h₁ : (↑x).1 ≤ (↑y).1<VAR>h₂ : (↑x).2 ≤ (↑y).2<GOAL>x = y
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>PartialOrder G<VAR>PartialOrder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<GOAL>(s.vaddAntidiagonal t a).Finite
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>PartialOrder G<VAR>PartialOrder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<GOAL>(s.smulAntidiagonal t a).Finite
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>(Mathlib.Vector.cons a v).head = a
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>(Mathlib.Vector.cons a v).tail = v
<VAR>α : Type u<VAR>n : ℕ<VAR>v : Mathlib.Vector α n.succ<GOAL>Mathlib.Vector.cons v.head v.tail = v
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Mathlib.Vector.map f Mathlib.Vector.nil = Mathlib.Vector.nil
<VAR>α : Type u<VAR>β : Type v<VAR>n : ℕ<VAR>f : α → β<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>Mathlib.Vector.map f (Mathlib.Vector.cons a v) = Mathlib.Vector.cons (f a) (Mathlib.Vector.map f v)
<VAR>α : Type u<VAR>n : ℕ<VAR>a1 a2 : Mathlib.Vector α n<GOAL>a1.toList = a2.toList → a1 = a2
<VAR>α : Type u<VAR>v : Mathlib.Vector α 0<GOAL>v = Mathlib.Vector.nil
<VAR>α : Type u<VAR>n : ℕ<VAR>v : List α<VAR>P : v.length = n<GOAL>Mathlib.Vector.toList ⟨v, P⟩ = v
<VAR>α : Type u<GOAL>Mathlib.Vector.nil.toList = []
<VAR>α : Type u<VAR>n : ℕ<VAR>v : Mathlib.Vector α n<GOAL>v.toList.length = n
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>(Mathlib.Vector.cons a v).toList = a :: v.toList
<VAR>α : Type u<VAR>n m : ℕ<VAR>v : Mathlib.Vector α n<VAR>w : Mathlib.Vector α m<GOAL>(v.append w).toList = v.toList ++ w.toList
<VAR>α : Type u<VAR>n m : ℕ<VAR>v : Mathlib.Vector α m<GOAL>(Mathlib.Vector.drop n v).toList = List.drop n v.toList
<VAR>α : Type u<VAR>n m : ℕ<VAR>v : Mathlib.Vector α m<GOAL>(Mathlib.Vector.take n v).toList = List.take n v.toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>i : Fin n<VAR>v : Mathlib.Vector α n<GOAL>v.get i ∈ v.toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>a ∈ v.toList ↔ ∃ i, v.get i = a
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∉ Mathlib.Vector.nil.toList
<VAR>α : Type u_1<VAR>a : α<VAR>v : Mathlib.Vector α 0<GOAL>a ∉ v.toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a a' : α<VAR>v : Mathlib.Vector α n<GOAL>a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α (n + 1)<GOAL>a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<GOAL>a ∈ (a ::ᵥ v).toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Mathlib.Vector α (n + 1)<GOAL>v.head ∈ v.toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a a' : α<VAR>v : Mathlib.Vector α n<VAR>ha' : a' ∈ v.toList<GOAL>a' ∈ (a ::ᵥ v).toList
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>v : Mathlib.Vector α n<VAR>ha : a ∈ v.tail.toList<GOAL>a ∈ v.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>b : β<VAR>v : Mathlib.Vector α n<VAR>f : α → β<GOAL>b ∈ (Mathlib.Vector.map f v).toList ↔ ∃ a ∈ v.toList, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>v : Mathlib.Vector α 0<VAR>f : α → β<GOAL>b ∉ (Mathlib.Vector.map f v).toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>b : β<VAR>v : Mathlib.Vector α (n + 1)<VAR>f : α → β<GOAL>b ∈ (Mathlib.Vector.map f v).toList ↔ f v.head = b ∨ ∃ a ∈ v.tail.toList, f a = b
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>x y : α<GOAL>(x ::ᵥ xs).snoc y = x ::ᵥ xs.snoc y
<GOAL>∀ {α : Type u_1} {x : α}, Mathlib.Vector.nil.snoc x = x ::ᵥ Mathlib.Vector.nil
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>x : α<GOAL>(x ::ᵥ xs).reverse = xs.reverse.snoc x
<VAR>α : Type u_1<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<VAR>x : α<GOAL>(xs.snoc x).reverse = x ::ᵥ xs.reverse
<VAR>α : Type u_1<VAR>n : ℕ<VAR>val : α<GOAL>Mathlib.Vector.replicate (n + 1) val = (Mathlib.Vector.replicate n val).snoc val
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<GOAL>∀ {α_1 : Type u_1} {f : α → α_1} {x : α}, Mathlib.Vector.map f (xs.snoc x) = (Mathlib.Vector.map f xs).snoc (f x)
<GOAL>∀ {α : Type u_1} {α_1 : Type} {β : Type u_2} {f : α → α_1 → α_1 × β} {s : α_1}, Mathlib.Vector.mapAccumr f Mathlib.Vector.nil s = (s, Mathlib.Vector.nil)
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Mathlib.Vector α n<GOAL>∀ {α_1 : Type} {β : Type u_1} {f : α → α_1 → α_1 × β} {x : α} {s : α_1}, Mathlib.Vector.mapAccumr f (xs.snoc x) s = let q := f x s; let r := Mathlib.Vector.mapAccumr f xs q.1; (r.1, r.2.snoc q.2)
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_3<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<GOAL>∀ {α_1 : Type u_1} {f : α → β → α_1} {x : α} {y : β}, Mathlib.Vector.map₂ f (xs.snoc x) (ys.snoc y) = (Mathlib.Vector.map₂ f xs ys).snoc (f x y)
<GOAL>∀ {α β α_1 β_1 : Type} {f : α → β → α_1 → α_1 × β_1} {s : α_1}, Mathlib.Vector.mapAccumr₂ f Mathlib.Vector.nil Mathlib.Vector.nil s = (s, Mathlib.Vector.nil)
<VAR>α : Type<VAR>n : ℕ<VAR>β : Type<VAR>xs : Mathlib.Vector α n<VAR>ys : Mathlib.Vector β n<VAR>σ φ : Type<VAR>c : σ<VAR>f : α → β → σ → σ × φ<VAR>x : α<VAR>y : β<GOAL>Mathlib.Vector.mapAccumr₂ f (xs.snoc x) (ys.snoc y) c = let q := f x y c; let r := Mathlib.Vector.mapAccumr₂ f xs ys q.1; (r.1, r.2.snoc q.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>f : α → β → γ<VAR>x : Mathlib.Vector α n<VAR>y : Mathlib.Vector β n<GOAL>(Mathlib.Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>f : α → β → γ<VAR>x : Mathlib.Vector α n<VAR>y : Mathlib.Vector β n<VAR>i : Fin n<GOAL>(Mathlib.Vector.zipWith f x y).get i = f (x.get i) (y.get i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>f : α → β → γ<VAR>x : Mathlib.Vector α n<VAR>y : Mathlib.Vector β n<GOAL>(Mathlib.Vector.zipWith f x y).tail = Mathlib.Vector.zipWith f x.tail y.tail
<VAR>α : Type u_1<VAR>n : ℕ<VAR>AddCommMonoid α<VAR>x y : Mathlib.Vector α n<GOAL>x.toList.sum + y.toList.sum = (Mathlib.Vector.zipWith (fun x x_1 => x + x_1) x y).toList.sum
<VAR>α : Type u_1<VAR>n : ℕ<VAR>CommMonoid α<VAR>x y : Mathlib.Vector α n<GOAL>x.toList.prod * y.toList.prod = (Mathlib.Vector.zipWith (fun x x_1 => x * x_1) x y).toList.prod
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>i : ι<GOAL>Set.range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>i j : ι<VAR>h : i ≠ j<VAR>s : Set (α j)<GOAL>Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<GOAL>Sigma.mk i '' (g i ⁻¹' s) ⊆ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι' → Type u_5<VAR>f : ι → ι'<VAR>hf : Function.Injective f<VAR>g : (i : ι) → α i → β (f i)<VAR>i : ι<VAR>s : Set (β (f i))<GOAL>Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>x : (i : ι) × α i<GOAL>x ∈ s.sigma t ↔ x.fst ∈ s ∧ x.snd ∈ t x.fst
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>a : α i<GOAL>⟨i, a⟩ ∈ s.sigma t ↔ i ∈ s ∧ a ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>a : α i<VAR>hi : i ∈ s<VAR>ha : a ∈ t i<GOAL>⟨i, a⟩ ∈ s.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s₁ s₂ : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<VAR>hs : s₁ ⊆ s₂<VAR>ht : ∀ (i : ι), t₁ i ⊆ t₂ i<GOAL>s₁.sigma t₁ ⊆ s₂.sigma t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<GOAL>s.sigma t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → ⟨i, a⟩ ∈ u
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>p : (i : ι) × α i → Prop<GOAL>(∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p ⟨i, a⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>p : (i : ι) × α i → Prop<GOAL>(∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<GOAL>(s.sigma fun i => ∅) = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>t : (i : ι) → Set (α i)<GOAL>∅.sigma t = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>i : ι<GOAL>(Set.univ.sigma fun x => Set.univ) = Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<GOAL>(s.sigma fun x => Set.univ) = Sigma.fst ⁻¹' s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ((i : ι) × α i)<GOAL>(Set.univ.sigma fun i => Sigma.mk i ⁻¹' s) = s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>a : α i<GOAL>{i}.sigma t = Sigma.mk i '' t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>a : (i : ι) → α i<GOAL>(s.sigma fun i => {a i}) = (fun i => ⟨i, a i⟩) '' s
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>i : ι<VAR>a : (i : ι) → α i<GOAL>({i}.sigma fun i => {a i}) = {⟨i, a i⟩}
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s₁ s₂ : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>(s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>(s.sigma fun i => t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s₁ s₂ : Set ι<VAR>t₁ t₂ : (i : ι) → Set (α i)<GOAL>s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i => t₁ i ∩ t₂ i
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_5<VAR>CompleteLattice β<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : Sigma α → β<GOAL>⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_5<VAR>CompleteLattice β<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i → β<GOAL>⨆ i ∈ s, ⨆ j ∈ t i, f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_5<VAR>CompleteLattice β<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : Sigma α → β<GOAL>⨅ ij ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_5<VAR>CompleteLattice β<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i → β<GOAL>⨅ i ∈ s, ⨅ j ∈ t i, f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_6<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : Sigma α → Set β<GOAL>⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_6<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i → Set β<GOAL>⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_6<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : Sigma α → Set β<GOAL>⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : Type u_6<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i → Set β<GOAL>⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.fst ij.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>a : α i<GOAL>(insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>a : (i : ι) → α i<GOAL>(s.sigma fun i => insert (a i) (t i)) = (fun i => ⟨i, a i⟩) '' s ∪ s.sigma t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>β : ι → Type u_7<VAR>f : ι' → ι<VAR>g : (i : ι) → β i → α i<GOAL>((f ⁻¹' s).sigma fun i => g (f i) ⁻¹' t (f i)) = (fun p => ⟨f p.fst, g (f p.fst) p.snd⟩) ⁻¹' s.sigma t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : ι' → ι<GOAL>((f ⁻¹' s).sigma fun i => t (f i)) = (fun p => ⟨f p.fst, p.snd⟩) ⁻¹' s.sigma t
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>β : ι → Type u_7<VAR>g : (i : ι) → β i → α i<GOAL>(s.sigma fun i => g i ⁻¹' t i) = (fun p => ⟨p.fst, g p.fst p.snd⟩) ⁻¹' s.sigma t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>α' : ι' → Type u_8<VAR>f : ι → ι'<VAR>g : (i : ι) → α i → α' (f i)<VAR>s : Set ι'<VAR>t : (i : ι') → Set (α' i)<GOAL>Sigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma fun i => g i ⁻¹' t (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Sigma.mk i ⁻¹' s.sigma t = t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>hi : i ∉ s<GOAL>Sigma.mk i ⁻¹' s.sigma t = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>DecidablePred fun x => x ∈ s<GOAL>Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>i : ι<VAR>β : Type u_8<VAR>DecidablePred fun x => x ∈ s<VAR>g : β → α i<GOAL>(fun b => ⟨i, g b⟩) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>β : ι → Type u_7<VAR>f : (i : ι) → α i → β i<GOAL>(Set.univ.sigma fun i => Set.range (f i)) = Set.range fun x => ⟨x.fst, f x.fst x.snd⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_3<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<GOAL>s.Nonempty → (∀ (i : ι), (t i).Nonempty) → (s.sigma t).Nonempty