ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy✝ : y = 0 → x = 0 ∨ z = 0<VAR>hx : x ≠ 0<VAR>hz : z ≠ 0<VAR>hy : y ≠ 0<VAR>r₁ r₂ : R<VAR>hr₁ : 0 < r₁<VAR>hr₂ : 0 < r₂<VAR>h₁ : r₁ • x = r₂ • y<VAR>r₃ r₄ : R<VAR>hr₃ : 0 < r₃<VAR>hr₄ : 0 < r₄<VAR>h₂ : r₃ • y = r₄ • z<GOAL>(r₃ * r₁) • x = (r₂ * r₄) • z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t s : Set α<GOAL>μ (toMeasurable μ s) = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t s : Set α<GOAL>μ (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose else if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose else ⋯.choose) = μ s
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>((ofSet s hs).trans e).source = (e.restr s).source
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Iio b).card = ↑b
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x : M ⊗[R] N<VAR>h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n<GOAL>∃ m n, x = m ⊗ₜ[R] n
<VAR>f g : ℕ → ℂ<VAR>s a b : ℂ<VAR>hf : LSeriesHasSum f s a<VAR>hg : LSeriesHasSum g s b<GOAL>LSeriesHasSum (f - g) s (a - b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p q : Submodule R M<GOAL>Nontrivial ↥p ↔ p ≠ ⊥
<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>y z : E<VAR>hz : z ∈ EMetric.ball 0 r<GOAL>HasSum (fun n => (p n) fun x => z) (f (x + y + z - 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>y z : E<VAR>hz : z ∈ EMetric.ball 0 r<GOAL>x + y + z - y = x + z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsIntegralClosure A R B<VAR>x y : B<VAR>hx : IsIntegral R x<VAR>hy : IsIntegral R y<GOAL>(algebraMap A B) (mk' A (x * y) ⋯) = (algebraMap A B) (mk' A x hx * mk' A y hy)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>evariance X μ < ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<VAR>this : eLpNorm (X - fun x => ∫ (x : Ω), X x ∂μ) 2 μ ^ 2 < ⊤<GOAL>evariance X μ < ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<VAR>this : ((∫⁻ (x : Ω), ↑‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖₊ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ⊤<GOAL>evariance X μ < ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<VAR>this : ((∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ) ^ 2⁻¹) ^ 2 < ⊤<GOAL>evariance X μ < ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<VAR>this : ∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ < ⊤<GOAL>evariance X μ < ⊤
<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>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : CompactSpace α<VAR>inst✝³ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = Lp.boundedContinuousFunction E p μ
<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>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : CompactSpace α<VAR>inst✝³ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>↑(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = ↑(Lp.boundedContinuousFunction E p μ)
<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>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : CompactSpace α<VAR>inst✝³ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)<GOAL>↑(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = ↑(Lp.boundedContinuousFunction E p μ)
<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>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : CompactSpace α<VAR>inst✝³ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)<GOAL>↑(Lp.boundedContinuousFunction E p μ) = Set.range ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>x : α<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>x : α<VAR>s : Set α<VAR>s_compact : IsCompact s<VAR>hs : s ∈ 𝓝 x<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>x : α<VAR>s : Set α<VAR>s_compact : IsCompact s<VAR>hs : s ∈ 𝓝 x<VAR>r : ℝ<VAR>hr : closedBall x r ⊆ s<GOAL>IsCompact (closedBall x r)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ I J : Ideal A<VAR>HI : IsHomogeneous 𝒜 I<VAR>HJ : IsHomogeneous 𝒜 J<GOAL>IsHomogeneous 𝒜 (I * J)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ I J : Ideal A<VAR>HI : ∃ S, I = span (Subtype.val '' S)<VAR>HJ : ∃ S, J = span (Subtype.val '' S)<GOAL>∃ S, I * J = span (Subtype.val '' S)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)<GOAL>∃ S, span (Subtype.val '' s₁) * span (Subtype.val '' s₂) = span (Subtype.val '' S)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)<GOAL>∃ S, span (Subtype.val '' s₁ * Subtype.val '' s₂) = span (Subtype.val '' S)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Field K<VAR>R₁✝ : Type u_4<VAR>inst✝¹⁰ : CommRing R₁✝<VAR>inst✝⁹ : IsDomain R₁✝<VAR>inst✝⁸ : Algebra R₁✝ K<VAR>inst✝⁷ : IsFractionRing R₁✝ K<VAR>I✝ J : FractionalIdeal R₁✝⁰ K<VAR>K' : Type u_5<VAR>inst✝⁶ : Field K'<VAR>inst✝⁵ : Algebra R₁✝ K'<VAR>inst✝⁴ : IsFractionRing R₁✝ K'<VAR>R₁ : Type u_6<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsLocalization R₁⁰ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>I * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Field K<VAR>R₁✝ : Type u_4<VAR>inst✝¹⁰ : CommRing R₁✝<VAR>inst✝⁹ : IsDomain R₁✝<VAR>inst✝⁸ : Algebra R₁✝ K<VAR>inst✝⁷ : IsFractionRing R₁✝ K<VAR>I✝ J : FractionalIdeal R₁✝⁰ K<VAR>K' : Type u_5<VAR>inst✝⁶ : Field K'<VAR>inst✝⁵ : Algebra R₁✝ K'<VAR>inst✝⁴ : IsFractionRing R₁✝ K'<VAR>R₁ : Type u_6<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsLocalization R₁⁰ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>spanSingleton R₁⁰ (generator ↑I) * spanSingleton R₁⁰ (generator ↑I)⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Field K<VAR>R₁✝ : Type u_4<VAR>inst✝¹⁰ : CommRing R₁✝<VAR>inst✝⁹ : IsDomain R₁✝<VAR>inst✝⁸ : Algebra R₁✝ K<VAR>inst✝⁷ : IsFractionRing R₁✝ K<VAR>I✝ J : FractionalIdeal R₁✝⁰ K<VAR>K' : Type u_5<VAR>inst✝⁶ : Field K'<VAR>inst✝⁵ : Algebra R₁✝ K'<VAR>inst✝⁴ : IsFractionRing R₁✝ K'<VAR>R₁ : Type u_6<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsLocalization R₁⁰ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<GOAL>generator ↑I ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Field K<VAR>R₁✝ : Type u_4<VAR>inst✝¹⁰ : CommRing R₁✝<VAR>inst✝⁹ : IsDomain R₁✝<VAR>inst✝⁸ : Algebra R₁✝ K<VAR>inst✝⁷ : IsFractionRing R₁✝ K<VAR>I✝ J : FractionalIdeal R₁✝⁰ K<VAR>K' : Type u_5<VAR>inst✝⁶ : Field K'<VAR>inst✝⁵ : Algebra R₁✝ K'<VAR>inst✝⁴ : IsFractionRing R₁✝ K'<VAR>R₁ : Type u_6<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsLocalization R₁⁰ K<VAR>I : FractionalIdeal R₁⁰ K<VAR>inst✝ : (↑I).IsPrincipal<VAR>h : I ≠ 0<VAR>generator_I_eq_zero : generator ↑I = 0<GOAL>I = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>𝒜 : Finset (Finset α)<GOAL>∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂<VAR>e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃<VAR>x : CliffordAlgebra Q₁<GOAL>((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃)) x = (equivOfIsometry (e₁₂.trans e₂₃)) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>p : α → β → Prop<GOAL>(∀ a ∈ s, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ s, p a b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<GOAL>map (⇑(MeasurableEquiv.piCongrLeft (fun i => β i) e)) (Measure.pi fun i => μ (e i)) = Measure.pi μ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<GOAL>(map (⇑(MeasurableEquiv.piCongrLeft (fun i => β i) e)) (Measure.pi fun i => μ (e i))) (univ.pi s) = ∏ i : ι', (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<GOAL>(Measure.pi fun i => μ (e i)) (⇑e_meas ⁻¹' univ.pi s) = ∏ i : ι', (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<GOAL>(Measure.pi fun i => μ (e i)) (⇑e_meas ⁻¹' univ.pi s) = ∏ i : ι', (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<VAR>this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'<GOAL>(Measure.pi fun i => μ (e i)) (⇑e_meas ⁻¹' univ.pi s) = ∏ i : ι', (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<VAR>this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'<GOAL>∀ (i : ι'), i ∈ Finset.univ ↔ e.symm i ∈ Finset.univ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<VAR>this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'<GOAL>∀ i ∈ Finset.univ, (μ i) (s i) = (μ (e (e.symm i))) (s' (e.symm i))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<VAR>this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'<VAR>i : ι'<VAR>a✝ : i ∈ Finset.univ<GOAL>i = e (e.symm i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<VAR>this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'<VAR>i : ι'<VAR>a✝ : i ∈ Finset.univ<GOAL>HEq (fun x => ℝ≥0∞) fun x => ℝ≥0∞
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>hι' : Fintype ι'<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_4<VAR>inst✝¹ : (i : ι') → MeasurableSpace (β i)<VAR>μ : (i : ι') → Measure (β i)<VAR>inst✝ : ∀ (i : ι'), SigmaFinite (μ i)<VAR>e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e<VAR>s : (i : ι') → Set (β i)<VAR>x✝ : ∀ (i : ι'), MeasurableSet (s i)<VAR>s' : (i : ι) → Set (β (e i)) := fun i => s (e i)<VAR>this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'<VAR>i : ι'<VAR>a✝ : i ∈ Finset.univ<GOAL>HEq (s i) (s (e (e.symm i)))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<VAR>e : ¬LinearIndependent K ![(rootSystem H).root α, (rootSystem H).root β]<GOAL>(rootSystem H).root α = (rootSystem H).root β ∨ (rootSystem H).root α = -(rootSystem H).root β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<VAR>e : ∃ x, ¬x • (rootSystem H).root α ≠ (rootSystem H).root β<GOAL>(rootSystem H).root α = (rootSystem H).root β ∨ (rootSystem H).root α = -(rootSystem H).root β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<VAR>e : ∃ x, x • Weight.toLinear K (↥H) L ↑α = Weight.toLinear K (↥H) L ↑β<GOAL>(rootSystem H).root α = (rootSystem H).root β ∨ (rootSystem H).root α = -(rootSystem H).root β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<VAR>u : K<VAR>hu : u • Weight.toLinear K (↥H) L ↑α = Weight.toLinear K (↥H) L ↑β<GOAL>(rootSystem H).root α = (rootSystem H).root β ∨ (rootSystem H).root α = -(rootSystem H).root β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<VAR>u : K<VAR>hu : u • Weight.toLinear K (↥H) L ↑α = Weight.toLinear K (↥H) L ↑β<VAR>h : ↑β = -↑α<GOAL>(rootSystem H).root α = (rootSystem H).root β ∨ (rootSystem H).root α = -(rootSystem H).root β