ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>h : J ⊔ K = ⊤<GOAL>I * K ⊔ J = I ⊔ J
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a✝ b a : α<VAR>f : ι → α<GOAL>a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
<VAR>x : ℂ<GOAL>(x ^ 2⁻¹).re = √((abs x + x.re) / 2)
<VAR>x : ℂ<GOAL>0 ≤ abs x
<VAR>x : ℂ<GOAL>-π ≤ x.arg
<VAR>x : ℂ<GOAL>x.arg ≤ π
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : Rˣ<GOAL>v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : Rˣ<GOAL>v.valuation (↑(algebraMap R K) ↑x) ≤ ↑1 ∧ ¬v.valuation (↑(algebraMap R K) ↑x) < ↑1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>Odd (cs.length 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>t : W<VAR>ht : cs.IsReflection t<GOAL>cs.lengthParity t = Multiplicative.ofAdd 1
<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 : W<VAR>i : B<GOAL>cs.lengthParity (w * cs.simple i * w⁻¹) = Multiplicative.ofAdd 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<GOAL>equalizerSieve a b ∈ K.sieves (Opposite.unop X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<GOAL>∀ ⦃Y : D⦄ ⦃f : Y ⟶ Opposite.unop X⦄, (Sieve.coverByImage H (Opposite.unop X)).arrows f → Sieve.pullback f (equalizerSieve a b) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<VAR>Y : D<VAR>g : Y ⟶ Opposite.unop X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ Opposite.unop X<VAR>fac : lift ≫ map = g<GOAL>Sieve.pullback g (equalizerSieve a b) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<VAR>Y : D<VAR>g : Y ⟶ Opposite.unop X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ Opposite.unop X<VAR>fac : lift ≫ map = g<GOAL>Sieve.pullback lift (Sieve.pullback map (equalizerSieve a b)) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<VAR>Y : D<VAR>g : Y ⟶ Opposite.unop X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ Opposite.unop X<VAR>fac : lift ≫ map = g<GOAL>Sieve.pullback map (equalizerSieve a b) ∈ K.sieves (H.obj Z)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<VAR>Y : D<VAR>g : Y ⟶ Opposite.unop X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ Opposite.unop X<VAR>fac : lift ≫ map = g<GOAL>Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback map (equalizerSieve a b))) ∈ K.sieves (H.obj Z)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<VAR>Y : D<VAR>g : Y ⟶ Opposite.unop X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ Opposite.unop X<VAR>fac : lift ≫ map = g<GOAL>equalizerSieve ((forget A).map (F.map map.op) a) ((forget A).map (F.map map.op) b) ≤ Sieve.functorPullback H (Sieve.pullback map (equalizerSieve a b))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_7, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallyInjective J (whiskerLeft H.op f)<VAR>X : Dᵒᵖ<VAR>a b : (forget A).obj (F.obj X)<VAR>h : (f.app X) a = (f.app X) b<VAR>Y : D<VAR>g : Y ⟶ Opposite.unop X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ Opposite.unop X<VAR>fac : lift ≫ map = g<GOAL>((whiskerLeft H.op f).app (Opposite.op Z)) ((forget A).map (F.map map.op) a) = ((whiskerLeft H.op f).app (Opposite.op Z)) ((forget A).map (F.map map.op) b)
<VAR>R : Type u<VAR>inst✝¹¹ : Ring R<VAR>ι : Type v<VAR>inst✝¹⁰ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁹ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁸ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁷ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>g✝ : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x<VAR>G' : ι → Type v'<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G' i)<VAR>inst✝³ : (i : ι) → Module R (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j<VAR>G'' : ι → Type v''<VAR>inst✝² : (i : ι) → AddCommGroup (G'' i)<VAR>inst✝¹ : (i : ι) → Module R (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃ₗ[R] G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)<VAR>i✝ : ι<VAR>g : G' i✝<VAR>i j : ι<VAR>h : i ≤ j<GOAL>↑(e j).symm ∘ₗ f' i j h = f i j h ∘ₗ ↑(e i).symm
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f₁ f₂ : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>hl : f₁ =ᶠ[l₁] f₂<GOAL>Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t : Set α<VAR>f g : α → M<VAR>a : α<VAR>s : Set M<GOAL>t.mulIndicator 1 ⁻¹' s ∈ {univ, ∅}
<VAR>g : SL(2, ℤ)<VAR>z✝ z : ℍ<GOAL>∃ g, g • z ∈ 𝒟
<VAR>g : SL(2, ℤ)<VAR>z✝ z : ℍ<VAR>g₀ : SL(2, ℤ)<VAR>hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im<GOAL>∃ g, g • z ∈ 𝒟
<VAR>g✝ : SL(2, ℤ)<VAR>z✝ z : ℍ<VAR>g₀ : SL(2, ℤ)<VAR>hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im<VAR>g : SL(2, ℤ)<VAR>hg : ↑g 1 = ↑g₀ 1<VAR>hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|<GOAL>∃ g, g • z ∈ 𝒟
<VAR>g✝ : SL(2, ℤ)<VAR>z✝ z : ℍ<VAR>g₀ : SL(2, ℤ)<VAR>hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im<VAR>g : SL(2, ℤ)<VAR>hg : ↑g 1 = ↑g₀ 1<VAR>hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|<GOAL>g • z ∈ 𝒟
<VAR>g✝ : SL(2, ℤ)<VAR>z✝ z : ℍ<VAR>g₀ : SL(2, ℤ)<VAR>hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im<VAR>g : SL(2, ℤ)<VAR>hg : ↑g 1 = ↑g₀ 1<VAR>hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|<VAR>hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im<GOAL>g • z ∈ 𝒟
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z✝ : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>ta1 ta2 : TopologicalSpace X<VAR>tb1 tb2 : TopologicalSpace Y<VAR>tc1 : TopologicalSpace Z<VAR>h : Continuous fun p => f p.1 p.2<GOAL>Continuous fun p => f p.1 p.2
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z✝ : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>ta1 ta2 : TopologicalSpace X<VAR>tb1 tb2 : TopologicalSpace Y<VAR>tc1 : TopologicalSpace Z<VAR>h : Continuous fun p => f p.1 p.2<VAR>ha : Continuous id<GOAL>Continuous fun p => f p.1 p.2
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z✝ : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>ta1 ta2 : TopologicalSpace X<VAR>tb1 tb2 : TopologicalSpace Y<VAR>tc1 : TopologicalSpace Z<VAR>h : Continuous fun p => f p.1 p.2<VAR>ha : Continuous id<VAR>hb : Continuous id<GOAL>Continuous fun p => f p.1 p.2
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z✝ : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>ta1 ta2 : TopologicalSpace X<VAR>tb1 tb2 : TopologicalSpace Y<VAR>tc1 : TopologicalSpace Z<VAR>h : Continuous fun p => f p.1 p.2<VAR>ha : Continuous id<VAR>hb : Continuous id<VAR>h_continuous_id : Continuous fun p => (id p.1, id p.2)<GOAL>Continuous fun p => f p.1 p.2
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>g : α → α<VAR>a : α<GOAL>corec f g a = f a :: corec f g (g a)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>g : α → α<VAR>a : α<GOAL>f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate' (n % l.length) = (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length))
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n : ℕ<VAR>a : α<VAR>hf : Injective f<GOAL>f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b c d : α<VAR>hb : IsUnit b<VAR>hd : IsUnit d<GOAL>a / b = c / d ↔ a * d = c * b
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : BEq α<VAR>inst✝² : LawfulBEq α<VAR>inst✝¹ : BEq β<VAR>inst✝ : LawfulBEq β<VAR>f : α → β<VAR>I : Injective f<VAR>a b : α<GOAL>(f a == f b) = (a == b)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f : SimpleFunc (ι → ℝ) E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<GOAL>HasIntegral I l (↑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>y : E<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<GOAL>HasIntegral I l (↑(piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0))) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) (piecewise s hs (const (ι → ℝ) y) (const (ι → ℝ) 0)))
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>f g : SimpleFunc (ι → ℝ) E<VAR>a✝ : Disjoint (Function.support ↑f) (Function.support ↑g)<VAR>hfi : HasIntegral I l (↑f) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) f)<VAR>hgi : HasIntegral I l (↑g) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) g)<GOAL>HasIntegral I l (↑(f + g)) μ.toBoxAdditive.toSMul (integral (μ.restrict ↑I) (f + g))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.3839, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<GOAL>A.EqId ↔ (unop A.fst).len = (unop Δ).len
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.3839, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<GOAL>A.fst = Δ ↔ (unop A.fst).len = (unop Δ).len
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : Cofork f g<GOAL>f ≫ t.π = g ≫ t.π
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ 𝓒 u v s<VAR>ha : a ∉ s<GOAL>u ≤ a
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a<VAR>ha : a ∉ s<GOAL>u ≤ a
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>v : E<VAR>μ : Eigenvalues T<GOAL>hT.diagonalization (T v) μ = ↑T μ • hT.diagonalization v μ
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>v : E<VAR>μ : Eigenvalues T<GOAL>∀ (w : PiLp 2 fun μ => ↥(eigenspace T (↑T μ))), T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T μ • w μ
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>v : E<VAR>μ : Eigenvalues T<VAR>w : PiLp 2 fun μ => ↥(eigenspace T (↑T μ))<GOAL>T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T μ • w μ
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>v : E<VAR>μ : Eigenvalues T<VAR>w : PiLp 2 fun μ => ↥(eigenspace T (↑T μ))<VAR>hwT : ∀ (μ : Eigenvalues T), T ↑(w μ) = ↑T μ • ↑(w μ)<GOAL>T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => ↑T μ • w μ
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : CU P<VAR>x : X<VAR>h : x ∈ c.C<GOAL>c.lim x = 0
<VAR>R : Type u<VAR>L : Type v<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>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N : Submodule R M<VAR>h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier<GOAL>{ toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f₁ i).NeBot<VAR>h : pi f₁ = pi f₂<GOAL>f₁ = f₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f₁ i).NeBot<VAR>h : pi f₁ = pi f₂<VAR>hle : f₁ ≤ f₂<GOAL>f₁ = f₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f₁ i).NeBot<VAR>h : pi f₁ = pi f₂<VAR>hle : f₁ ≤ f₂<VAR>this : ∀ (i : ι), (f₂ i).NeBot<GOAL>f₁ = f₂
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = i₁ ≫ f'<VAR>e₂ : g = i₂ ≫ g'<GOAL>P (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = i₁ ≫ f'<VAR>e₂ : g = i₂ ≫ g'<VAR>this : P.RespectsIso<GOAL>P (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = i₁ ≫ f'<VAR>e₂ : g = i₂ ≫ g'<VAR>this✝ : P.RespectsIso<VAR>this : pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ = ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫ (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left<GOAL>P (pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = i₁ ≫ f'<VAR>e₂ : g = i₂ ≫ g'<VAR>this✝ : P.RespectsIso<VAR>this : pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ = ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫ (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left<GOAL>P (((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫ (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = i₁ ≫ f'<VAR>e₂ : g = i₂ ≫ g'<VAR>this✝ : P.RespectsIso<VAR>this : pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ = ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫ (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left<GOAL>P ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.IsStableUnderComposition<VAR>S X X' Y Y' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S<VAR>g' : Y' ⟶ S<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>h₁ : P i₁<VAR>h₂ : P i₂<VAR>e₁ : f = i₁ ≫ f'<VAR>e₂ : g = i₂ ≫ g'<VAR>this✝ : P.RespectsIso<VAR>this : pullback.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ = ((pullbackSymmetry (Over.mk f).hom (Over.mk g).hom).hom ≫ ((Over.pullback (Over.mk f).hom).map (Over.homMk i₂ ⋯)).left) ≫ (pullbackSymmetry (Over.mk g').hom (Over.mk f).hom).hom ≫ ((Over.pullback g').map (Over.homMk i₁ ⋯)).left<GOAL>P ((Over.pullback g').map (Over.homMk i₁ ⋯)).left
<VAR>a b c : Ordinal.{u}<GOAL>1 ♯ a = succ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>t : f.NeBot<VAR>p : Prop<GOAL>(∀ᶠ (x : α) in f, p) ↔ p
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : 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>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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : 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>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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>(∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆) ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q✝ : QuadraticMap R M N<VAR>Q : QuadraticMap R M R<VAR>x y : M<GOAL>(RingHom.id R) ((((associatedHom S) Q) x) y) = (((associatedHom S) Q) y) x
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>a₁ a₂ a₃ : (i : ι) → A i<VAR>ha : SemiconjBy a₁ a₂ a₃<GOAL>SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)