ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p'✝ : ι' → Prop<VAR>s'✝ : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>p' : ι → Prop<VAR>s' : ι → Set α<VAR>hp : ∀ (i : ι), p i ↔ p' i<VAR>hs : ∀ (i : ι), p i → s i = s' i<VAR>t : Set α<GOAL>(∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ s' i ⊆ t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>β : Type u_1<VAR>X Y : GradedObject β C<VAR>f g : X ⟶ Y<VAR>h : ∀ (x : β), f x = g x<GOAL>f = g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>β : Type u_1<VAR>X Y : GradedObject β C<VAR>f g : X ⟶ Y<VAR>h : ∀ (x : β), f x = g x<VAR>x✝ : β<GOAL>f x✝ = g x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<GOAL>(f.subtypePerm ⋯).IsCycle
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a✝ b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<VAR>a : α<VAR>ha : a ∈ s<GOAL>(f.subtypePerm ⋯).IsCycle
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝ : Field R<VAR>A : Matrix n n R<VAR>hAps : Splits (RingHom.id R) A.charpoly<GOAL>A.trace = A.charpoly.roots.sum
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝ : Field R<VAR>A : Matrix n n R<VAR>hAps : Splits (RingHom.id R) A.charpoly<VAR>h : IsEmpty n<GOAL>A.trace = A.charpoly.roots.sum
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝ : Field R<VAR>A : Matrix n n R<VAR>hAps : Splits (RingHom.id R) A.charpoly<VAR>h✝ : Nonempty n<GOAL>A.trace = A.charpoly.roots.sum
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>p : (x : G) → x ∈ closure k → Prop<VAR>mem : ∀ (x : G) (h : x ∈ k), p x ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x : G) (hx : x ∈ closure k) (y : G) (hy : y ∈ closure k), p x hx → p y hy → p (x * y) ⋯<VAR>inv : ∀ (x : G) (hx : x ∈ closure k), p x hx → p x⁻¹ ⋯<VAR>x : G<VAR>hx : x ∈ closure k<GOAL>p x hx
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>p : (x : G) → x ∈ closure k → Prop<VAR>mem : ∀ (x : G) (h : x ∈ k), p x ⋯<VAR>one : p 1 ⋯<VAR>mul : ∀ (x : G) (hx : x ∈ closure k) (y : G) (hy : y ∈ closure k), p x hx → p y hy → p (x * y) ⋯<VAR>inv : ∀ (x : G) (hx : x ∈ closure k), p x hx → p x⁻¹ ⋯<VAR>x : G<VAR>hx : x ∈ closure k<GOAL>∃ (x_1 : x ∈ closure k), p x x_1
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>oddKernel (-a) x = -oddKernel a x
<VAR>x a' : ℝ<GOAL>oddKernel (-↑a') x = -oddKernel (↑a') x
<VAR>b✝ : Game<VAR>b : PGame<VAR>c✝ : Game<VAR>c : PGame<VAR>h : Quot.mk Setoid.r b ⧏ Quot.mk Setoid.r c<VAR>a✝ : Game<VAR>a : PGame<GOAL>Quot.mk Setoid.r b + Quot.mk Setoid.r a ⧏ Quot.mk Setoid.r c + Quot.mk Setoid.r a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y X : C<VAR>s : Cone (Functor.empty C)<VAR>P : IsLimit s<VAR>t : BinaryFan s.pt X<VAR>Q : IsLimit t<GOAL>t.snd ≫ Q.lift (mk (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }) (𝟙 { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }.pt)) = 𝟙 t.pt
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y X : C<VAR>s : Cone (Functor.empty C)<VAR>P : IsLimit s<VAR>t : BinaryFan s.pt X<VAR>Q : IsLimit t<GOAL>∀ (j : Discrete WalkingPair), (t.snd ≫ Q.lift (mk (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }) (𝟙 { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }.pt))) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝² : SigmaFinite ν₁<VAR>inst✝¹ : SigmaFinite ν₂<VAR>inst✝ : SigmaFinite μ<VAR>h : ν₂ ⟂ₘ μ<GOAL>(ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝² : SigmaFinite ν₁<VAR>inst✝¹ : SigmaFinite ν₂<VAR>inst✝ : SigmaFinite μ<VAR>h : ν₂ ⟂ₘ μ<VAR>x : α<VAR>hx_add : (ν₁ + ν₂).rnDeriv μ x = (ν₁.rnDeriv μ + ν₂.rnDeriv μ) x<VAR>hx_zero : ν₂.rnDeriv μ x = 0 x<GOAL>(ν₁ + ν₂).rnDeriv μ x = ν₁.rnDeriv μ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b✝ c✝ a b c : G<GOAL>a * b / c = a * (b / c)
<VAR>x y z : ℂ<GOAL>sin z = sin ↑z.re * cosh ↑z.im + cos ↑z.re * sinh ↑z.im * I
<VAR>x y z : ℂ<GOAL>z = ↑z.re + ↑z.im * I
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<GOAL>(∃ᶠ (x : α) in f, True) ↔ f.NeBot
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<VAR>a : ℝ<GOAL>(interior (Iic a)).Nonempty
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Wbtw R x y z<GOAL>Wbtw R w y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>w x y z : P<VAR>h₁ : Wbtw R z x w<VAR>h₂ : Wbtw R z y x<GOAL>Wbtw R z y w
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {5} ℚ K<GOAL>IsPrincipalIdealRing (𝓞 K)
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {5} ℚ K<GOAL>↑|discr K| < (2 * (π / 4) ^ NrComplexPlaces K * (↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K / ↑(FiniteDimensional.finrank ℚ K)!)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {5} ℚ K<GOAL>↑|(-1) ^ ((↑5 - 1) / 2) * ↑↑5 ^ (↑5 - 2)| < (2 * (π / 4) ^ ((↑5 - 1) / 2) * (↑(↑5 - 1) ^ (↑5 - 1) / ↑(↑5 - 1)!)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {5} ℚ K<GOAL>125 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {5} ℚ K<GOAL>(2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2
<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {5} ℚ K<GOAL>3 < π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<GOAL>Integrable (fun a => ‖f a‖) μ ↔ Integrable f μ
<VAR>Ω : Type u_1<VAR>inst✝⁴ : TopologicalSpace Ω<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝¹ : L.IsCountablyGenerated<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>f : Ω → ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>Tendsto (fun i => ∫⁻ (ω : Ω), ↑((fs i) ω) ∂μ) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂μ))
<VAR>Ω : Type u_1<VAR>inst✝⁴ : TopologicalSpace Ω<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝¹ : L.IsCountablyGenerated<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>f : Ω → ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, ↑((fs n) a) ≤ (fun x => ↑c) a
<VAR>Ω : Type u_1<VAR>inst✝⁴ : TopologicalSpace Ω<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝¹ : L.IsCountablyGenerated<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>fs : ι → Ω →ᵇ ℝ≥0<VAR>c : ℝ≥0<VAR>fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i) ω ≤ c<VAR>f : Ω → ℝ≥0<VAR>fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => (fs i) ω) L (𝓝 (f ω))<GOAL>∀ᵐ (a : Ω) ∂μ, Tendsto (fun n => ↑((fs n) a)) L (𝓝 ↑(f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>hwv : w =o[l] v<GOAL>u - w ~[l] v
<VAR>x y : ℝ<GOAL>abs { re := x, im := y } ≤ √2 * max |{ re := x, im := y }.re| |{ re := x, im := y }.im|
<VAR>x y : ℝ<GOAL>√(x ^ 2 + y ^ 2) ≤ √2 * max |x| |y|
<VAR>n : ℕ<GOAL>2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π
<VAR>n : ℕ<VAR>this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π<GOAL>2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π
<VAR>n : ℕ<VAR>this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π<GOAL>2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) = √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2)
<VAR>n : ℕ<VAR>this : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π<GOAL>2 ≠ 0
<VAR>a b q q' : ℤ<VAR>h : IsInt (a / -b) q<VAR>hq : -q = q'<GOAL>a / b = ↑q'
<VAR>x : ℝ<GOAL>sign (-↑x) = -sign ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>c * a / (c * b) = a / b
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>inst✝¹ : HasContDiffBump G<VAR>inst✝ : CompleteSpace E'<VAR>φ : ContDiffBump 0<VAR>x₀✝ x₀ : G<VAR>hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀<GOAL>(↑φ ⋆[lsmul ℝ ℝ, μ] g) x₀ = integral μ ↑φ • g x₀
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝⁴ : HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>inst✝³ : HasPullback i i<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback (f ≫ i) (g ≫ i)<VAR>inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(pullbackDiagonalMapIdIso f g i).inv ≫ fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) = fst f g ≫ f
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝⁴ : HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>inst✝³ : HasPullback i i<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback (f ≫ i) (g ≫ i)<VAR>inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ fst i i = (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g ≫ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hg : EqOn f g (EMetric.ball x r)<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<GOAL>HasSum (fun n => (p n) fun x => y) (g (x + y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hg : EqOn f g (EMetric.ball x r)<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<GOAL>g (x + y) = f (x + y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hg : EqOn f g (EMetric.ball x r)<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 r<GOAL>x + y ∈ EMetric.ball x r
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>x✝¹ : NonAssocSemiring α<VAR>x✝ : NonAssocSemiring β<VAR>f : α →+* β<VAR>x y : α<VAR>inst✝ : Nontrivial β<VAR>h : 1 = 0<GOAL>f 1 = 0
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₁' p₂ p₃ p₃' : P<VAR>h₁ : Sbtw ℝ p₁ p₂ p₁'<VAR>h₃ : Sbtw ℝ p₃ p₂ p₃'<GOAL>∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : StrongOplaxNatTrans F G<VAR>θ : StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : G.obj a ⟶ a'<GOAL>(η.naturality (𝟙 a)).hom ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ G.mapId a ▷ f = F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s t : Multiset α<GOAL>Rel (flip fun x x_1 => x = x_1) s t ↔ s = t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>c : E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>Memℒp (fun x => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>c : E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>Memℒp (fun x => c) p μ ↔ eLpNorm (fun x => c) p μ < ⊤
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>f g : M₁ →ₗ[R] M₁<GOAL>(toMatrixAlgEquiv v₁) (f ∘ₗ g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<GOAL>s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<GOAL>⟪T x, y⟫_𝕜 = (⟪T (x + y), x + y⟫_𝕜 - ⟪T (x - y), x - y⟫_𝕜 - I * ⟪T (x + I • y), x + I • y⟫_𝕜 + I * ⟪T (x - I • y), x - I • y⟫_𝕜) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<VAR>h : I = 0<GOAL>⟪T x, y⟫_𝕜 = (⟪T (x + y), x + y⟫_𝕜 - ⟪T (x - y), x - y⟫_𝕜 - I * ⟪T (x + I • y), x + I • y⟫_𝕜 + I * ⟪T (x - I • y), x - I • y⟫_𝕜) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<VAR>h : I * I = -1<GOAL>⟪T x, y⟫_𝕜 = (⟪T (x + y), x + y⟫_𝕜 - ⟪T (x - y), x - y⟫_𝕜 - I * ⟪T (x + I • y), x + I • y⟫_𝕜 + I * ⟪T (x - I • y), x - I • y⟫_𝕜) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<GOAL>x ∈ [y-[𝕜]z] ↔ SameRay 𝕜 (x - y) (z - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : SameRay 𝕜 (x - y) (z - x)<GOAL>x ∈ [y-[𝕜]z]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : SameRay 𝕜 (x - y) (z - x)<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hxy : x - y = a • (x - y + (z - x))<VAR>hzx : z - x = b • (x - y + (z - x))<GOAL>x ∈ [y-[𝕜]z]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : SameRay 𝕜 (x - y) (z - x)<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hxy : x - y = a • (z - y)<VAR>hzx : z - x = b • (z - y)<GOAL>x ∈ [y-[𝕜]z]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : SameRay 𝕜 (x - y) (z - x)<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hxy : x - y = a • (z - y)<VAR>hzx : z - x = b • (z - y)<GOAL>0 ∈ [-x + y-[𝕜]-x + z]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x y z : E<VAR>h : SameRay 𝕜 (x - y) (z - x)<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hxy : x - y = a • (z - y)<VAR>hzx : z - x = b • (z - y)<GOAL>b • (-x + y) + a • (-x + z) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v U : Set α<GOAL>ConnectedComponents.mk ⁻¹' (ConnectedComponents.mk '' U) = ⋃ x ∈ U, connectedComponent x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>ι : Sort u_4<VAR>p : ι → Submonoid M<GOAL>⨆ i, p i = closure (⋃ i, ↑(p i))
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>f : G →* N<VAR>h : Surjective ⇑f<GOAL>map f ⊤ = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>f : G →* N<VAR>h : Surjective ⇑f<GOAL>⊤ ≤ map f ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>f : G →* N<VAR>h : Surjective ⇑f<VAR>x : N<VAR>a✝ : x ∈ ⊤<VAR>y : G<VAR>hy : f y = x<GOAL>x ∈ map f ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢￢(a \ b) = ￢￢a \ ￢￢b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢￢(a \ b) ≤ ￢￢a \ ￢￢b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢￢a \ ￢￢b ≤ ￢￢(a \ b)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x₁ x₂ L : R<GOAL>f L ^ 2 + (map W f).toAffine.a₁ * f L - (map W f).toAffine.a₂ - f x₁ - f x₂ = f (L ^ 2 + W.a₁ * L - W.a₂ - x₁ - x₂)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>f : MvPolynomial σ R ⧸ Ideal.map C I<GOAL>eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) f) = f
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>f : MvPolynomial σ R<GOAL>eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) f)) = (Ideal.Quotient.mk (Ideal.map C I)) f
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>f : MvPolynomial σ R<GOAL>∀ (a : R), eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) (C a))) = (Ideal.Quotient.mk (Ideal.map C I)) (C a)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>f : MvPolynomial σ R<GOAL>∀ (p q : MvPolynomial σ R), eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) p)) = (Ideal.Quotient.mk (Ideal.map C I)) p → eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) q)) = (Ideal.Quotient.mk (Ideal.map C I)) q → eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) = (Ideal.Quotient.mk (Ideal.map C I)) (p + q)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>f : MvPolynomial σ R<GOAL>∀ (p : MvPolynomial σ R) (n : σ), eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) p)) = (Ideal.Quotient.mk (Ideal.map C I)) p → eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) (fun i => (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯) ((Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) = (Ideal.Quotient.mk (Ideal.map C I)) (p * X n)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π