ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.sections = bif L.any isEmpty then [] else (foldr sectionsTR.go #[[]] L).data
<VAR>α : Type u_1<VAR>L : List (List α)<VAR>e : L.any isEmpty = false<GOAL>L.sections = (foldr sectionsTR.go #[[]] L).data
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>IH : L.sections = (foldr sectionsTR.go #[[]] L).data<GOAL>((foldr sectionsTR.go #[[]] L).data.bind fun s => map (fun a => a :: s) l) = (Array.foldl (fun acc' l' => foldl (fun acc' a => acc'.push (a :: l')) acc' l) #[] (foldr sectionsTR.go #[[]] L) 0).data
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>IH : L.sections = (foldr sectionsTR.go #[[]] L).data<GOAL>((foldr sectionsTR.go #[[]] L).data.bind fun s => map (fun a => a :: s) l) = #[].data ++ (foldr sectionsTR.go #[[]] L).data.bind ?h.h.false.cons.G
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>IH : L.sections = (foldr sectionsTR.go #[[]] L).data<GOAL>List α → List (List α)
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>IH : L.sections = (foldr sectionsTR.go #[[]] L).data<GOAL>∀ (acc : Array (List α)) (a : List α), (foldl (fun acc' a_1 => acc'.push (a_1 :: a)) acc l).data = acc.data ++ ?h.h.false.cons.G a
<VAR>α : Type u_1<VAR>l : List α<VAR>L : List (List α)<VAR>IH : L.sections = (foldr sectionsTR.go #[[]] L).data<VAR>acc✝ : Array (List α)<VAR>a✝ : List α<GOAL>(foldl (fun acc' a => acc'.push (a :: a✝)) acc✝ l).data = acc✝.data ++ map (fun a => a :: a✝) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>sym : Symmetric r<VAR>h : Irreflexive r<GOAL>∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>sym : Symmetric r<VAR>h : Irreflexive r<GOAL>∀ (x y : α), s(x, y) ∈ fromRel sym → ¬s(x, y).IsDiag
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : Set (Subsemigroup M)<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s
<VAR>V : Type (u + 1)<VAR>inst✝³ : LargeCategory V<VAR>G✝ : MonCat<VAR>W : Type (u + 1)<VAR>inst✝² : LargeCategory W<VAR>inst✝¹ : MonoidalCategory V<VAR>inst✝ : MonoidalCategory W<VAR>F : MonoidalFunctor V W<VAR>G : MonCat<GOAL>(inv (F.mapAction G).ε).hom = inv F.ε
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ : Finset α<VAR>u✝ v a b : α<VAR>inst✝ : DecidableEq α<VAR>u : α<VAR>s : Finset α<GOAL>filter (fun x => compress u u x ∈ s) s ∪ filter (fun x => x ∉ s) (image (compress u u) s) = s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ : Finset α<VAR>u✝ v a b : α<VAR>inst✝ : DecidableEq α<VAR>u : α<VAR>s : Finset α<GOAL>filter (fun x => compress u u x ∈ s) s = s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s✝ : Finset α<VAR>u✝ v a b : α<VAR>inst✝ : DecidableEq α<VAR>u : α<VAR>s : Finset α<GOAL>filter (fun x => x ∉ s) (image (compress u u) s) = ∅
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₁' p₂ p₃ : P<VAR>h : Wbtw ℝ p₂ p₁ p₁'<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₃p₂ : ¬p₃ = p₂<VAR>hp₁'p₂ : ¬p₁' = p₂<GOAL>∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : MeasurableSpace M<VAR>inst✝⁵ : MeasurableSpace N<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : SMul M α<VAR>inst✝¹ : SMulInvariantMeasure M α μ<VAR>inst✝ : MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f g : ↥(Lp E p μ)<GOAL>edist (c • f) (c • g) = edist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>Ico a b ∩ Ici c = Ico (a ⊔ c) b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>m : M<VAR>a✝ : ι<GOAL>((basisAux A b) (a ⊗ₜ[R] m)) a✝ = (a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)) a✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : LinearOrderedCommRing S<VAR>n : Type u_3<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>A : ι → Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x<VAR>i j : n<GOAL>abv ((∑ k ∈ s, A k) i j) = abv (∑ k ∈ s, A k i j)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.111951, u_1} C<VAR>inst✝⁶ : Category.{?u.111955, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<GOAL>inr φ₁ ≫ map φ₁ φ₂ a b comm = b ≫ inr φ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.111951, u_1} C<VAR>inst✝⁶ : Category.{?u.111955, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<GOAL>(triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a = map φ₁ φ₂ a b comm ≫ (triangle φ₂).mor₃
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>hf : Measurable f<GOAL>Measurable (∫⋯∫⁻_s, f ∂μ)
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>hf : Measurable f<GOAL>Measurable (uncurry fun x y => f (updateFinset x s y))
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>hf : Measurable f<GOAL>Measurable fun a => updateFinset a.1 s a.2
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>hf : Measurable f<GOAL>∀ (a : δ), Measurable fun x => updateFinset x.1 s x.2 a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>t : Set α<VAR>a b : α<VAR>s : Finset α<GOAL>(infClosure ↑s).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x ∈ Ico a b ∪ Ici c ↔ x ∈ Ici (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>a ≤ x ∧ x < b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : ι → Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((sum μ).withDensity f) s = (sum fun n => (μ n).withDensity f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ici a \ Ici b = Ico a b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i : ℕ<GOAL>⇑(cast R M ⋯) = _root_.cast ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i : ℕ<GOAL>⇑(LinearEquiv.refl R (⨂[R]^i M)) = _root_.cast ⋯
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.WOppSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : ↑s = ∅<GOAL>IsPreconnected {y | s.WOppSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : (↑s).Nonempty<GOAL>IsPreconnected {y | s.WOppSide x y}
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<VAR>hc0 : ¬c = 0<GOAL>a * (b / c) * c ≤ a * b
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<VAR>hc0 : ¬c = 0<GOAL>a * (b / c * c) ≤ a * b
<VAR>n i : Nat<VAR>h : i < (list n).length<GOAL>(enum n).data[i] = cast ⋯ ⟨i, h⟩
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : FirstObj P S.arrows<GOAL>((firstObjEqFamily P S.arrows).hom x).Compatible ↔ firstMap P S x = secondMap P S x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : FirstObj P S.arrows<GOAL>((firstObjEqFamily P S.arrows).hom x).SieveCompatible ↔ firstMap P S x = secondMap P S x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : Function.End α<VAR>h : LocallyLipschitz f<GOAL>LocallyLipschitz (f ^ 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : Function.End α<VAR>h : LocallyLipschitz f<VAR>n : ℕ<GOAL>LocallyLipschitz (f ^ (n + 1))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : Function.End α<VAR>h : LocallyLipschitz f<VAR>n : ℕ<GOAL>LocallyLipschitz (f ^ n * f)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>v : n → R<VAR>i : n<GOAL>v ⬝ᵥ (LinearMap.stdBasis R (fun x => R) i) 1 = v i
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<GOAL>limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y<GOAL>limsup u f ≤ x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : AddCommMonoid ι<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝⁴ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>inst✝³ : SMul α R<VAR>inst✝² : SMul α A<VAR>inst✝¹ : IsScalarTower α R A<VAR>inst✝ : IsScalarTower α A A<VAR>n : ℕ<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(n • y).val = n • y.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E p μ)<GOAL>↑(toSimpleFunc f) =ᶠ[ae μ] ↑↑↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E p μ)<GOAL>↑↑f = AEEqFun.mk ↑(toSimpleFunc f) ⋯
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>l : List (Sigma β)<VAR>l' : List (Sigma β)<VAR>hl : [] = l'<GOAL>(foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>l : List (Sigma β)<VAR>l' : List (Sigma β)<VAR>hl : [] = l'<VAR>this : l'.NodupKeys<GOAL>(foldr (fun x => kinsert x.fst x.snd) l' l).NodupKeys
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<GOAL>(A.ρ g) (↑f (g⁻¹, g)) - ↑f (g, g⁻¹) = ↑f (1, 1) - ↑f (g, 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<VAR>this : ↑f (g * g⁻¹, g) + ↑f (g, g⁻¹) = (A.ρ g) (↑f (g⁻¹, g)) + ↑f (g, g⁻¹ * g)<GOAL>(A.ρ g) (↑f (g⁻¹, g)) - ↑f (g, g⁻¹) = ↑f (1, 1) - ↑f (g, 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<VAR>this : ↑f (1, 1) + ↑f (g, g⁻¹) = (A.ρ g) (↑f (g⁻¹, g)) + ↑f (g, 1)<GOAL>(A.ρ g) (↑f (g⁻¹, g)) - ↑f (g, g⁻¹) = ↑f (1, 1) - ↑f (g, 1)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₂ p₃ p₁).sign = 1<GOAL>∡ p₂ p₃ p₁ = ↑(Real.arctan (dist p₁ p₂ / dist p₃ p₂))
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>r : R<VAR>f : R[X]<VAR>s : R<GOAL>eval s ((taylor r) f) = eval (s + r) f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>F : D ⥤ PresheafOfModules R<VAR>inst✝¹ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>hF : ∀ (j : D), Presheaf.IsSheaf J (F.obj j).presheaf<VAR>inst✝ : HasLimitsOfShape D AddCommGrp<VAR>G : D ⥤ Sheaf J AddCommGrp := { obj := fun j => { val := (F.obj j).presheaf, cond := ⋯ }, map := fun {X Y} φ => { val := (toPresheaf R).map (F.map φ) }, map_id := ⋯, map_comp := ⋯ }<GOAL>Presheaf.IsSheaf J c.pt.presheaf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<GOAL>(M.map f hf).Basis (f '' I) (f '' X) ↔ M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>I' : Set α<VAR>hI' : M.Indep I'<VAR>hII' : f '' I = f '' I'<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>I' : Set α<VAR>hI' : M.Indep I'<VAR>hII' : I = I'<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>hI' : M.Indep I<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>hI' : M.Indep I<VAR>hss : I ⊆ X<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>hI' : M.Indep I<VAR>hss : I ⊆ X<VAR>J : Set α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>J ⊆ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>hI' : M.Indep I<VAR>hss : I ⊆ X<VAR>J : Set α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<VAR>hIJ' : f '' I = f '' J<GOAL>J ⊆ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<VAR>h : (M.map f hf).Basis (f '' I) (f '' X)<VAR>hI' : M.Indep I<VAR>hss : I ⊆ X<VAR>J : Set α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<VAR>hIJ' : I = J<GOAL>J ⊆ I
<VAR>a x✝ z x : ℂ<GOAL>↑(abs x) * (cos ↑x.arg + sin ↑x.arg * I) = x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<VAR>h : (constantCoeff σ R) φ = ↑u<GOAL>φ.invOfUnit u * φ = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<VAR>h : (constantCoeff σ R) φ = ↑u<GOAL>φ.invOfUnit u ∈ nonZeroDivisors (MvPowerSeries σ R)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<VAR>h : (constantCoeff σ R) φ = ↑u<GOAL>(constantCoeff σ R) (φ.invOfUnit u) ∈ nonZeroDivisors R
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<GOAL>IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L<VAR>x : E<GOAL>IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L<VAR>x : E<VAR>hx : IsIntegral F x<GOAL>IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L<VAR>x : E<VAR>hx : IsIntegral F x<VAR>x✝ : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h✝ : ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L<VAR>x : E<VAR>hx : IsIntegral F x<VAR>x✝ : IsSeparable F x<VAR>y : F<VAR>h : (algebraMap F ↥F⟮x⟯) y = AdjoinSimple.gen F x<GOAL>x ∈ (algebraMap F E).range
<VAR>R S T : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hf : f.IsIntegral<VAR>hg : g.IsIntegral<GOAL>(g.comp f).IsIntegral
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<VAR>S : Set β<GOAL>UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S ↔ ∀ (k : κ), UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → β → α'<VAR>S : Set β<GOAL>Tendsto (fun x => ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α')) ↔ ∀ (k : κ), Tendsto (fun x => ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α'))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Unique ι<VAR>k : K<VAR>x✝ : ?m.169717<GOAL>(?m.169723.repr (fract (Basis.singleton ι K) k)) x✝ = (?m.169723.repr (Int.fract k)) x✝
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>G : Type u<VAR>inst✝ : Group G<VAR>V : FDRep k G<VAR>g h : G<GOAL>V.character (h * g * h⁻¹) = V.character g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>i✝ : ℕ<VAR>x✝ : Fin i✝ → M<GOAL>(((toDirectSum.comp ofDirectSum).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i => ⨂[R]^i M) i✝).compMultilinearMap (PiTensorProduct.tprod R)) x✝ = (((AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i => ⨂[R]^i M) i✝).compMultilinearMap (PiTensorProduct.tprod R)) x✝