ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<VAR>hε₁ : ε ≤ 1<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<VAR>hε₁ : ε ≤ 1<VAR>this : NoAccidental (Corners.triangleIndices A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<VAR>hε₁ : ε ≤ 1<VAR>this : NoAccidental (Corners.triangleIndices A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : (triangleRemovalBound (ε / 9) * 27)⁻¹ < ↑(Fintype.card G)<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<VAR>hε₁ : ε ≤ 1<VAR>this : NoAccidental (Corners.triangleIndices A)<GOAL>0 < triangleRemovalBound (ε / 9) * 27
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<VAR>hε₁ : ε ≤ 1<VAR>this : NoAccidental (Corners.triangleIndices A)<GOAL>triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 ≤ 1 * ↑(Fintype.card G) ^ 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<GOAL>f - g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (f - g) x ∂μ = 0<GOAL>f - g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (f - g) x ∂μ = 0<VAR>hfg_int : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (f - g) s μ<GOAL>f - g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<GOAL>0 = hammingDist x y ↔ x = y
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : -s.re < ↑n<VAR>u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s<GOAL>Gamma s = GammaAux n s
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : -s.re < ↑n<VAR>u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s<GOAL>n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)
<VAR>s : ℂ<VAR>n : ℕ<VAR>h1 : -s.re < ↑n<VAR>u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s<GOAL>⌊1 - s.re⌋₊ ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>h : xs.Disjoint ys<GOAL>(xs ++ ys).dedup = xs.dedup ++ ys.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>h : xs.Disjoint ys<GOAL>xs.Disjoint ys.dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>h : xs.Disjoint ys<VAR>a : α<VAR>hx : a ∈ xs<VAR>hy : a ∈ ys.dedup<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>f : R[X]<VAR>hf : ¬f = 0<VAR>i : ℕ<GOAL>i ∈ f.integralNormalization.support ↔ i ∈ f.support
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>f : R[X]<VAR>hf : ¬f = 0<VAR>i : ℕ<GOAL>i ∈ f.support → i ∈ f.integralNormalization.support
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsDomain R<VAR>f : R[X]<VAR>hf : ¬f = 0<VAR>i : ℕ<GOAL>f.coeff i ≠ 0 → (if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, J⁆ ≤ I
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅J, I⁆ ≤ I
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h : decide (num✝¹ * ↑db < num✝ * ↑da) = true<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true<VAR>h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true<VAR>h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)<VAR>ha : 0 < ⅟↑da<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true<VAR>h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)<VAR>ha : 0 < ⅟↑da<VAR>hb : 0 < ⅟↑db<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true<VAR>h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)<VAR>ha : 0 < ⅟↑da<VAR>hb : 0 < ⅟↑db<VAR>h : ⅟↑db * ((fun x => ↑x) (num✝¹ * ↑db) * ⅟↑da) < ⅟↑db * ((fun x => ↑x) (num✝ * ↑da) * ⅟↑da)<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true<VAR>h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)<VAR>ha : 0 < ⅟↑da<VAR>hb : 0 < ⅟↑db<VAR>h : ↑(num✝¹ * ↑db) * ⅟↑db * ⅟↑da < ⅟↑db * ((fun x => ↑x) (num✝ * ↑da) * ⅟↑da)<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Nontrivial α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true<VAR>h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)<VAR>ha : 0 < ⅟↑da<VAR>hb : 0 < ⅟↑db<VAR>h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝<GOAL>↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
<VAR>x y : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hy₂ : y ≤ π<VAR>hxy : x < y<GOAL>cos y < cos x
<VAR>x y : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hy₂ : y ≤ π<VAR>hxy : x < y<GOAL>sin (π / 2 - y) < sin (π / 2 - x)
<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>h₁ : LieAlgebra.IsNilpotent R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L' L' k = ⊥<GOAL>∃ k, lowerCentralSeries R L L k = ⊥
<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>h₁ : LieAlgebra.IsNilpotent R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L' L' k = ⊥<GOAL>lowerCentralSeries R L L k = ⊥
<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>h₁ : LieAlgebra.IsNilpotent R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L' L' k = ⊥<GOAL>LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
<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>h₁ : LieAlgebra.IsNilpotent R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L' L' k = ⊥<GOAL>LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<GOAL>P.IsEquipartition ↔ ∀ a ∈ P.parts, a.card = s.card / P.parts.card ∨ a.card = s.card / P.parts.card + 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hx : ¬IsIntegral K x<GOAL>(Algebra.trace K ↥K⟮x⟯) (gen K x) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hx : ¬IsIntegral K x<GOAL>¬∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hx : ∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)<GOAL>IsIntegral K x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>s : Finset ↥K⟮x⟯<VAR>b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯<GOAL>IsIntegral K x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>s : Finset ↥K⟮x⟯<VAR>b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯<GOAL>(Subalgebra.toSubmodule K⟮x⟯.toSubalgebra).FG
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>s : Finset ↥K⟮x⟯<VAR>b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯<GOAL>x ∈ K⟮x⟯.toSubalgebra
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<VAR>gp : Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.nums 1 = gp.b * g.h + gp.a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>m : MeasurableSpace α<VAR>f : α → β<GOAL>⊥ ∈ {a | ∀ᶠ (n : β) in map f (ae 0), n ≤ a}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedCancelAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>p q : E × β<VAR>hp : p.1 ∈ s ∧ f p.1 < p.2<VAR>hq : q.1 ∈ s ∧ f q.1 ≤ q.2<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • p + b • q ∈ {p | p.1 ∈ s ∧ f p.1 < p.2}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedCancelAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>p q : E × β<VAR>hp : p.1 ∈ s ∧ f p.1 < p.2<VAR>hq : q.1 ∈ s ∧ f q.1 ≤ q.2<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f (a • p + b • q).1 < (a • p + b • q).2
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<GOAL>quadraticCharFun F 1 = 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>PInfty.f n ≫ PInfty.f n = PInfty.f n
<VAR>n : ℕ<GOAL>n.properDivisors = ∅ ↔ n ≤ 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>B : Set (ι × α)<GOAL>(Matroid.sum' M).Base B ↔ ∀ (i : ι), (M i).Base (Prod.mk i ⁻¹' B)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>B : Set (ι × α)<GOAL>(∀ (i : ι), (M i).Base (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B))) ↔ ∀ (i : ι), (M i).Base (Prod.mk i ⁻¹' B)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>B : Set (ι × α)<VAR>a✝ : ι<GOAL>Prod.mk a✝ ⁻¹' B = Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' B)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<GOAL>Tendsto (fun x => r * f x) l atBot ↔ r < 0
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}<VAR>a_in : a ∈ H<VAR>a_pos : 0 < a<GOAL>H = closure {a}
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}<VAR>a_in : a ∈ H<VAR>a_pos : 0 < a<GOAL>H ≤ closure {a}
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}<VAR>a_in : a ∈ H<VAR>a_pos : 0 < a<VAR>g : G<VAR>g_in : g ∈ H<GOAL>g ∈ closure {a}
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}<VAR>a_in : a ∈ H<VAR>a_pos : 0 < a<VAR>g : G<VAR>g_in : g ∈ H<VAR>k : ℤ<VAR>right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k<VAR>nonneg : 0 ≤ g - k • a<VAR>lt : g - k • a < a<GOAL>g ∈ closure {a}
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}<VAR>a_in : a ∈ H<VAR>a_pos : 0 < a<VAR>g : G<VAR>g_in : g ∈ H<VAR>k : ℤ<VAR>right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k<VAR>nonneg : 0 ≤ g - k • a<VAR>lt : g - k • a < a<VAR>h_zero : g - k • a = 0<GOAL>g ∈ closure {a}
<VAR>e : ℤˣ<GOAL>‖↑e‖ = 1
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂✝ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>S₂ : Type u_2<VAR>inst✝ : CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>w = w⁻¹⁻¹
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<VAR>ht : t ∈ measurableCylinders α<GOAL>s \ t ∈ measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<VAR>ht : t ∈ measurableCylinders α<GOAL>tᶜ ∩ s ∈ measurableCylinders α
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K✝ : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M''<VAR>inst✝⁸ : Module R M✝<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M''<VAR>a b : R<VAR>x y : M✝<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>inst✝⁵ : CommSemiring K<VAR>inst✝⁴ : Semiring M<VAR>inst✝³ : Algebra K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>LinearIndependent L AlgHom.toLinearMap
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K✝ : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M''<VAR>inst✝⁸ : Module R M✝<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M''<VAR>a b : R<VAR>x y : M✝<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>inst✝⁵ : CommSemiring K<VAR>inst✝⁴ : Semiring M<VAR>inst✝³ : Algebra K M<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<GOAL>LinearIndependent L (⇑(ltoFun K M L) ∘ AlgHom.toLinearMap)
<VAR>n m : ℕ<VAR>i j : Fin n<GOAL>i < j.rev ↔ j < i.rev
<VAR>u v : Level<VAR>n : ℕ<VAR>pn : NormNum.IsNat n 0<GOAL>Finset.range n = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<GOAL>LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<GOAL>(∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
<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>x y : E<GOAL>⟪x, y⟫_𝕜 = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4
<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>x y : E<GOAL>↑((‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4) + ↑((‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4) * I = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4
<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>x y : E<GOAL>(↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖) / 4 + (↑‖x - I • y‖ * ↑‖x - I • y‖ - ↑‖x + I • y‖ * ↑‖x + I • y‖) / 4 * I = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<GOAL>p.toOuterMeasure (s ∩ p.support) = p.toOuterMeasure s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.60827, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryExtensive C<VAR>inst✝¹ : ∀ (X : C), Projective X<VAR>inst✝ : PreservesFiniteProducts s<VAR>hF : IsSheaf (coherentTopology C) F<GOAL>IsSheaf (coherentTopology C) (F ⋙ s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.60827, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝⁴ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryExtensive C<VAR>inst✝¹ : ∀ (X : C), Projective X<VAR>inst✝ : PreservesFiniteProducts s<VAR>hF : Nonempty (PreservesFiniteProducts F)<GOAL>Nonempty (PreservesFiniteProducts (F ⋙ s))
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>S : Subalgebra R A<VAR>a : A<VAR>ha : a ∈ (S ⊔ star S).carrier<GOAL>star a ∈ (S ⊔ star S).carrier