ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : AEMeasurable X μ<VAR>hs : MeasurableSet s<GOAL>Integrable (fun a => (((condDistrib Y X μ) (X a)) s).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : AEMeasurable X μ<VAR>hs : MeasurableSet s<GOAL>AEMeasurable (fun a => ((condDistrib Y X μ) (X a)) s) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : AEMeasurable X μ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>b : β<VAR>x y : α<GOAL>b ∈ map f s(x, y) ↔ ∃ a ∈ s(x, y), f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>b : β<VAR>x y : α<GOAL>b = f x ∨ b = f y ↔ f x = b ∨ f y = b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s t : Set α<VAR>f : α → E<VAR>x : α<GOAL>‖(s.indicator f - t.indicator f) x‖ = ‖(s ∆ t).indicator f x‖
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h✝ : d₁ ≤ d₂<VAR>s : Set X<VAR>h : d₁ < d₂<GOAL>μH[d₂] s ≤ μH[d₁] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h✝ : d₁ ≤ d₂<VAR>s : Set X<VAR>h : d₁ < d₂<VAR>hs : μH[d₂] s = 0<GOAL>μH[d₂] s ≤ μH[d₁] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d₁ d₂ : ℝ<VAR>h✝ : d₁ ≤ d₂<VAR>s : Set X<VAR>h : d₁ < d₂<VAR>hs : μH[d₁] s = ⊤<GOAL>μH[d₂] s ≤ μH[d₁] s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>(WeierstrassCurve.expDegree (2 * (m + 3)) = 2 * WeierstrassCurve.expDegree (m + 2) + WeierstrassCurve.expDegree (m + 3) + WeierstrassCurve.expDegree (m + 5) ∧ WeierstrassCurve.expDegree (2 * (m + 3)) = WeierstrassCurve.expDegree (m + 1) + WeierstrassCurve.expDegree (m + 3) + 2 * WeierstrassCurve.expDegree (m + 4)) ∧ (WeierstrassCurve.expDegree (2 * (m + 2) + 1) = WeierstrassCurve.expDegree (m + 4) + 3 * WeierstrassCurve.expDegree (m + 2) + if Even m then 2 * 3 else 0) ∧ WeierstrassCurve.expDegree (2 * (m + 2) + 1) = WeierstrassCurve.expDegree (m + 1) + 3 * WeierstrassCurve.expDegree (m + 3) + if Even m then 0 else 2 * 3
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>(2 * ↑(WeierstrassCurve.expDegree (2 * m + 6)) = 2 * (2 * ↑(WeierstrassCurve.expDegree (m + 2))) + 2 * ↑(WeierstrassCurve.expDegree (m + 3)) + 2 * ↑(WeierstrassCurve.expDegree (m + 5)) ∧ 2 * ↑(WeierstrassCurve.expDegree (2 * m + 6)) = 2 * ↑(WeierstrassCurve.expDegree (m + 1)) + 2 * ↑(WeierstrassCurve.expDegree (m + 3)) + 2 * (2 * ↑(WeierstrassCurve.expDegree (m + 4)))) ∧ (2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) = 2 * ↑(WeierstrassCurve.expDegree (m + 4)) + 3 * (2 * ↑(WeierstrassCurve.expDegree (m + 2))) + 2 * if Even m then 6 else 0) ∧ 2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) = 2 * ↑(WeierstrassCurve.expDegree (m + 1)) + 3 * (2 * ↑(WeierstrassCurve.expDegree (m + 3))) + 2 * if Even m then 0 else 6
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) = 2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧ (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) = (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧ ((↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) = (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧ (↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) = (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>((2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) + ((↑m + 5) ^ 2 - if Even m then 1 else 4) ∧ (2 * ↑m + 6) ^ 2 - 4 = ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) + 2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)) ∧ ((2 * ↑m + 4 + 1) ^ 2 - 1 = ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + 2 * if Even m then 6 else 0) ∧ (2 * ↑m + 4 + 1) ^ 2 - 1 = ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) + 2 * if Even m then 0 else 6
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : ReflectsColimit (span f g) F<VAR>e : f ≫ h = g ≫ i<VAR>H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt ≅ H.cocone.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : ReflectsColimit (span f g) F<VAR>e : f ≫ h = g ≫ i<VAR>H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.left ≫ ?refine_1.hom = H.cocone.ι.app WalkingCospan.left
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : ReflectsColimit (span f g) F<VAR>e : f ≫ h = g ≫ i<VAR>H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)<GOAL>((Cocones.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.right ≫ ?refine_1.hom = H.cocone.ι.app WalkingCospan.right
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ico a b ⊆ Icc a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Set.Ico a b ⊆ Set.Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : α → E<VAR>f : α → ℝ≥0∞<VAR>g : α → E<VAR>hf : AEMeasurable f μ<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>hfg : Integrable (fun x => (f x).toReal • g x) μ<GOAL>(μ.withDensityᵥ fun x => (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : α → E<VAR>f : α → ℝ≥0∞<VAR>g : α → E<VAR>hf : AEMeasurable f μ<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>hfg : Integrable (fun x => (f x).toReal • g x) μ<GOAL>(μ.withDensityᵥ fun x => (f x).toReal • g x) = μ.withDensityᵥ ((fun x => (f x).toNNReal) • g)
<VAR>r : ℝ<VAR>n : ℕ<GOAL>r.toNNReal ≤ ↑n ↔ r ≤ ↑n
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Finite<VAR>hs : ∀ i ∈ t, (s i).Finite<VAR>he : ∀ i ∉ t, s i = ∅<GOAL>(⋃ i, s i).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Finite<VAR>hs : ∀ i ∈ t, (s i).Finite<VAR>he : ∀ i ∉ t, s i = ∅<GOAL>⋃ i, s i ⊆ ⋃ i ∈ t, s i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Finite<VAR>hs : ∀ i ∈ t, (s i).Finite<VAR>he : ∀ i ∉ t, s i = ∅<VAR>i : ι<VAR>x : α<VAR>hx : x ∈ s i<GOAL>x ∈ ⋃ i ∈ t, s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<VAR>a b : α<VAR>f : α ↪ β<GOAL>(SimpleGraph.map f G).IsClique (⇑f '' s) ↔ G.IsClique s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<VAR>a b : α<VAR>f : α ↪ β<GOAL>(s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>hs : s.Subsingleton<GOAL>(s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>hs : s.Nontrivial<GOAL>(s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball 1 δ / {x} = ball x⁻¹ δ
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>a_glb : IsGLB s a<VAR>a_mem : a ∈ s<GOAL>⋃ x ∈ s, Ici x = Ici a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>a_glb : IsGLB s a<VAR>a_mem : a ∈ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>Ici x ⊆ Ici a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>a_glb : IsGLB s a<VAR>a_mem : a ∈ s<VAR>x : α<VAR>hx : x ∈ Ici a<GOAL>x ∈ ⋃ i ∈ s, Ici i
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Y' : D<VAR>g : Y ⟶ Y'<GOAL>F.map (𝟙 X, g) ≫ F.map (f, 𝟙 Y') = F.map (f, g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Function.Injective v<VAR>f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv<GOAL>Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Function.Injective v<VAR>f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv<VAR>h : Orthonormal 𝕜 v<GOAL>Orthonormal 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Function.Injective v<VAR>f : ι ≃ ↑(Set.range v) := Equiv.ofInjective v hv<VAR>h : Orthonormal 𝕜 v<GOAL>Orthonormal 𝕜 (v ∘ ⇑(Equiv.ofInjective v hv).symm)
<VAR>x : ℝ<GOAL>(-↑x).abs = (↑x).abs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>ThreeAPFree ↑(sphere n d k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }<GOAL>ThreeAPFree ↑(sphere n d k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }<GOAL>ThreeAPFree (⇑f '' ↑(sphere n d k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }<VAR>x : Fin n → ℕ<GOAL>x ∈ ↑(sphere n d k) → x ∈ ⇑f ⁻¹' Metric.sphere 0 √↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f => Nat.cast ∘ f, map_zero' := ⋯, map_add' := ⋯ }<VAR>x : Fin n → ℕ<GOAL>x ∈ ↑(sphere n d k) → ‖f x‖ = √↑k
<VAR>X Y : TopCat<VAR>f : ↑X ≃ₜ ↑Y<VAR>x✝ : (forget TopCat).obj X<GOAL>(f.toContinuousMap ≫ f.symm.toContinuousMap) x✝ = (𝟙 X) x✝
<VAR>X Y : TopCat<VAR>f : ↑X ≃ₜ ↑Y<VAR>x✝ : (forget TopCat).obj Y<GOAL>(f.symm.toContinuousMap ≫ f.toContinuousMap) x✝ = (𝟙 Y) x✝
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∀ x ∈ s, p x<GOAL>∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∀ x ∈ s, p x<GOAL>∀ x ∈ s, p x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T : Triangle Cᵒᵖ<GOAL>T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T : Triangle Cᵒᵖ<GOAL>Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate ∈ Pretriangulated.distinguishedTriangles
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h₁ : I₁ ≤ I<VAR>h₂ : I₂ ≤ I<GOAL>⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h₁ : I₁ ≤ I<VAR>h₂ : I₂ ≤ I<GOAL>comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<VAR>h₁ : I ⊓ I₁ = I₁<VAR>h₂ : I ⊓ I₂ = I₂<GOAL>comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, 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>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivAt h₂ h₂' (h x)<VAR>hh : HasDerivAt h h' x<VAR>hy : y = h x<GOAL>HasDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>factors' a = factors' b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>h : a ~ᵤ 0<GOAL>factors' a = factors' 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<VAR>hb : b ≠ 0<GOAL>factors' a = factors' b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<VAR>hb : b ≠ 0<VAR>ha : a ≠ 0<GOAL>factors' a = factors' b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<VAR>hb : b ≠ 0<VAR>ha : a ≠ 0<GOAL>Rel Associated (factors a) (factors b)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>t : L[[α]].Term (β ⊕ Fin n)<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs) (constantsVarsEquivLeft t) = realize (Sum.elim v xs) t
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>t : L[[α]].Term (β ⊕ Fin n)<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars = realize (Sum.elim v xs) t
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>t : L[[α]].Term (β ⊕ Fin n)<VAR>v : β → M<VAR>xs : Fin n → M<GOAL>realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars = realize (Sum.elim (fun a => ↑(L.con a)) (Sum.elim v xs)) t.constantsToVars
<VAR>I : Type u<VAR>X : I → TopCat<VAR>x : (i : I) → ↑(π.obj (X i))<GOAL>(Path.Homotopic.pi fun i => ⟦Path.refl (x i).as⟧) = 𝟙 ({ obj := fun g => { as := fun i => (g i).as }, map := fun {X_1 Y} p => Path.Homotopic.pi p }.obj x)
<VAR>I : Type u<VAR>X : I → TopCat<VAR>x : (i : I) → ↑(π.obj (X i))<GOAL>⟦Path.pi fun i => Path.refl (x i).as⟧ = 𝟙 { as := fun i => (x i).as }
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>ha : Even a<VAR>hb : Odd b<GOAL>Odd (a - b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>ha : Even a<VAR>hb : Odd b<GOAL>Odd (a + -b)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<GOAL>M.Basis I {x | M.Basis I (insert x I)}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e✝ : α<VAR>hI : M.Indep I<VAR>e : α<VAR>he : e ∈ I<GOAL>M.Basis I (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e✝ : α<VAR>hI : M.Indep I<VAR>e : α<VAR>he : e ∈ {x | M.Basis I (insert x I)} \ I<VAR>hu : M.Indep (insert e I)<GOAL>e ∈ I
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>v : E<VAR>s : Set ℝ<GOAL>μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>s : Set ℝ<GOAL>μH[1] ((fun r => r • 0) '' s) = ‖0‖₊ • μH[1] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>v : E<VAR>s : Set ℝ<VAR>hv : v ≠ 0<GOAL>μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>v : E<VAR>s : Set ℝ<VAR>hv : v ≠ 0<VAR>hn : ‖v‖ ≠ 0<GOAL>μH[1] ((fun r => r • v) '' s) = ‖v‖₊ • μH[1] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>v : E<VAR>s : Set ℝ<VAR>hv : v ≠ 0<VAR>hn : ‖v‖ ≠ 0<GOAL>μH[1] ((fun x => ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s)) = ‖v‖₊ • μH[1] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>v : E<VAR>s : Set ℝ<VAR>hv : v ≠ 0<VAR>hn : ‖v‖ ≠ 0<VAR>iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))<GOAL>μH[1] ((fun x => ‖v‖ • x) '' (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s)) = ‖v‖₊ • μH[1] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<GOAL>G.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<VAR>this : Nonempty α<GOAL>G.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<VAR>this✝ : Nonempty α<VAR>this : Nonempty β<GOAL>G.Connected
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t