ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝¹ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : T2Space M<VAR>inst✝ : One M'<VAR>n : ℕ∞<VAR>U : Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : ContMDiff I I' n f<VAR>x✝ : M<VAR>x : ↥U<VAR>h : ↑x ∈ mulTSupport (extend Subtype.val f 1)<GOAL>ContMDiffAt I I' n (extend Subtype.val f 1 ∘ Subtype.val) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝¹ : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : T2Space M<VAR>inst✝ : One M'<VAR>n : ℕ∞<VAR>U : Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : ContMDiff I I' n f<VAR>x✝ : M<VAR>x : ↥U<VAR>h : ↑x ∈ mulTSupport (extend Subtype.val f 1)<GOAL>ContMDiffAt I I' n f x
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<GOAL>¬IsCyclic α ↔ exponent α = p
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<VAR>_inst : Fintype α := Fintype.ofFinite α<GOAL>¬IsCyclic α ↔ exponent α = p
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<VAR>_inst : Fintype α := Fintype.ofFinite α<VAR>hα' : Fintype.card α = p ^ 2<GOAL>¬IsCyclic α ↔ exponent α = p
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<VAR>_inst : Fintype α := Fintype.ofFinite α<VAR>hα' : Fintype.card α = p ^ 2<VAR>this : Nontrivial α<GOAL>¬IsCyclic α ↔ exponent α = p
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<VAR>_inst : Fintype α := Fintype.ofFinite α<VAR>hα' : Fintype.card α = p ^ 2<VAR>this : Nontrivial α<VAR>h_cyc : ¬IsCyclic α<VAR>g : α<VAR>hg : g ≠ 1<GOAL>orderOf g = p
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<VAR>_inst : Fintype α := Fintype.ofFinite α<VAR>hα' : Fintype.card α = p ^ 2<VAR>this✝ : Nontrivial α<VAR>h_cyc : ¬IsCyclic α<VAR>g : α<VAR>hg : g ≠ 1<VAR>this : orderOf g ∈ (p ^ 2).divisors<GOAL>orderOf g = p
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hα : Nat.card α = p ^ 2<VAR>_inst : Fintype α := Fintype.ofFinite α<VAR>hα' : Fintype.card α = p ^ 2<VAR>this✝ : Nontrivial α<VAR>h_cyc : ¬IsCyclic α<VAR>g : α<VAR>hg : g ≠ 1<VAR>this : ∃ a < 3, p ^ a = orderOf g<GOAL>orderOf g = p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : Filter (α → β)<VAR>g : Filter α<VAR>s : Set β<GOAL>s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>r : β → γ → Prop<VAR>f : α →ₘ[μ] β<VAR>g : α →ₘ[μ] γ<GOAL>LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r (↑f a) (↑g a)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace<VAR>a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((sheafedSpaceMap f).base p))<VAR>ha : IsUnit ((localizationToStalk (↑S) p) ((Localization.localRingHom (Ideal.comap f p.asIdeal) p.asIdeal f ⋯) ((stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap f) p)) a)))<GOAL>IsUnit a
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace<VAR>a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((sheafedSpaceMap f).base p))<VAR>ha : IsUnit ((Localization.localRingHom (Ideal.comap f p.asIdeal) p.asIdeal f ⋯) ((stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap f) p)) a))<GOAL>IsUnit a
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace<VAR>a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((sheafedSpaceMap f).base p))<VAR>ha : IsUnit ((stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap f) p)) a)<GOAL>IsUnit a
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace<VAR>a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((sheafedSpaceMap f).base p))<VAR>ha : IsUnit ((stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap f) p)) a)<VAR>e_1✝ : ↑((locallyRingedSpaceObj R).presheaf.stalk ((sheafedSpaceMap f).base p)) = ↑((structureSheaf ↑R).presheaf.stalk ((PrimeSpectrum.comap f) p))<GOAL>a = (stalkIso (↑R) ((PrimeSpectrum.comap f) p)).inv ((stalkToFiberRingHom (↑R) ((PrimeSpectrum.comap f) p)) a)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u v u' v' : V<VAR>p : G.Walk u v<GOAL>(Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges
<VAR>α : Type u_1<GOAL>∀ (m n : Num), ↑(m ||| n) = ↑m ||| ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x)) ∂κ a = ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<GOAL>(fun x => F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x))) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<VAR>a✝ : β<VAR>h2f : Integrable (fun y => f (a✝, y)) (η (a, a✝))<VAR>h2g : Integrable (fun y => g (a✝, y)) (η (a, a✝))<GOAL>F (∫ (y : γ), f (a✝, y) + g (a✝, y) ∂η (a, a✝)) = F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) + ∫ (y : γ), g (a✝, y) ∂η (a, a✝))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>p q : Submodule R M<VAR>hpq : Codisjoint p q<VAR>B : BilinForm R M<VAR>hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0<VAR>z : M<VAR>hz : z ∈ p<GOAL>⟨z, hz⟩ ∈ ker (B.restrict p) ↔ ⟨z, hz⟩ ∈ Submodule.comap p.subtype (ker B)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>p q : Submodule R M<VAR>hpq : Codisjoint p q<VAR>B : BilinForm R M<VAR>hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0<VAR>z : M<VAR>hz : z ∈ p<GOAL>(B.restrict p) ⟨z, hz⟩ = 0 ↔ B z = 0
<VAR>m n : ℤ<GOAL>Odd (m * n) ↔ Odd m ∧ Odd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a✝ p : α<VAR>hp : Prime p<VAR>a b : α<VAR>k l : ℕ<VAR>x✝² : p ^ k ∣ a<VAR>x✝¹ : p ^ l ∣ b<VAR>x✝ : p ^ (k + l + 1) ∣ a * b<VAR>x : α<VAR>hx : a = p ^ k * x<VAR>y : α<VAR>hy : b = p ^ l * y<VAR>z : α<VAR>hz : a * b = p ^ (k + l + 1) * z<GOAL>p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a✝ p : α<VAR>hp : Prime p<VAR>a b : α<VAR>k l : ℕ<VAR>x✝² : p ^ k ∣ a<VAR>x✝¹ : p ^ l ∣ b<VAR>x✝ : p ^ (k + l + 1) ∣ a * b<VAR>x : α<VAR>hx : a = p ^ k * x<VAR>y : α<VAR>hy : b = p ^ l * y<VAR>z : α<VAR>hz : a * b = p ^ (k + l + 1) * z<VAR>h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)<VAR>hp0 : p ^ (k + l) ≠ 0<GOAL>x * y = p * z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a✝ p : α<VAR>hp : Prime p<VAR>a b : α<VAR>k l : ℕ<VAR>x✝³ : p ^ k ∣ a<VAR>x✝² : p ^ l ∣ b<VAR>x✝¹ : p ^ (k + l + 1) ∣ a * b<VAR>x : α<VAR>hx : a = p ^ k * x<VAR>y : α<VAR>hy : b = p ^ l * y<VAR>z : α<VAR>hz : a * b = p ^ (k + l + 1) * z<VAR>h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)<VAR>hp0 : p ^ (k + l) ≠ 0<VAR>hpd : p ∣ x * y<VAR>x✝ : p ∣ x<VAR>d : α<VAR>hd : x = p * d<GOAL>a = p ^ (k + 1) * d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a✝ p : α<VAR>hp : Prime p<VAR>a b : α<VAR>k l : ℕ<VAR>x✝³ : p ^ k ∣ a<VAR>x✝² : p ^ l ∣ b<VAR>x✝¹ : p ^ (k + l + 1) ∣ a * b<VAR>x : α<VAR>hx : a = p ^ k * x<VAR>y : α<VAR>hy : b = p ^ l * y<VAR>z : α<VAR>hz : a * b = p ^ (k + l + 1) * z<VAR>h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)<VAR>hp0 : p ^ (k + l) ≠ 0<VAR>hpd : p ∣ x * y<VAR>x✝ : p ∣ y<VAR>d : α<VAR>hd : y = p * d<GOAL>b = p ^ (l + 1) * d
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Projective R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Projective F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P 2 = 0<VAR>hQz : Q 2 = 0<GOAL>P ≈ Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Projective R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Projective F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular ![P 0, P 1, 0]<VAR>hQ : W.Nonsingular Q<VAR>hPz : P 2 = 0<VAR>hQz : Q 2 = 0<GOAL>![P 0, P 1, 0] ≈ Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Projective R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Projective F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular ![P 0, P 1, 0]<VAR>hQ : W.Nonsingular ![Q 0, Q 1, 0]<VAR>hPz : P 2 = 0<VAR>hQz : Q 2 = 0<GOAL>![P 0, P 1, 0] ≈ ![Q 0, Q 1, 0]
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Projective R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Projective F<VAR>P Q : Fin 3 → F<VAR>hPz : P 2 = 0<VAR>hQz : Q 2 = 0<VAR>hP : 0 = P 0 ^ 3 ∧ (¬3 = 0 ∧ ¬P 0 = 0 ∨ ¬P 1 ^ 2 + W.a₁ * P 0 * P 1 = W.a₂ * P 0 ^ 2)<VAR>hQ : 0 = Q 0 ^ 3 ∧ (¬3 = 0 ∧ ¬Q 0 = 0 ∨ ¬Q 1 ^ 2 + W.a₁ * Q 0 * Q 1 = W.a₂ * Q 0 ^ 2)<GOAL>![P 0, P 1, 0] ≈ ![Q 0, Q 1, 0]
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Projective R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Projective F<VAR>P Q : Fin 3 → F<VAR>hPz : P 2 = 0<VAR>hQz : Q 2 = 0<VAR>hP : ¬P 1 = 0<VAR>hQ : ¬Q 1 = 0<GOAL>![0, P 1, 0] ≈ ![0, Q 1, 0]
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>inst✝ : SigmaFinite (μ.trim hm)<GOAL>∫⁻ (a : α), ↑‖↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (x_1 : α) in t, ↑‖↑↑↑((condexpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E'<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>s ∩ t ⊆ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>multinomial {a, b} f = (f a + f b).choose (f a)
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>f : V →ₗ[MonoidAlgebra k G] W<VAR>hf : LinearMap.ker f = ⊥<VAR>A : Type u := MonoidAlgebra k G<VAR>this✝ : Module k W := Module.compHom W (algebraMap k A)<VAR>this : Module k V := Module.compHom V (algebraMap k A)<GOAL>∃ g, g ∘ₗ f = LinearMap.id
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>f : V →ₗ[MonoidAlgebra k G] W<VAR>hf : LinearMap.ker f = ⊥<VAR>A : Type u := MonoidAlgebra k G<VAR>this✝¹ : Module k W := Module.compHom W (algebraMap k A)<VAR>this✝ : Module k V := Module.compHom V (algebraMap k A)<VAR>this : IsScalarTower k A W<GOAL>∃ g, g ∘ₗ f = LinearMap.id
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>f : V →ₗ[MonoidAlgebra k G] W<VAR>hf : LinearMap.ker f = ⊥<VAR>A : Type u := MonoidAlgebra k G<VAR>this✝² : Module k W := Module.compHom W (algebraMap k A)<VAR>this✝¹ : Module k V := Module.compHom V (algebraMap k A)<VAR>this✝ : IsScalarTower k A W<VAR>this : IsScalarTower k A V<GOAL>∃ g, g ∘ₗ f = LinearMap.id
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>f : V →ₗ[MonoidAlgebra k G] W<VAR>hf : LinearMap.ker f = ⊥<VAR>A : Type u := MonoidAlgebra k G<VAR>this✝² : Module k W := Module.compHom W (algebraMap k A)<VAR>this✝¹ : Module k V := Module.compHom V (algebraMap k A)<VAR>this✝ : IsScalarTower k A W<VAR>this : IsScalarTower k A V<VAR>φ : W →ₗ[k] V<VAR>hφ : φ ∘ₗ ↑k f = LinearMap.id<GOAL>∃ g, g ∘ₗ f = LinearMap.id
<VAR>k : Type u<VAR>inst✝⁷ : Field k<VAR>G : Type u<VAR>inst✝⁶ : Fintype G<VAR>inst✝⁵ : Invertible ↑(Fintype.card G)<VAR>inst✝⁴ : Group G<VAR>V : Type u<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module (MonoidAlgebra k G) W<VAR>f : V →ₗ[MonoidAlgebra k G] W<VAR>hf : LinearMap.ker f = ⊥<VAR>A : Type u := MonoidAlgebra k G<VAR>this✝² : Module k W := Module.compHom W (algebraMap k A)<VAR>this✝¹ : Module k V := Module.compHom V (algebraMap k A)<VAR>this✝ : IsScalarTower k A W<VAR>this : IsScalarTower k A V<VAR>φ : W →ₗ[k] V<VAR>hφ : φ ∘ₗ ↑k f = LinearMap.id<GOAL>∀ (x : V), (LinearMap.equivariantProjection G φ ∘ₗ f) x = LinearMap.id x
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsDomain B<VAR>h₁ : Finite ↑S<VAR>h₂ : IsCyclotomicExtension S A B<GOAL>Module.Finite A B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsDomain B<VAR>h₁ : Finite ↑S<VAR>h₂ : IsCyclotomicExtension S A B<VAR>h : Fintype ↑S<GOAL>Module.Finite A B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h₁ : Finite ↑S<VAR>h : Fintype ↑S<GOAL>∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B] [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h₁ : Finite ↑S<VAR>h : Fintype ↑S<VAR>A : Type u<VAR>B : Type v<GOAL>∀ [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B] [h₂ : IsCyclotomicExtension ∅ A B], Module.Finite A B
<VAR>n✝ : ℕ+<VAR>S✝ T : Set ℕ+<VAR>K : Type w<VAR>L : Type z<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h₁ : Finite ↑S✝<VAR>h : Fintype ↑S✝<VAR>n : ℕ+<VAR>S : Set ℕ+<VAR>x✝¹ : n ∉ S<VAR>x✝ : S.Finite<VAR>H : ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B] [h₂ : IsCyclotomicExtension S A B], Module.Finite A B<VAR>A : Type u<VAR>B : Type v<GOAL>∀ [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B] [h₂ : IsCyclotomicExtension (insert n S) A B], Module.Finite A B
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u + 1}<VAR>h : c < univ.{u, u + 1}<GOAL>∃ c', c = lift.{u + 1, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u + 1}<VAR>h : c < univ.{u, u + 1}<VAR>this : c.ord < univ.{u, u + 1}.ord<GOAL>∃ c', c = lift.{u + 1, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u + 1}<VAR>h : c < univ.{u, u + 1}<VAR>this : c.ord < Ordinal.univ.{u, u + 1}<GOAL>∃ c', c = lift.{u + 1, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u + 1}<VAR>h : c < univ.{u, u + 1}<VAR>this : c.ord < Ordinal.univ.{u, u + 1}<VAR>o : Ordinal.{u}<VAR>e : lift.principalSeg.toRelEmbedding o = c.ord<GOAL>∃ c', c = lift.{u + 1, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u + 1}<VAR>h : c < univ.{u, u + 1}<VAR>this✝ : c.ord < Ordinal.univ.{u, u + 1}<VAR>o : Ordinal.{u}<VAR>e : lift.principalSeg.toRelEmbedding o = c.ord<VAR>this : c.ord.card = c<GOAL>∃ c', c = lift.{u + 1, u} c'