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>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>edgeDensity r s₂ t₂ - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * edgeDensity r s₂ t₂ ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>edgeDensity r s₂ t₂ - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * edgeDensity r s₂ t₂ ≤ (1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)) * edgeDensity r s₂ t₂
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>0 ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>↑s₂.card / ↑s₁.card ≤ 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>0 ≤ ↑t₂.card / ↑t₁.card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>↑t₂.card / ↑t₁.card ≤ 1
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<GOAL>IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf f) = ⊤
<VAR>α : Type u_1<GOAL>∀ (a b : ZNum), a * b = b * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>Periodic f ((2 * n) • c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>Periodic f (n • 2 • c)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b x y : α<GOAL>span {x, y} = span {y, x}
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>hf : CircleIntegrable f c R<VAR>hg : CircleIntegrable g c R<GOAL>(∮ (z : ℂ) in C(c, R), f z - g z) = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>B : ι → Submodule R A<VAR>hB✝ hB : SubmodulesRingBasis B<GOAL>RingSubgroupsBasis fun i => (B i).toAddSubgroup
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>B : ι → Submodule R A<VAR>hB✝ hB : SubmodulesRingBasis B<GOAL>∀ (x : A) (i : ι), ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => x * y) ⁻¹' ↑(B i).toAddSubgroup
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>B : ι → Submodule R A<VAR>hB✝ hB : SubmodulesRingBasis B<VAR>a : A<VAR>i : ι<GOAL>∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>B : ι → Submodule R A<VAR>hB✝ hB : SubmodulesRingBasis B<VAR>a : A<VAR>i j : ι<VAR>hj : a • B j ≤ B i<GOAL>∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>B : ι → Submodule R A<VAR>hB✝ hB : SubmodulesRingBasis B<VAR>a : A<VAR>i j : ι<VAR>hj : a • B j ≤ B i<GOAL>↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>W : α → Sort w<VAR>Z : β → Sort z<VAR>h₁ : α ≃ β<VAR>h₂ : (b : β) → W (h₁.symm b) ≃ Z b<VAR>f : (b : β) → Z b<VAR>b : β<GOAL>(h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>X₁ : Type u_1<VAR>X₂ : Type u_2<VAR>X₃ : Type u_3<VAR>inst✝¹¹ : AddCommMonoid X₁<VAR>inst✝¹⁰ : AddCommMonoid X₂<VAR>inst✝⁹ : AddCommMonoid X₃<VAR>inst✝⁸ : Module R X₁<VAR>inst✝⁷ : Module R X₂<VAR>inst✝⁶ : Module R X₃<VAR>Y₁ : Type u_4<VAR>Y₂ : Type u_5<VAR>Y₃ : Type u_6<VAR>inst✝⁵ : AddCommMonoid Y₁<VAR>inst✝⁴ : AddCommMonoid Y₂<VAR>inst✝³ : AddCommMonoid Y₃<VAR>inst✝² : Module R Y₁<VAR>inst✝¹ : Module R Y₂<VAR>inst✝ : Module R Y₃<VAR>f₁ : X₁ →ₗ[R] Y₁<VAR>f₂ : X₂ →ₗ[R] Y₂<VAR>f₃ : X₃ →ₗ[R] Y₃<GOAL>↑(assoc R Y₁ Y₂ Y₃) ∘ₗ map (map f₁ f₂) f₃ = map f₁ (map f₂ f₃) ∘ₗ ↑(assoc R X₁ X₂ X₃)
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>X₁ : Type u_1<VAR>X₂ : Type u_2<VAR>X₃ : Type u_3<VAR>inst✝¹¹ : AddCommMonoid X₁<VAR>inst✝¹⁰ : AddCommMonoid X₂<VAR>inst✝⁹ : AddCommMonoid X₃<VAR>inst✝⁸ : Module R X₁<VAR>inst✝⁷ : Module R X₂<VAR>inst✝⁶ : Module R X₃<VAR>Y₁ : Type u_4<VAR>Y₂ : Type u_5<VAR>Y₃ : Type u_6<VAR>inst✝⁵ : AddCommMonoid Y₁<VAR>inst✝⁴ : AddCommMonoid Y₂<VAR>inst✝³ : AddCommMonoid Y₃<VAR>inst✝² : Module R Y₁<VAR>inst✝¹ : Module R Y₂<VAR>inst✝ : Module R Y₃<VAR>f₁ : X₁ →ₗ[R] Y₁<VAR>f₂ : X₂ →ₗ[R] Y₂<VAR>f₃ : X₃ →ₗ[R] Y₃<GOAL>∀ (x : X₁) (y : X₂) (z : X₃), (↑(assoc R Y₁ Y₂ Y₃) ∘ₗ map (map f₁ f₂) f₃) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = (map f₁ (map f₂ f₃) ∘ₗ ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
<VAR>a✝ b✝ c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b d : ℕ<VAR>hdb : d ∣ b<VAR>h : a < b<GOAL>a / d < b / d
<VAR>a✝ b✝ c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b d : ℕ<VAR>hdb : d ∣ b<VAR>h : a < b<GOAL>d * (a / d) < b
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>b ≤ c / a ↔ a * b ≤ c
<VAR>u v m✝ n : ℤ<VAR>x✝ : Even n<VAR>m : ℤ<VAR>hm : n = m + m<GOAL>n % 2 = 0
<VAR>u v m n : ℤ<VAR>h : n % 2 = 0<GOAL>n % 2 + 2 * (n / 2) = n / 2 + n / 2
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in Ioc a b, f x ∂μ + ∫ (x : ℝ) in Ioc b c, f x ∂μ + ∫ (x : ℝ) in Ioc c a, f x ∂μ = ∫ (x : ℝ) in Ioc b a, f x ∂μ + ∫ (x : ℝ) in Ioc c b, f x ∂μ + ∫ (x : ℝ) in Ioc a c, f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ = ∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>Disjoint (Ioc b a ∪ Ioc c b) (Ioc a c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>MeasurableSet (Ioc a c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc b a ∪ Ioc c b) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc a c) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>Disjoint (Ioc b a) (Ioc c b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>MeasurableSet (Ioc c b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc b a) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc c b) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>MeasurableSet (Ioc c a)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc a b ∪ Ioc b c) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc c a) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>Disjoint (Ioc a b) (Ioc b c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>MeasurableSet (Ioc b c)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc a b) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<VAR>hac : IntervalIntegrable f μ a c<GOAL>IntegrableOn f (Ioc b c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<GOAL>∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x univ = 1<GOAL>∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1<GOAL>∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1<VAR>x : γ<VAR>hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1<GOAL>κ.density κ.fst a x univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<GOAL>(blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<VAR>a b : ↥L<GOAL>Codisjoint a b ↔ Codisjoint ↑a ↑b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>v : V<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>h : v ∈ e<VAR>e' : Sym2 V<GOAL>e' ∈ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) ↔ e' ∈ {e}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>v : V<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<VAR>h : v ∈ e<VAR>e' : Sym2 V<GOAL>(e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<GOAL>(comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ range m
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(pullback f g).OpenCover
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (i : 𝒰.J), pullback.map (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i)) f g (pullback.fst f (𝒰.map i)) (pullback.fst g (𝒰.map i)) (𝒰.map i) ⋯ ⋯ = (Iso.refl ((fun i => pullback (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i))) i)).hom ≫ (openCoverOfBase' 𝒰 f g).map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>pullback.map (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i)) f g (pullback.fst f (𝒰.map i)) (pullback.fst g (𝒰.map i)) (𝒰.map i) ⋯ ⋯ = (Iso.refl ((fun i => pullback (pullback.snd f (𝒰.map i)) (pullback.snd g (𝒰.map i))) i)).hom ≫ (openCoverOfBase' 𝒰 f g).map (((Equiv.prodPUnit 𝒰.J).symm.trans (Equiv.sigmaEquivProd 𝒰.J PUnit.{u + 1}).symm) i)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>hl : HasStrictFDerivAt l l' (f x)<VAR>hf : HasStrictDerivAt f f' x<VAR>hy : y = f x<GOAL>HasStrictDerivAt (l ∘ f) (l' f') x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<GOAL>IsOpen {p | Disjoint (𝓝 p.1) (𝓝 p.2)}
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<GOAL>∀ (a b : X), Disjoint (𝓝 a) (𝓝 b) → {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (a, b)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x y : X<VAR>h : Disjoint (𝓝 x) (𝓝 y)<GOAL>{p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x y : X<VAR>h : Disjoint (𝓝 x) (𝓝 y)<VAR>U : Set X<VAR>hU : x ∈ U ∧ IsOpen U<VAR>V : Set X<VAR>hV : y ∈ V ∧ IsOpen V<VAR>hd : Disjoint U V<GOAL>{p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>h : ∀ (x y : α), f x ≤ f y + ↑K * dist x y<GOAL>LipschitzWith K f
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>inst✝² : Nonempty ι<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>inst✝¹ : HasWidePullback B X f<VAR>inst✝ : PreservesLimit (wideCospan B X f) (forget C)<VAR>x y : (forget C).obj (widePullback B X f)<VAR>h : ∀ (j : ι), (π f j) x = (π f j) y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>inst✝² : Nonempty ι<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>inst✝¹ : HasWidePullback B X f<VAR>inst✝ : PreservesLimit (wideCospan B X f) (forget C)<VAR>x y : (forget C).obj (widePullback B X f)<VAR>h : ∀ (j : ι), (π f j) x = (π f j) y<GOAL>(base f) x = (base f) y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>B : C<VAR>ι : Type w<VAR>inst✝² : Nonempty ι<VAR>X : ι → C<VAR>f : (j : ι) → X j ⟶ B<VAR>inst✝¹ : HasWidePullback B X f<VAR>inst✝ : PreservesLimit (wideCospan B X f) (forget C)<VAR>x y : (forget C).obj (widePullback B X f)<VAR>h : ∀ (j : ι), (π f j) x = (π f j) y<VAR>inhabited_h : Inhabited ι<GOAL>(base f) x = (base f) y
<VAR>K : Type u<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidWithZeroHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p q : K[X]<GOAL>(map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
<VAR>K : Type u<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidWithZeroHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p : K[X]<GOAL>(map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) 0) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ 0)
<VAR>K : Type u<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidWithZeroHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<VAR>a : Ordinal.{u_4}<GOAL>a < o ↔ ∃ x < o, a < x
<VAR>a b : Ordinal.{u_1}<GOAL>succ a ⨳ b = a ⨳ b ♯ b