ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Ico (b ^ n) (b ^ (n + 1)))
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>h : Submodule.span ℝ {y} = Submodule.span ℝ {z}<GOAL>2 • o.oangle x y = 2 • o.oangle x z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>h : ∃ z_1, z_1 • y = z<GOAL>2 • o.oangle x y = 2 • o.oangle x z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝˣ<GOAL>2 • o.oangle x y = 2 • o.oangle x (r • y)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<GOAL>σ ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<GOAL>∀ (n : ℕ) (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<VAR>hn : l.length = 2 * (n + 1)<GOAL>l.prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ l, g.IsSwap<VAR>hn : l.length = 2 * n + 2<GOAL>l.prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>a : Perm α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ a :: l, g.IsSwap<VAR>hn : (a :: l).length = 2 * n + 2<GOAL>(a :: l).prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>a : Perm α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ a :: l, g.IsSwap<VAR>hn : l.length = 2 * n + 1<GOAL>(a :: l).prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>a b : Perm α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ a :: b :: l, g.IsSwap<VAR>hn : (b :: l).length = 2 * n + 1<GOAL>(a :: b :: l).prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>a b : Perm α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ a :: b :: l, g.IsSwap<VAR>hn : (b :: l).length = 2 * n + 1<GOAL>a * b * l.prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ∈ alternatingGroup α<VAR>n : ℕ<VAR>ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}<VAR>a b : Perm α<VAR>l : List (Perm α)<VAR>hl : ∀ g ∈ a :: b :: l, g.IsSwap<VAR>hn : l.length = 2 * n<GOAL>a * b * l.prod ∈ closure {σ | σ.IsThreeCycle}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<GOAL>Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu✝ : IsUnit u✝<VAR>u : R<VAR>hu : IsUnit u<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular (u • P)<GOAL>W'.Nonsingular P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu✝ : IsUnit u✝<VAR>u : R<VAR>hu : IsUnit u<VAR>P : Fin 3 → R<VAR>hP✝ : W'.Nonsingular (u • P)<VAR>hP : W'.Equation (u • P)<VAR>hP' : W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) ≠ 0 ∨ 2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 ≠ 0 ∨ W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 - (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) ≠ 0<GOAL>W'.Nonsingular P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu✝ : IsUnit u✝<VAR>u : R<VAR>hu : IsUnit u<VAR>P : Fin 3 → R<VAR>hP✝ : W'.Nonsingular (u • P)<VAR>hP : W'.Equation (u • P)<VAR>hP' : W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) ≠ 0 ∨ 2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 ≠ 0 ∨ W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 - (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) ≠ 0<GOAL>W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨ 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨ W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu✝ : IsUnit u✝<VAR>u : R<VAR>hu : IsUnit u<VAR>P : Fin 3 → R<VAR>hP✝ : W'.Nonsingular (u • P)<VAR>hP : W'.Equation (u • P)<VAR>hP' : W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) = 0 ∧ 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 = 0 ∧ W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) = 0<GOAL>W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z ^ 2 + W'.a₄ * (u • P) z ^ 4) = 0 ∧ 2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 3 = 0 ∧ W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * (u • P) z ^ 2 - (2 * W'.a₂ * (u • P) x ^ 2 * (u • P) z + 4 * W'.a₄ * (u • P) x * (u • P) z ^ 3 + 6 * W'.a₆ * (u • P) z ^ 5) = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu✝ : IsUnit u✝<VAR>u : R<VAR>hu : IsUnit u<VAR>P : Fin 3 → R<VAR>hP✝ : W'.Nonsingular (u • P)<VAR>hP : W'.Equation (u • P)<VAR>hP' : W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) = 0 ∧ 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 = 0 ∧ W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) = 0<GOAL>W'.a₁ * (u ^ 3 * P y) * (u * P z) - (3 * (u ^ 2 * P x) ^ 2 + 2 * W'.a₂ * (u ^ 2 * P x) * (u * P z) ^ 2 + W'.a₄ * (u * P z) ^ 4) = 0 ∧ 2 * (u ^ 3 * P y) + W'.a₁ * (u ^ 2 * P x) * (u * P z) + W'.a₃ * (u * P z) ^ 3 = 0 ∧ W'.a₁ * (u ^ 2 * P x) * (u ^ 3 * P y) + 3 * W'.a₃ * (u ^ 3 * P y) * (u * P z) ^ 2 - (2 * W'.a₂ * (u ^ 2 * P x) ^ 2 * (u * P z) + 4 * W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 3 + 6 * W'.a₆ * (u * P z) ^ 5) = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<VAR>this : ∀ {u : R}, IsUnit u → ∀ {P : Fin 3 → R}, W'.Nonsingular (u • P) → W'.Nonsingular P<VAR>h : W'.Nonsingular P<GOAL>W'.Nonsingular (↑hu.unit⁻¹ • u • P)
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ≥0<VAR>r : ℝ<GOAL>(List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ≥0<VAR>r : ℝ<GOAL>(List.map (fun x => f x ^ r) l).prod = (List.map ((fun x => x ^ r) ∘ f) l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>a✝ : α<VAR>b✝ : β<VAR>l₁✝ : List α<VAR>l₂✝ : List β<VAR>h₁ : R a✝ b✝<VAR>h₂ : Forall₂ R l₁✝ l₂✝<GOAL>Forall₂ R (a✝ :: l₁✝).reverse (b✝ :: l₂✝).reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>a✝ : α<VAR>b✝ : β<VAR>l₁✝ : List α<VAR>l₂✝ : List β<VAR>h₁ : R a✝ b✝<VAR>h₂ : Forall₂ R l₁✝ l₂✝<GOAL>Forall₂ R (l₁✝.reverse ++ [a✝]) (l₂✝.reverse ++ [b✝])
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumsphere = sx₂.circumsphere
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<VAR>r : Sphere P<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r<GOAL>sx₁.circumsphere = sx₂.circumsphere
<VAR>α : Type u<VAR>x y n : ℕ<GOAL>x - y ∣ x ^ n - y ^ n
<VAR>α : Type u<VAR>x y n : ℕ<VAR>h : y ≤ x<GOAL>x - y ∣ x ^ n - y ^ n
<VAR>α : Type u<VAR>x y n : ℕ<VAR>h : x < y<GOAL>x - y ∣ x ^ n - y ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hx : p x ∈ (convexHull 𝕜) (p '' s)<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hx : p x ∈ (convexHull 𝕜) (p '' s)<VAR>hp : Injective p<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hx : p x ∈ ⋃ t, ⋃ (_ : ↑t ⊆ p '' s), (convexHull 𝕜) ↑t<VAR>hp : Injective p<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>hx : ∃ i, ∃ (_ : ↑i ⊆ p '' s), p x ∈ (convexHull 𝕜) ↑i<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>t : Finset E<VAR>ht : ↑t ⊆ p '' s<VAR>hx : p x ∈ (convexHull 𝕜) ↑t<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>t : Finset E<VAR>ht : ↑t ⊆ p '' s<VAR>hx : p x ∈ (convexHull 𝕜) ↑t<GOAL>p x ∈ p '' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>t : Finset E<VAR>ht : ↑t ⊆ p '' s<VAR>hx : p x ∈ (convexHull 𝕜) ↑t<GOAL>p x ∈ ↑t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>t : Finset E<VAR>ht : ↑t ⊆ p '' s<VAR>hx : p x ∈ (convexHull 𝕜) ↑t<GOAL>x ∈ t.preimage p ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>t : Finset E<VAR>ht : ↑t ⊆ p '' s<VAR>hx : p x ∈ (convexHull 𝕜) ↑t<GOAL>p x ∈ (convexHull 𝕜) ↑(image p (t.preimage p ⋯))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ : Set E<VAR>p : ι → E<VAR>h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s<VAR>s : Set ι<VAR>x : ι<VAR>hp : Injective p<VAR>t : Finset E<VAR>ht : ↑t ⊆ p '' s<VAR>hx : p x ∈ (convexHull 𝕜) ↑t<GOAL>∀ x ∈ t, x ∈ Set.range p
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : Field 𝕂<VAR>inst✝³ : Ring 𝔸<VAR>inst✝² : Algebra 𝕂 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<VAR>n : ℕ<GOAL>((expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁴ : Field 𝕂<VAR>inst✝³ : Ring 𝔸<VAR>inst✝² : Algebra 𝕂 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<VAR>n : ℕ<GOAL>(↑n !)⁻¹ • 0 ^ n = Pi.single 0 1 n
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>A B : J<VAR>f : A ⟶ B<GOAL>𝟙 c.pt ≫ c.π.app B = c.π.app A ≫ (D.map f).f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>A B : J<VAR>f : A ⟶ B<GOAL>c.π.app ?m.210336 ≫ (D ⋙ T.forget).map ?h = c.π.app A ≫ (D.map f).f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>A B : J<VAR>f : A ⟶ B<GOAL>?m.210336 ⟶ B
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>A B : J<VAR>f : A ⟶ B<GOAL>J
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>hi : i ∈ s<VAR>w : ι → k<VAR>hw : s.sum w = 1<GOAL>(b.coord i) ((Finset.affineCombination k s ⇑b) w) = w i
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>s' s : Heap α<VAR>eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'<GOAL>s.realSize = s'.realSize + 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>S : Type u_4<VAR>inst✝³ : Monoid S<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DistribMulAction S M<VAR>sR : Set R<VAR>s : Set S<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ s • ⊥<GOAL>x ∈ ⊥
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T1Space X<VAR>inst✝¹ : DecidableEq X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<GOAL>ContinuousOn (update f x y) s ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T1Space X<VAR>inst✝¹ : DecidableEq X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<GOAL>(∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b) ∧ (x ∈ s → ContinuousWithinAt (update f x y) s x) ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T1Space X<VAR>inst✝¹ : DecidableEq X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>H : ∀ (b : X), b ≠ x → b ∈ s → ContinuousWithinAt (update f x y) s b<VAR>z : X<VAR>hz : z ∈ s \ {x}<GOAL>ContinuousWithinAt f (s \ {x}) z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T1Space X<VAR>inst✝¹ : DecidableEq X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>H : ContinuousOn f (s \ {x})<VAR>z : X<VAR>hzx : z ≠ x<VAR>hzs : z ∈ s<GOAL>ContinuousWithinAt (update f x y) s z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T1Space X<VAR>inst✝¹ : DecidableEq X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>x✝ : x ∈ s<GOAL>ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)
<VAR>x n m : ℕ<VAR>h : x < 2 ^ n<GOAL>x <<< m < 2 ^ (n + m)
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1<VAR>z x y : ℕ<VAR>x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x<VAR>c : ℕ<VAR>hc : z + y * c = x<VAR>hl : z < y<GOAL>z % y = z
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1<VAR>z x y : ℕ<VAR>e : x % y = z<GOAL>(y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => f n ω) atTop atBot
<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<GOAL>eLpNormEssSup 0 μ = 0
<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<GOAL>essSup (fun x => ⊥) μ = ⊥
<VAR>a : ℕ<GOAL>Periodic a.gcd a
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>γ : Cochain F G n<VAR>p q' : ℤ<VAR>hpq : p + n = q'<GOAL>γ.v p q' hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).inv = γ.v p q' ⋯
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Group α<VAR>a b : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : 1 ≤ a<VAR>hab : a ≤ b<GOAL>mabs a ≤ mabs b
<VAR>m n✝ n : ℤ<GOAL>∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
<VAR>m n k : ℤ<GOAL>Xor' (k + k = 2 * k) (k + k = 2 * k + 1)
<VAR>m n k : ℤ<GOAL>Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : #↑s ≤ 𝔠<GOAL>max (#↑s) 2 ^ ℵ₀ ≤ 𝔠
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : #↑s ≤ 𝔠<GOAL>max (#↑s) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<GOAL>All p (match l, v, r with | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d) | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d) | a, x, b => node black a x b) ↔ p v ∧ All p l ∧ All p r
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.98653, u_1} J<VAR>inst✝ : Category.{?u.99132, u_2} C<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>s : ↑(F ⋙ yoneda.obj X).sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>𝟙 (op X) ≫ (↑s j').op = (↑s j).op ≫ F.map f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.98653, u_1} J<VAR>inst✝ : Category.{?u.99132, u_2} C<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>s : ↑(F ⋙ yoneda.obj X).sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>(↑s j').op = (↑s j).op ≫ F.map f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.98653, u_1} J<VAR>inst✝ : Category.{?u.99132, u_2} C<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>τ : (const J).obj (op X) ⟶ F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>Quiver.Hom.op ((F ⋙ yoneda.obj X).map f ((fun j => (τ.app j).unop) j)) = ((fun j => (τ.app j).unop) j').op
<VAR>R : Type u_1<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>{ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔ c ≤ d
<VAR>R : Type u_1<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>(∀ {x y : Rᵐᵒᵖ}, ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y → ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔ ∀ {x y : R}, c x y → d x y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>n : ℕ<GOAL>(a + b) ^ (n + n) ≤ 2 ^ (n + n - 1) * (a ^ (n + n) + b ^ (n + n))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>n : ℕ<GOAL>((a + b) ^ 2) ^ n ≤ 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))