ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>g : γ → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : γ), g c ∂κ.snd a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂)) = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂)) = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>span {XClass W x₁ * XClass W x₂, XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)), YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂, YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>span {XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * (mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {XClass W x₁ * (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔ span {XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ (span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)})) * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) = YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔ span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>(span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)})) * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} = span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>span {XClass W x₁} ⊔ (span {XClass W x₂} ⊔ span {(mk W) (Y - W.negPolynomial)}) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c<GOAL>∃ x, (∃ a a_1 a_2, a_2 * (Y - W.negPolynomial) = x + a * C (X - C x₁) + a_1 * C (X - C x₂)) ∧ (AdjoinRoot.mk W.polynomial) x = 1
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>A : Fin n → Fq[X]<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>A : Fin n → Fq[X]<VAR>t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet (fun p => f p.1 < p.2) (μ.prod volume)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet (fun p => p.2 < g p.1) (μ.prod volume)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>a : α<VAR>f : Filter β<GOAL>pure a ×ˢ f = map (Prod.mk a) f
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>U : M → Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ support ↑(fs.toFun (fs.ind x hx))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)<GOAL>inst✝⁸ = MeasurableSpace.generateFrom ?convert_2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)<GOAL>Set (Set α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)<GOAL>∀ t ∈ ?convert_2, MeasurableSet (f ⁻¹' t)
<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 : E<GOAL>re ⟪x, x⟫_𝕜 ≤ 0 ↔ x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝⁴ : NonUnitalSemiring α<VAR>inst✝³ : StarRing α<VAR>inst✝² : NonUnitalSemiring β<VAR>inst✝¹ : StarRing β<VAR>inst✝ : Fintype n<VAR>A : Matrix m n α<GOAL>(A * Aᴴ).IsHermitian
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>(X - C ((starRingEnd ℂ) z)) * (X - C z) ∣ map (algebraMap ℝ ℂ) p
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>IsCoprime (X - C ((starRingEnd ℂ) z)) (X - C z)
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>X - C ((starRingEnd ℂ) z) ∣ map (algebraMap ℝ ℂ) p
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>X - C z ∣ map (algebraMap ℝ ℂ) p
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<VAR>h : x = yᶜ<GOAL>IsCompl yᶜ y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>s t : Set α<VAR>l : Filter α<GOAL>s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
<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✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hab : IntervalIntegrable f volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f la' volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb' volume<VAR>ha_lim : Tendsto f (la' ⊓ ae volume) (𝓝 ca)<VAR>hb_lim : Tendsto f (lb' ⊓ ae volume) (𝓝 cb)<VAR>hua : Tendsto ua lt la<VAR>hva : Tendsto va lt la<VAR>hub : Tendsto ub lt lb<VAR>hvb : Tendsto vb lt lb<GOAL>(fun t => ((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) - ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt] fun t => ‖va t - ua t‖ + ‖vb t - ub t‖
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l₂ : List α<VAR>h : a ∈ l₂<VAR>l₁ : List α<GOAL>(a :: l₁).diff l₂ = l₁.diff (l₂.erase a)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : L₃ ⟶ L₂<VAR>b : B<GOAL>((mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β)).app b = (rightAdjointSquareConjugate.vcomp ((mateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : L₃ ⟶ L₂<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<GOAL>((mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β)).app b = (rightAdjointSquareConjugate.vcomp ((mateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : L₃ ⟶ L₂<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft G (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) ≫ whiskerRight α (𝟭 D)) = whiskerRight ((mateEquiv adj₁ adj₂) α) (𝟭 C) ≫ whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<GOAL>((mateEquiv adj₁ adj₃) (whiskerLeft G β ≫ α)).app b = ((mateEquiv adj₁ adj₂) α ≫ whiskerLeft H ((Trans.trans (Trans.trans (L₃.leftUnitor.homCongr L₂.rightUnitor).symm (mateEquiv adj₂ adj₃)) (R₂.rightUnitor.homCongr R₃.leftUnitor)) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : L₃ ⟶ L₂<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft G (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) ≫ whiskerRight α (𝟭 D)) = whiskerRight ((mateEquiv adj₁ adj₂) α) (𝟭 C) ≫ whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<VAR>vcompb : ((mateEquiv adj₁ adj₃) (whiskerLeft G (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) ≫ whiskerRight α (𝟭 D))).app b = (whiskerRight ((mateEquiv adj₁ adj₂) α) (𝟭 C) ≫ whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))).app b<GOAL>((mateEquiv adj₁ adj₃) (whiskerLeft G β ≫ α)).app b = ((mateEquiv adj₁ adj₂) α ≫ whiskerLeft H ((Trans.trans (Trans.trans (L₃.leftUnitor.homCongr L₂.rightUnitor).symm (mateEquiv adj₂ adj₃)) (R₂.rightUnitor.homCongr R₃.leftUnitor)) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : L₃ ⟶ L₂<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft G (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) ≫ whiskerRight α (𝟭 D)) = whiskerRight ((mateEquiv adj₁ adj₂) α) (𝟭 C) ≫ whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<VAR>vcompb : adj₃.unit.app (G.obj (R₁.obj b)) ≫ R₃.map (β.app (G.obj (R₁.obj b))) ≫ R₃.map (α.app (R₁.obj b)) ≫ R₃.map (H.map (adj₁.counit.app b)) = adj₂.unit.app (G.obj (R₁.obj b)) ≫ R₂.map (α.app (R₁.obj b)) ≫ R₂.map (H.map (adj₁.counit.app b)) ≫ adj₃.unit.app (R₂.obj (H.obj b)) ≫ R₃.map (β.app (R₂.obj (H.obj b))) ≫ R₃.map (adj₂.counit.app (H.obj b))<GOAL>({ toFun := fun α => whiskerLeft (R₁ ⋙ G) adj₃.unit ≫ whiskerRight (whiskerLeft R₁ α) R₃ ≫ whiskerRight adj₁.counit (H ⋙ R₃), invFun := fun β => whiskerRight adj₁.unit (G ⋙ L₃) ≫ whiskerRight (whiskerLeft L₁ β) L₃ ≫ whiskerLeft (L₁ ⋙ H) adj₃.counit, left_inv := ⋯, right_inv := ⋯ } (whiskerLeft G β ≫ α)).app b = ({ toFun := fun α => whiskerLeft (R₁ ⋙ G) adj₂.unit ≫ whiskerRight (whiskerLeft R₁ α) R₂ ≫ whiskerRight adj₁.counit (H ⋙ R₂), invFun := fun β => whiskerRight adj₁.unit (G ⋙ L₂) ≫ whiskerRight (whiskerLeft L₁ β) L₂ ≫ whiskerLeft (L₁ ⋙ H) adj₂.counit, left_inv := ⋯, right_inv := ⋯ } α ≫ whiskerLeft H ((Trans.trans (Trans.trans (L₃.leftUnitor.homCongr L₂.rightUnitor).symm { toFun := fun α => whiskerLeft (R₂ ⋙ 𝟭 C) adj₃.unit ≫ whiskerRight (whiskerLeft R₂ α) R₃ ≫ whiskerRight adj₂.counit (𝟭 D ⋙ R₃), invFun := fun β => whiskerRight adj₂.unit (𝟭 C ⋙ L₃) ≫ whiskerRight (whiskerLeft L₂ β) L₃ ≫ whiskerLeft (L₂ ⋙ 𝟭 D) adj₃.counit, left_inv := ⋯, right_inv := ⋯ }) (R₂.rightUnitor.homCongr R₃.leftUnitor)) β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>G : A ⥤ C<VAR>H : B ⥤ D<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : C ⥤ D<VAR>R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : L₃ ⟶ L₂<VAR>b : B<VAR>vcomp : (mateEquiv adj₁ adj₃) (whiskerLeft G (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv) ≫ whiskerRight α (𝟭 D)) = whiskerRight ((mateEquiv adj₁ adj₂) α) (𝟭 C) ≫ whiskerLeft H ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<VAR>vcompb : adj₃.unit.app (G.obj (R₁.obj b)) ≫ R₃.map (β.app (G.obj (R₁.obj b))) ≫ R₃.map (α.app (R₁.obj b)) ≫ R₃.map (H.map (adj₁.counit.app b)) = adj₂.unit.app (G.obj (R₁.obj b)) ≫ R₂.map (α.app (R₁.obj b)) ≫ R₂.map (H.map (adj₁.counit.app b)) ≫ adj₃.unit.app (R₂.obj (H.obj b)) ≫ R₃.map (β.app (R₂.obj (H.obj b))) ≫ R₃.map (adj₂.counit.app (H.obj b))<GOAL>adj₃.unit.app (G.obj (R₁.obj b)) ≫ R₃.map (β.app (G.obj (R₁.obj b))) ≫ R₃.map (α.app (R₁.obj b)) ≫ R₃.map (H.map (adj₁.counit.app b)) = adj₂.unit.app (G.obj (R₁.obj b)) ≫ R₂.map (α.app (R₁.obj b)) ≫ R₂.map (H.map (adj₁.counit.app b)) ≫ adj₃.unit.app (R₂.obj (H.obj b)) ≫ R₃.map (β.app (R₂.obj (H.obj b))) ≫ R₃.map (adj₂.counit.app (H.obj b))
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S<GOAL>λ ^ (S.multiplicity + 1) ∣ S.c
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S<GOAL>λ ^ S.multiplicity * λ ∣ S.c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>y : β<VAR>hs : autoParam s.Finite _auto✝<GOAL>{x | x ∈ s ∧ f x = y}.ncard ≠ 0 ↔ y ∈ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>y : β<VAR>hs : autoParam s.Finite _auto✝<GOAL>y ∈ f '' s → {x | x ∈ s ∧ f x = y}.ncard ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>z : α<VAR>hz : z ∈ s<GOAL>{x | x ∈ s ∧ f x = f z}.ncard ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>ι : Type u_3<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsPreconnected (s i)<VAR>K : ∀ (i j : ι), ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j<GOAL>IsPreconnected (⋃ n, s n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>ι : Type u_3<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsPreconnected (s i)<VAR>K : ∀ (i j : ι), ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j<GOAL>IsPreconnected (⋃ x ∈ univ, s x)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a (b - p) = toIocDiv hp a b - 1
<VAR>n : ℕ<VAR>hn : 1 < n<VAR>w z : ℂ<GOAL>‖↑n ^ w‖ ≤ ‖↑n ^ z‖ ↔ w.re ≤ z.re
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>s : Stream' α<GOAL>map f s = f s.head :: map f s.tail
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : Cardinal.{u_2}<VAR>ha : ℵ₀ ≤ a<VAR>b1 : 1 < b<GOAL>a < (b ^ a).ord.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : Cardinal.{u_2}<VAR>ha : ℵ₀ ≤ a<VAR>b1 : 1 < b<VAR>b0 : b ≠ 0<GOAL>a < (b ^ a).ord.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : Cardinal.{u_2}<VAR>ha : ℵ₀ ≤ a<VAR>b1 : 1 < b<VAR>b0 : b ≠ 0<GOAL>(b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof