ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>t : R[T;T⁻¹] := T 1<VAR>t_inv : R[T;T⁻¹] := T (-1)<VAR>p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det<VAR>q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det<VAR>ht : t_inv * t = 1<VAR>hp : toLaurentAlg M.charpoly = p<VAR>hq : toLaurentAlg M.charpolyRev = q<GOAL>M.charpoly.reverse = M.charpolyRev
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>t : R[T;T⁻¹] := T 1<VAR>t_inv : R[T;T⁻¹] := T (-1)<VAR>p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det<VAR>q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det<VAR>ht : t_inv * t = 1<VAR>hp : toLaurentAlg M.charpoly = p<VAR>hq : toLaurentAlg M.charpolyRev = q<GOAL>t_inv ^ Fintype.card n * p = invert q
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>t : R[T;T⁻¹] := T 1<VAR>t_inv : R[T;T⁻¹] := T (-1)<VAR>p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det<VAR>q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det<VAR>ht : t_inv * t = 1<VAR>hp : toLaurentAlg M.charpoly = p<VAR>hq : toLaurentAlg M.charpolyRev = q<GOAL>(1 - t_inv • M.map ⇑LaurentPolynomial.C).det = (invert.mapMatrix (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C)).det
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<GOAL>fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<GOAL>(1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<GOAL>∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<GOAL>∫ (x : ℝ) in Ioc a b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x ∂volume = ∫ (x : ℝ) in Ioc a b, (fourier (-n)) ↑x • f x ∂volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<VAR>x : ℝ<VAR>hx : x ∈ Ioc a b<GOAL>(fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>n : ℤ<VAR>hab : a < b<VAR>this : Fact (0 < b - a)<VAR>x : ℝ<VAR>hx : x ∈ Ioc a b<GOAL>x ∈ Ioc a (a + (b - a))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a b c : α<GOAL>￢a ≤ b ↔ Codisjoint a b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>h : r < infEdist x s<GOAL>Disjoint (closedBall x r) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>h : r < infEdist x s<GOAL>∀ ⦃a : α⦄, a ∈ closedBall x r → a ∉ s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>h : r < infEdist x s<VAR>y : α<VAR>hy : y ∈ closedBall x r<VAR>h'y : y ∈ s<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>h : r < infEdist x s<VAR>y : α<VAR>hy : y ∈ closedBall x r<VAR>h'y : y ∈ s<GOAL>infEdist x s < infEdist x s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f 0 p = f (p.coeff 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p : Option α → Prop<GOAL>(∃ x, x ≠ none ∧ p x) ↔ ∃ x, p (some x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝³ : DecidableEq I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝¹ : K.HasTotal c₁₂<VAR>inst✝ : L.HasTotal c₁₂<GOAL>map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝³ : DecidableEq I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝¹ : K.HasTotal c₁₂<VAR>inst✝ : L.HasTotal c₁₂<GOAL>(HomologicalComplex.forget C c₁₂).map (map (𝟙 K) c₁₂) = (HomologicalComplex.forget C c₁₂).map (𝟙 (K.total c₁₂))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>taylorWithinEval f (n + 1) s x₀ x = taylorWithinEval f n s x₀ x + (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>(PolynomialModule.eval x) (taylorWithin f n s x₀) + (PolynomialModule.eval (Polynomial.eval x (Polynomial.X - Polynomial.C x₀))) ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀)) = (PolynomialModule.eval x) (taylorWithin f n s x₀) + (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>(PolynomialModule.eval (Polynomial.eval x (Polynomial.X - Polynomial.C x₀))) ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀)) = (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>(x - x₀) ^ (n + 1) • taylorCoeffWithin f (n + 1) s x₀ = ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>n : ℕ<VAR>s : Set ℝ<VAR>x₀ x : ℝ<GOAL>(x - x₀) ^ (n + 1) • (↑(n + 1)!)⁻¹ • iteratedDerivWithin (n + 1) f s x₀ = ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddGroup α<VAR>f : α → E<VAR>inst✝ : One E<VAR>hf : HasCompactMulSupport f<GOAL>∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddGroup α<VAR>f : α → E<VAR>inst✝ : One E<VAR>hf : HasCompactMulSupport f<VAR>K : Set α<VAR>hK1 : IsCompact K<VAR>hK2 : ∀ x ∉ K, f x = 1<GOAL>∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddGroup α<VAR>f : α → E<VAR>inst✝ : One E<VAR>hf : HasCompactMulSupport f<VAR>K : Set α<VAR>hK1 : IsCompact K<VAR>hK2 : ∀ x ∉ K, f x = 1<VAR>S : ℝ<VAR>hS : S > 0<VAR>hS' : ∀ x ∈ K, ‖x‖ ≤ S<GOAL>∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddGroup α<VAR>f : α → E<VAR>inst✝ : One E<VAR>hf : HasCompactMulSupport f<VAR>K : Set α<VAR>hK1 : IsCompact K<VAR>hK2 : ∀ x ∉ K, f x = 1<VAR>S : ℝ<VAR>hS : S > 0<VAR>hS' : ∀ x ∈ K, ‖x‖ ≤ S<VAR>x : α<VAR>hx : S + 1 ≤ ‖x‖<GOAL>¬‖x‖ ≤ S
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddGroup α<VAR>f : α → E<VAR>inst✝ : One E<VAR>hf : HasCompactMulSupport f<VAR>K : Set α<VAR>hK1 : IsCompact K<VAR>hK2 : ∀ x ∉ K, f x = 1<VAR>S : ℝ<VAR>hS : S > 0<VAR>hS' : ∀ x ∈ K, ‖x‖ ≤ S<VAR>x : α<VAR>hx : ‖x‖ ≤ S<GOAL>‖x‖ < S + 1
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>f : C(X, Y)<VAR>A A' : DiscreteQuotient X<VAR>B B' : DiscreteQuotient Y<VAR>g : C(Y, Z)<VAR>C : DiscreteQuotient Z<GOAL>LEComap g B C → LEComap f A B → LEComap (g.comp f) A C
<VAR>m n✝ n : ℕ<GOAL>↑((val 0).gcdA (n + 1)) = 0
<VAR>m n✝ n : ℕ<GOAL>↑(Nat.gcdA 0 (n + 1)) = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>y : ↥M<VAR>hxy : mk' S 0 y ≠ 0<GOAL>False
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>inst✝ : Nontrivial R<VAR>i j : n<GOAL>(M.charmatrix i j).natDegree = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F'✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'✝<VAR>inst✝² : InnerProductSpace ℝ F'✝<VAR>inst✝¹ : CompleteSpace F'✝<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹<VAR>F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))<VAR>e : F ≃L[ℝ] F' := toEuclidean<VAR>C₁ : ℝ≥0 := ‖↑e.symm‖₊<VAR>C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p<VAR>C₂ : ℝ≥0 := ‖↑e‖₊<VAR>v : E → F' := ⇑e ∘ u<GOAL>eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F'✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'✝<VAR>inst✝² : InnerProductSpace ℝ F'✝<VAR>inst✝¹ : CompleteSpace F'✝<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹<VAR>F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))<VAR>e : F ≃L[ℝ] F' := toEuclidean<VAR>C₁ : ℝ≥0 := ‖↑e.symm‖₊<VAR>C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p<VAR>C₂ : ℝ≥0 := ‖↑e‖₊<VAR>v : E → F' := ⇑e ∘ u<VAR>hv : ContDiff ℝ 1 v<GOAL>eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F'✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'✝<VAR>inst✝² : InnerProductSpace ℝ F'✝<VAR>inst✝¹ : CompleteSpace F'✝<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹<VAR>F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))<VAR>e : F ≃L[ℝ] F' := toEuclidean<VAR>C₁ : ℝ≥0 := ‖↑e.symm‖₊<VAR>C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p<VAR>C₂ : ℝ≥0 := ‖↑e‖₊<VAR>v : E → F' := ⇑e ∘ u<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<GOAL>eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F'✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'✝<VAR>inst✝² : InnerProductSpace ℝ F'✝<VAR>inst✝¹ : CompleteSpace F'✝<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹<VAR>F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))<VAR>e : F ≃L[ℝ] F' := toEuclidean<VAR>C₁ : ℝ≥0 := ‖↑e.symm‖₊<VAR>C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p<VAR>C₂ : ℝ≥0 := ‖↑e‖₊<VAR>v : E → F' := ⇑e ∘ u<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<VAR>this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ<GOAL>eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F'✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'✝<VAR>inst✝² : InnerProductSpace ℝ F'✝<VAR>inst✝¹ : CompleteSpace F'✝<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹<VAR>F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))<VAR>e : F ≃L[ℝ] F' := toEuclidean<VAR>C₁ : ℝ≥0 := ‖↑e.symm‖₊<VAR>C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p<VAR>C₂ : ℝ≥0 := ‖↑e‖₊<VAR>v : E → F' := ⇑e ∘ u<VAR>hv : ContDiff ℝ 1 v<VAR>h2v : HasCompactSupport v<VAR>this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ<VAR>h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖<GOAL>eLpNorm u (↑p') μ ≤ ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : X'<VAR>y : ↑(Set.range fun x => x • ↑(MonoidHom.range f))<GOAL>fromCoset ⟨1 • ↑y, ⋯⟩ = fromCoset y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<VAR>this : (⋃ l ∈ s, ⋃ u ∈ s, ⋃ (_ : l < u), {Ico l u}).Countable<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<VAR>this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<VAR>this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable<GOAL>{x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} ⊆ {S | ∃ l u, l < u ∧ Ico l u = S}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<VAR>this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable<GOAL>⋃₀ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2} = univ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<VAR>this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable<GOAL>∀ s_1 ∈ {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}, μ s_1 ≠ ⊤
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : NoMaxOrder α<VAR>μ ν : Measure α<VAR>hμ : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) ≠ ⊤<VAR>h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsd : Dense s<VAR>hsb : ∀ (x : α), IsBot x → x ∈ s<VAR>right✝ : ∀ (x : α), IsTop x → x ∈ s<VAR>this : {x | ∃ i, ∃ (_ : i ∈ s), ∃ i_2, ∃ (_ : i_2 ∈ s) (_ : i < i_2), x = Ico i i_2}.Countable<GOAL>∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint g<VAR>x : α<VAR>hf : f x = x<VAR>hg : f (g x) = g x<GOAL>(f * g) x = (g * f) x
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint g<VAR>x : α<VAR>hf : f x = x<VAR>hg : g (g x) = g x<GOAL>(f * g) x = (g * f) x