ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Set α<VAR>t✝ t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → α → β<VAR>s t : Set α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t
<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>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Set α<VAR>t✝ t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → α → β<VAR>s t : Set α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
<VAR>α : Type u_1<VAR>r₁ r₂ : Setoid α<VAR>h : r₁.classes = r₂.classes<VAR>a b : α<GOAL>r₁.Rel a b ↔ r₂.Rel a b
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>x : k<VAR>h2 : NeZero 2<GOAL>∃ z, x = z * z
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>h2 : NeZero 2<VAR>z : k<GOAL>∃ z_1, z ^ 2 = z_1 * z_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), (⨆ n, ↑(eapprox f n) a) + ⨆ n, ↑(eapprox g n) a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(fun a => (⨆ n, ↑(eapprox f n) a) + ⨆ n, ↑(eapprox g n) a) = fun a => ⨆ n, (↑(eapprox f n) + ↑(eapprox g n)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>a : α<GOAL>(⨆ n, ↑(eapprox f n) a) + ⨆ n, ↑(eapprox g n) a = ⨆ n, (↑(eapprox f n) + ↑(eapprox g n)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>a : α<GOAL>⨆ a_1, ↑(eapprox f a_1) a + ↑(eapprox g a_1) a = ⨆ n, (↑(eapprox f n) + ↑(eapprox g n)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>a : α<GOAL>Monotone fun n => ↑(eapprox f n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>a : α<GOAL>Monotone fun n => ↑(eapprox g n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (a : α), ⨆ n, (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ = ⨆ n, (eapprox f n).lintegral μ + (eapprox g n).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>⨆ n, ∫⁻ (a : α), (↑(eapprox f n) + ↑(eapprox g n)) a ∂μ = ⨆ n, (eapprox f n).lintegral μ + (eapprox g n).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∀ (n : ℕ), Measurable (↑(eapprox f n) + ↑(eapprox g n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Monotone fun n => ↑(eapprox f n) + ↑(eapprox g n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>(⨆ n, (eapprox f n).lintegral μ) + ⨆ n, (eapprox g n).lintegral μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x✝ y z : α<VAR>t : Set α<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<GOAL>diam (s ∪ t) ≤ diam s + diam t
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y : ℝ≥0∞<VAR>h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y<GOAL>x ≤ y
<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x y : ℝ≥0∞<VAR>h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y<VAR>r : ℝ≥0∞<VAR>hr : r < x<GOAL>r ≤ y
<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>x y : ℝ≥0∞<VAR>h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y<VAR>r : ℝ≥0<VAR>hr : ↑r < x<GOAL>↑r ≤ y
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>w : InfinitePlace K<VAR>a : 𝓞 K<VAR>ha : a ≠ 0<VAR>h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1<GOAL>1 ≤ ↑|(Algebra.norm ℚ) ↑a|
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>w : InfinitePlace K<VAR>a : 𝓞 K<VAR>ha : a ≠ 0<VAR>h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1<GOAL>1 ≤ |(Algebra.norm ℤ) a|
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = g ≫ h<VAR>inst✝³ : HasCoequalizer f g<VAR>inst✝² : HasCoequalizer (G.map f) (G.map g)<VAR>inst✝¹ : PreservesColimit (parallelPair f g) G<VAR>X' Y' : D<VAR>f' g' : X' ⟶ Y'<VAR>inst✝ : HasCoequalizer f' g'<VAR>p : G.obj X ⟶ X'<VAR>q : G.obj Y ⟶ Y'<VAR>wf : G.map f ≫ q = p ≫ f'<VAR>wg : G.map g ≫ q = p ≫ g'<GOAL>G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) = q ≫ coequalizer.π f' g'
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>(ΓIso f U).inv = Scheme.Hom.appLE f (Scheme.Hom.opensRange f ⊓ U) (f ⁻¹ᵁ U) ⋯
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>Convex R s ↔ ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>(∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s) → Convex R s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>ι : Type u_3<VAR>s : Multiset ι<VAR>t : ι → Multiset α<VAR>b : ι → α<VAR>b₀ : α<GOAL>fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun i => fold op (b i) (t i)) s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>ι : Type u_3<VAR>t : ι → Multiset α<VAR>b : ι → α<VAR>b₀ : α<GOAL>fold op (fold op b₀ (map b 0)) (bind 0 t) = fold op b₀ (map (fun i => fold op (b i) (t i)) 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha✝ : Std.Associative op<VAR>ι : Type u_3<VAR>t : ι → Multiset α<VAR>b : ι → α<VAR>b₀ : α<VAR>a : ι<VAR>ha : Multiset ι<VAR>ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i => fold op (b i) (t i)) ha)<GOAL>fold op (fold op b₀ (map b (a ::ₘ ha))) ((a ::ₘ ha).bind t) = fold op b₀ (map (fun i => fold op (b i) (t i)) (a ::ₘ ha))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) (o.rightAngleRotation y) = ⟪x, y⟫_ℝ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype n<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : n ≃ o<VAR>e₂ : l → o<VAR>M : Matrix m n α<GOAL>M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype n<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : n ≃ o<VAR>e₂ : l → o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<GOAL>M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype n<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : n ≃ o<VAR>e₂ : l → o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<VAR>A : Matrix m o α := M.submatrix id ⇑e₁.symm<GOAL>M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype n<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : n ≃ o<VAR>e₂ : l → o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<VAR>A : Matrix m o α := M.submatrix id ⇑e₁.symm<VAR>this : M = A.submatrix id ⇑e₁<GOAL>M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype n<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : n ≃ o<VAR>e₂ : l → o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<VAR>A : Matrix m o α := M.submatrix id ⇑e₁.symm<VAR>this : M = A.submatrix id ⇑e₁<GOAL>(A * 1).submatrix id e₂ = (A.submatrix id ⇑e₁).submatrix id (⇑e₁.symm ∘ e₂)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : R[X]<VAR>r : R<GOAL>derivative (eval₂ C q (C r)) = eval₂ C q (derivative (C r)) * derivative q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>p q p₁ p₂ : R[X]<VAR>ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q<VAR>ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q<GOAL>derivative (eval₂ C q (p₁ + p₂)) = eval₂ C q (derivative (p₁ + p₂)) * derivative q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>r : R<VAR>ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q<GOAL>derivative (eval₂ C q (C r * X ^ (n + 1))) = eval₂ C q (derivative (C r * X ^ (n + 1))) * derivative q
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f g : CauSeq β abv<GOAL>(const abv (f.lim * g.lim) - f * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f g : CauSeq β abv<VAR>h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)<GOAL>(const abv (f.lim * g.lim) - f * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f g : CauSeq β abv<VAR>h : const abv (f.lim * g.lim) - f * g = (const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)<GOAL>((const abv f.lim - f) * g + const abv f.lim * (const abv g.lim - g)).LimZero
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<GOAL>∃ u, u.card * t.card ≤ (s * t).card ∧ s ⊆ u * t / t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ∈ C<VAR>hCmax : ∀ x ∈ C, ¬u < x<GOAL>∃ u, u.card * t.card ≤ (s * t).card ∧ s ⊆ u * t / t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<GOAL>∃ u, u.card * t.card ≤ (s * t).card ∧ s ⊆ u * t / t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<VAR>a : α<VAR>ha : a ∈ s<GOAL>a ∈ u * t / t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<VAR>a : α<VAR>ha : a ∈ s<GOAL>a ∈ u * (t / t)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<VAR>a : α<VAR>ha : a ∈ s<VAR>hau : a ∉ u<VAR>H : ∃ b ∈ u, ¬Disjoint (a • t) (b • t)<GOAL>a ∈ u * (t / t)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<VAR>a : α<VAR>ha : a ∈ s<VAR>hau : a ∉ u<VAR>H : ∃ b ∈ u, ∃ a_1, a⁻¹ • a_1 ∈ t ∧ b⁻¹ • a_1 ∈ t<GOAL>a ∈ u * (t / t)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<VAR>a : α<VAR>ha : a ∈ s<VAR>hau : a ∉ u<VAR>b : α<VAR>hb : b ∈ u<VAR>c : α<VAR>hc₁ : a⁻¹ • c ∈ t<VAR>hc₂ : b⁻¹ • c ∈ t<GOAL>a ∈ u * (t / t)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>s t : Finset α<VAR>ht : t.Nonempty<VAR>this : (u : Set α) → Decidable (u.PairwiseDisjoint fun x => x • t)<VAR>C : Finset (Finset α) := filter (fun u => (↑u).PairwiseDisjoint fun x => x • t) s.powerset<VAR>u : Finset α<VAR>hu : u ⊆ s ∧ (↑u).PairwiseDisjoint fun x => x • t<VAR>hCmax : ∀ x ∈ C, ¬u < x<VAR>a : α<VAR>ha : a ∈ s<VAR>hau : a ∉ u<VAR>b : α<VAR>hb : b ∈ u<VAR>c : α<VAR>hc₁ : a⁻¹ • c ∈ t<VAR>hc₂ : b⁻¹ • c ∈ t<GOAL>a / b ∈ t / t
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : { w // w ≠ w₀ }<VAR>r : NNReal<VAR>h : ‖(logEmbedding K) x‖ ≤ ↑r<GOAL>|(logEmbedding K) x w| ≤ ↑r
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : { w // w ≠ w₀ }<VAR>r : NNReal<VAR>h : ∀ b ∈ univ, ↑‖(logEmbedding K) x b‖₊ ≤ ↑r<GOAL>|(logEmbedding K) x w| ≤ ↑r
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>x : R<GOAL>(comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x)) ⋯).comp (algebraMap R ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen x)))) = (IsLocalization.map (↑((structureSheaf S).val.obj (op (PrimeSpectrum.basicOpen (f x))))) f ⋯).comp (algebraMap R ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen x))))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a✝ : α<VAR>b : β<VAR>q✝ : ℚ<VAR>a : α<VAR>q : ℚ<GOAL>↑q < inducedMap β γ (inducedMap α β a) ↔ ↑q < inducedMap α γ a
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ F_int 1 a =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<GOAL>∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)<GOAL>∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)<GOAL>∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)<GOAL>F_int 1 ↑a =O[atTop] fun t => rexp (-min p q * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)<VAR>this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t<GOAL>F_int 1 ↑a =O[atTop] fun t => rexp (-min p q * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)<VAR>this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t<GOAL>min p q ≤ p
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : F_nat 1 a =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : F_nat 1 (1 - a) =O[atTop] fun t => rexp (-q * t)<VAR>this : F_int 1 ↑a =ᶠ[atTop] fun t => F_nat 1 a t + F_nat 1 (1 - a) t<GOAL>min p q ≤ q
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a✝ b : α<VAR>inst✝ : IsSymm α r<VAR>a : α<VAR>l : List α<VAR>ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)<VAR>hl : (a :: l).Nodup<GOAL>{a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a✝ b : α<VAR>inst✝ : IsSymm α r<VAR>a : α<VAR>l : List α<VAR>ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)<VAR>hl : a ∉ l ∧ l.Nodup<GOAL>{a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a✝ b : α<VAR>inst✝ : IsSymm α r<VAR>a : α<VAR>l : List α<VAR>ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)<VAR>hl : a ∉ l ∧ l.Nodup<VAR>this : ∀ b ∈ l, ¬a = b → r a b ↔ r a b<GOAL>{a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E✝ : Type u_3<VAR>inst✝⁹ : AddCommGroup E✝<VAR>inst✝⁸ : Module ℝ E✝<VAR>inst✝⁷ : TopologicalSpace E✝<VAR>inst✝⁶ : TopologicalAddGroup E✝<VAR>inst✝⁵ : ContinuousSMul ℝ E✝<VAR>E : Type u_4<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>x y : E<VAR>s : Set E<VAR>h : [x-[ℝ]y] ⊆ s<VAR>A : Continuous fun t => (1 - t) • x + t • y<GOAL>JoinedIn s x y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E✝ : Type u_3<VAR>inst✝⁹ : AddCommGroup E✝<VAR>inst✝⁸ : Module ℝ E✝<VAR>inst✝⁷ : TopologicalSpace E✝<VAR>inst✝⁶ : TopologicalAddGroup E✝<VAR>inst✝⁵ : ContinuousSMul ℝ E✝<VAR>E : Type u_4<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>x y : E<VAR>s : Set E<VAR>h : [x-[ℝ]y] ⊆ s<VAR>A : Continuous fun t => (1 - t) • x + t • y<GOAL>(fun t => (1 - t) • x + t • y) '' unitInterval ⊆ s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E✝ : Type u_3<VAR>inst✝⁹ : AddCommGroup E✝<VAR>inst✝⁸ : Module ℝ E✝<VAR>inst✝⁷ : TopologicalSpace E✝<VAR>inst✝⁶ : TopologicalAddGroup E✝<VAR>inst✝⁵ : ContinuousSMul ℝ E✝<VAR>E : Type u_4<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>x y : E<VAR>s : Set E<VAR>h : [x-[ℝ]y] ⊆ s<VAR>A : Continuous fun t => (1 - t) • x + t • y<GOAL>(fun t => (1 - t) • x + t • y) '' unitInterval = [x-[ℝ]y]
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>eval n (ascPochhammer ℕ 0) = n.ascFactorial 0
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n t : ℕ<GOAL>eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)<GOAL>doset a ↑H ↑K = doset b ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)<GOAL>doset a ↑H ↑K = doset b ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)<VAR>ha : a ∈ doset b ↑H ↑K<GOAL>doset a ↑H ↑K = doset b ↑H ↑K
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>p : M → Prop<VAR>hs : closure s = ⊤<VAR>x : M<VAR>H1 : p 1<VAR>Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)<VAR>this : x ∈ closure s<GOAL>p x
<VAR>α : Type u_1<VAR>inst✝¹ : StrictOrderedSemiring α<VAR>β : Type u_2<VAR>inst✝ : OrderedRing β<VAR>x : ↑(Ioo 0 1)<GOAL>0 < 1 - ↑x