ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.34757, u_1} C₁<VAR>inst✝⁴ : Category.{?u.34761, u_2} C₂<VAR>inst✝³ : Category.{?u.34765, u_3} C₃<VAR>inst✝² : Category.{?u.34769, u_4} C₄<VAR>inst✝¹ : Category.{?u.34773, u_5} C₁₂<VAR>inst✝ : Category.{?u.34777, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>α : F ⟶ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>φ : X₂ ⟶ Y₂<VAR>X₃ : GradedObject I₃ C₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<GOAL>((F.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃) ≫ ((α.app (X₁ i₁)).app (Y₂ i₂)).app (X₃ i₃) = ((α.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((F'.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.34757, u_1} C₁<VAR>inst✝⁴ : Category.{?u.34761, u_2} C₂<VAR>inst✝³ : Category.{?u.34765, u_3} C₃<VAR>inst✝² : Category.{?u.34769, u_4} C₄<VAR>inst✝¹ : Category.{?u.34773, u_5} C₁₂<VAR>inst✝ : Category.{?u.34777, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>α : F ⟶ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<GOAL>((F.map (φ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((α.app (Y₁ i₁)).app (X₂ i₂)).app (X₃ i₃) = ((α.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((F'.map (φ i₁)).app (X₂ i₂)).app (X₃ i₃)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝¹ : UniformSpace β<VAR>l : Filter ((i : ι) → α i)<VAR>inst✝ : l.NeBot<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>x : ℂ<VAR>f' : E<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>update f i '' Icc a (f i) = Icc (update f i a) f
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ ≃ᵐ ℝ<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>g : ℝ → ℝ<VAR>hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (⇑f '' s) volume<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x<GOAL>(Measure.map (⇑f.symm) (volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ ≃ᵐ ℝ<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>g : ℝ → ℝ<VAR>hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (⇑f '' s) volume<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>p q : Prop<VAR>α : Sort u_1<VAR>s✝ : α → Prop<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>s : Set β<VAR>A : ∀ (x : β), ¬x ∈ ∅<GOAL>(¬s.Nonempty) = (s = ∅)
<VAR>p q : Prop<VAR>α : Sort u_1<VAR>s✝ : α → Prop<VAR>β : Type u_2<VAR>inst✝ : LinearOrder β<VAR>s : Set β<VAR>A : ∀ (x : β), ¬x ∈ ∅<GOAL>(∀ (x : β), ¬x ∈ s) ↔ s = ∅
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithBot α<GOAL>a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithBot α<GOAL>(if a = 0 ∨ b = 0 then 0 else map₂ (fun x x_1 => x * x_1) a b) = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
<VAR>u v : ℤ<VAR>hu : IsUnit u<GOAL>u = 1 ∨ u = -1
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<VAR>A : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂μ.prod ν<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.prod ν)<VAR>A : ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (z : α × β), AEMeasurable.mk f hf z ∂μ.prod ν<VAR>B : ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), AEMeasurable.mk f hf (x, y) ∂ν ∂μ<GOAL>∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y U : Scheme<VAR>f : Y ⟶ U<VAR>g : U ⟶ X<VAR>h : IsOpenImmersion g<VAR>V : U.Opens<GOAL>f ⁻¹ᵁ V = (f ≫ g) ⁻¹ᵁ g ''ᵁ V
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y U : Scheme<VAR>f : Y ⟶ U<VAR>g : U ⟶ X<VAR>h : IsOpenImmersion g<VAR>V : U.Opens<GOAL>f ⁻¹ᵁ V = (Opens.map f.val.base).obj ((Opens.map g.val.base).obj (g ''ᵁ V))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y U : Scheme<VAR>f : Y ⟶ U<VAR>g : U ⟶ X<VAR>h : IsOpenImmersion g<VAR>V : U.Opens<GOAL>↑V = ↑((Opens.map g.val.base).obj (g ''ᵁ V))
<VAR>α✝¹ : Type u_1<VAR>G : Type u_2<VAR>α✝ : Type u_3<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : Div G<VAR>m✝ : MeasurableSpace α✝<VAR>f✝ g✝ : α✝ → G<VAR>μ✝ : Measure α✝<VAR>α : Type u_4<VAR>E : Type u_5<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : AddGroup E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : MeasurableSub₂ E<VAR>hm : m ≤ m0<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : f =ᶠ[ae μ] g<GOAL>f =ᶠ[ae (μ.trim hm)] g
<VAR>α✝¹ : Type u_1<VAR>G : Type u_2<VAR>α✝ : Type u_3<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : Div G<VAR>m✝ : MeasurableSpace α✝<VAR>f✝ g✝ : α✝ → G<VAR>μ✝ : Measure α✝<VAR>α : Type u_4<VAR>E : Type u_5<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : AddGroup E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : MeasurableSub₂ E<VAR>hm : m ≤ m0<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : f =ᶠ[ae μ] g<GOAL>MeasurableSet {a | ¬f a = g a}
<VAR>r : ℝ<VAR>n : ℕ<GOAL>↑n < r.toNNReal ↔ ↑n < r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁵ : Semifield K<VAR>inst✝⁴ : Semifield K₂<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>a : K<VAR>h : a ≠ 0<GOAL>range (a • f) = range f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>Dense (closure s) ↔ Dense s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hs : s.totalVariation i = 0<GOAL>↑s i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0<GOAL>↑s i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i : Set α<VAR>hs : s.toJordanDecomposition.posPart i = 0 ∧ s.toJordanDecomposition.negPart i = 0<GOAL>((if MeasurableSet i then (s.toJordanDecomposition.posPart i).toReal else 0) - if MeasurableSet i then (s.toJordanDecomposition.negPart i).toReal else 0) = 0
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>h : a * b ∣ c<GOAL>b ∣ c / a
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>b c : R<VAR>h : 0 * b ∣ c<GOAL>b ∣ c / 0
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>h : a * b ∣ c<VAR>ha : a ≠ 0<GOAL>b ∣ c / a
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<VAR>ha : a ≠ 0<VAR>d : R<GOAL>a * b * d / a = b * d
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>n a a' : ℤ<VAR>ha' : n + a = a'<VAR>K : CochainComplex C ℤ<GOAL>((homologyFunctor C (up ℤ) 0).shiftIso n a a' ha').hom.app ((quotient C (up ℤ)).obj K) = (homologyFunctor C (up ℤ) a).map (((quotient C (up ℤ)).commShiftIso n).inv.app K) ≫ (homologyFunctorFactors C (up ℤ) a).hom.app ((shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K) ≫ ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso n a a' ha').hom.app K ≫ (homologyFunctorFactors C (up ℤ) a').inv.app K
<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>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : ∀ (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>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : ∀ (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>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : ∀ (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>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : P<VAR>ps : Set P<VAR>h : p ∈ affineSpan k ps<GOAL>vectorSpan k (insert p ps) = vectorSpan k ps
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<GOAL>s.mongePoint = (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<GOAL>(affineCombination ℝ univ s.pointsWithCircumcenter) ((↑(n + 2 + 1) / ↑(n + 2 - 1)) • (centroidWeightsWithCircumcenter univ - circumcenterWeightsWithCircumcenter (n + 2)) + circumcenterWeightsWithCircumcenter (n + 2)) = (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i : PointsWithCircumcenterIndex (n + 2)<GOAL>((↑(n + 2 + 1) / ↑(n + 2 - 1)) • (centroidWeightsWithCircumcenter univ - circumcenterWeightsWithCircumcenter (n + 2)) + circumcenterWeightsWithCircumcenter (n + 2)) i = mongePointWeightsWithCircumcenter n i
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i : PointsWithCircumcenterIndex (n + 2)<GOAL>↑(n + 2 + 1) / ↑(n + 2 - 1) * (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) + circumcenterWeightsWithCircumcenter (n + 2) i = mongePointWeightsWithCircumcenter n i
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i : PointsWithCircumcenterIndex (n + 2)<VAR>hn1 : ↑n + 1 ≠ 0<GOAL>↑(n + 2 + 1) / ↑(n + 2 - 1) * (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) + circumcenterWeightsWithCircumcenter (n + 2) i = mongePointWeightsWithCircumcenter n i
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>hn1 : ↑n + 1 ≠ 0<VAR>a✝ : Fin (n + 2 + 1)<GOAL>↑(n + 2 + 1) / ↑(n + 1) * ((if a✝ ∈ univ then (↑univ.card)⁻¹ else 0) - 0) + 0 = (↑(n + 1))⁻¹
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>hn1 : ↑n + 1 ≠ 0<GOAL>↑(n + 2 + 1) / ↑(n + 1) * (0 - 1) + 1 = -2 / ↑(n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>T : Set (TopologicalSpace α)<VAR>t₂ : TopologicalSpace β<GOAL>Continuous f ↔ ∀ t ∈ T, Continuous f
<VAR>M : Type u_1<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : Pow M ℕ<VAR>inst✝ : NatPowAssoc M<VAR>k m n : ℕ<VAR>x : M<GOAL>x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : ⊥ = ⊤<GOAL>IsCyclotomicExtension ∅ A B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : ⊥ = ⊤<VAR>x : B<VAR>hx : x ∈ ⊤<GOAL>x ∈ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1}
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : G.LocallyFinite<VAR>n : ℕ<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p ∈ {p | p.length = n}.toFinset ↔ p ∈ G.finsetWalkLength n u v
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>φ P.c = φ P.a * (x * y + x * z + y * z)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : IsClosed s<VAR>hs : s.Nonempty<GOAL>x ∉ s ↔ 0 < infDist x s
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<GOAL>∃ ι c r r', (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r => 0 < r ∧ r < R x) fun r => ball x r<GOAL>∃ ι c r r', (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)
<VAR>α : Type u<VAR>ι✝ : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c✝ : ι✝ → α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r => 0 < r ∧ r < R x) fun r => ball x r<VAR>ι : Type u<VAR>c : ι → α<VAR>r' : ι → ℝ<VAR>hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)<VAR>hsub' : s ⊆ ⋃ a, ball (c a) (r' a)<VAR>hfin : LocallyFinite fun a => ball (c a) (r' a)<GOAL>∃ ι c r r', (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)
<VAR>α : Type u<VAR>ι✝ : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c✝ : ι✝ → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r => 0 < r ∧ r < R x) fun r => ball x r<VAR>ι : Type u<VAR>c : ι → α<VAR>r' : ι → ℝ<VAR>hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)<VAR>hsub' : s ⊆ ⋃ a, ball (c a) (r' a)<VAR>hfin : LocallyFinite fun a => ball (c a) (r' a)<VAR>r : ι → ℝ<VAR>hsub : s ⊆ ⋃ i, ball (c i) (r i)<VAR>hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)<GOAL>∃ ι c r r', (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>finInsepDegree F F = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>L S : TopologicalSpace α<VAR>inst✝¹ : IsLawson α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsClosed s ↔ DirSupClosed s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>L S : TopologicalSpace α<VAR>inst✝¹ : IsLawson α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsLowerSet s ∧ DirSupClosed s ↔ DirSupClosed s
<VAR>a b : ℕ+<GOAL>Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<GOAL>↑(d ⟨p, ⋯⟩) ∈ normalizedFactors n
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<GOAL>Prime ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>this : Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) = ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)<GOAL>Prime ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>this : Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) = ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)<GOAL>Prime ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>this✝ : Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) = ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)<VAR>this : DecidableEq (Associates M) := Classical.decEq (Associates M)<GOAL>Prime ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>this✝ : Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) = ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)<VAR>this : DecidableEq (Associates M) := Classical.decEq (Associates M)<GOAL>associatesEquivOfUniqueUnits.symm p ∈ normalizedFactors (Associates.mk m)
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero N<VAR>inst✝³ : Unique Mˣ<VAR>inst✝² : Unique Nˣ<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>this✝ : Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits (associatesEquivOfUniqueUnits.symm p), ⋯⟩) = ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) ⟨associatesEquivOfUniqueUnits.symm p, ⋯⟩)<VAR>this : DecidableEq (Associates M) := Classical.decEq (Associates M)<VAR>q : Associates M<VAR>hq : q ∈ normalizedFactors (Associates.mk m)<VAR>hq' : Associated (Associates.mk p) q<GOAL>associatesEquivOfUniqueUnits.symm p ∈ normalizedFactors (Associates.mk m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>o₁ o₂ : Option α<GOAL>o₁.toList ~ o₂.toList ↔ o₁ = o₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>o₁ o₂ : Option α<VAR>p : o₁.toList ~ o₂.toList<GOAL>o₁ = o₂