ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>ha : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = ↑(Ideal.span {a})<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) * ∏ᶠ (x : HeightOneSpectrum R), (↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))⁻¹
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>ha : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = ↑(Ideal.span {a})<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) * ∏ᶠ (x : HeightOneSpectrum R), ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>ha : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = ↑(Ideal.span {a})<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = ∏ᶠ (i : HeightOneSpectrum R), ↑i.asIdeal ^ ↑((Associates.mk i.asIdeal).count (Associates.mk J).factors) * ↑i.asIdeal ^ (-↑((Associates.mk i.asIdeal).count (Associates.mk (Ideal.span {a})).factors))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>ha : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = ↑(Ideal.span {a})<GOAL>∀ (x : HeightOneSpectrum R), ↑x.asIdeal ^ (↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk J).factors) * ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>ha : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = ↑(Ideal.span {a})<VAR>v : HeightOneSpectrum R<GOAL>↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) * ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors))
<VAR>cf : Code<GOAL>cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4
<VAR>cf : Code<VAR>this : 1 * cf.encodeCode ≤ 2 * 2 * cf.encodeCode<GOAL>cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4
<VAR>cf : Code<VAR>this : cf.encodeCode ≤ 2 * (2 * cf.encodeCode)<GOAL>cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4
<VAR>cf : Code<VAR>this : cf.encodeCode ≤ 2 * (2 * cf.encodeCode)<GOAL>2 * (2 * cf.encodeCode) ≤ 2 * (2 * cf.encodeCode + 1) + 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁶ : Fintype ι<VAR>inst✝¹⁵ : Fintype ι'<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁹ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : SeminormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f✝ g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedSpace 𝕜' G<VAR>inst✝¹ : SMulCommClass 𝕜 𝕜' G<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>f : G →L[𝕜] G'<VAR>this : Unique ι := uniqueOfSubsingleton i<GOAL>‖(ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this : ProperSpace E<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝ : ProperSpace E<VAR>this : FiniteDimensional 𝕜 E<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I : Function.Bijective ⇑(L.domRestrict T)<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I<VAR>L'_cont : Continuous ⇑L'<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I✝ : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<VAR>I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))<VAR>μS : Measure ↥S := addHaar<VAR>μT : Measure ↥T := addHaar<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I✝ : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<VAR>I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))<VAR>μS : Measure ↥S := addHaar<VAR>μT : Measure ↥T := addHaar<VAR>c₀ : ℝ≥0∞<VAR>c₀_pos : c₀ ≠ 0<VAR>c₀_fin : c₀ ≠ ⊤<VAR>h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I✝ : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<VAR>I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))<VAR>μS : Measure ↥S := addHaar<VAR>μT : Measure ↥T := addHaar<VAR>c₀ : ℝ≥0∞<VAR>c₀_pos : c₀ ≠ 0<VAR>c₀_fin : c₀ ≠ ⊤<VAR>h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT<VAR>J : map (⇑P) (μS.prod μT) = μS univ • μT<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>this✝¹ : ProperSpace E<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace F<VAR>S : Submodule 𝕜 E := ker L<VAR>T : Submodule 𝕜 E<VAR>hT : IsCompl S T<VAR>M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT<VAR>M_cont : Continuous ⇑M.symm<VAR>P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T<VAR>P_cont : Continuous ⇑P<VAR>I✝ : Function.Bijective ⇑(L.domRestrict T)<VAR>L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I✝<VAR>L'_cont : Continuous ⇑L'<VAR>A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm<VAR>I : map (⇑L) μ = map (⇑L') (map (⇑P) (map (⇑M.symm) μ))<VAR>μS : Measure ↥S := addHaar<VAR>μT : Measure ↥T := addHaar<VAR>c₀ : ℝ≥0∞<VAR>c₀_pos : c₀ ≠ 0<VAR>c₀_fin : c₀ ≠ ⊤<VAR>h₀ : map (⇑M.symm) μ = c₀ • μS.prod μT<VAR>J : map (⇑P) (μS.prod μT) = μS univ • μT<VAR>c₁ : ℝ≥0∞<VAR>c₁_pos : c₁ ≠ 0<VAR>c₁_fin : c₁ ≠ ⊤<VAR>h₁ : map (⇑L') μT = c₁ • ν<GOAL>∃ c, 0 < c ∧ c < ⊤ ∧ map (⇑L) μ = (c * addHaar univ) • ν