ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype V<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Field R<VAR>inst✝ : CharZero R<VAR>x : V → R<GOAL>((∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 else 0) + ∑ y : V, ∑ x_1 : V, if G.Adj y x_1 then x x_1 * x x_1 - x x_1 * x y else 0) / 2 = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Fintype V<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Field R<VAR>inst✝ : CharZero R<VAR>x : V → R<GOAL>(∑ x_1 : V, ∑ x_2 : V, if G.Adj x_1 x_2 then x x_1 * x x_1 - x x_1 * x x_2 + (x x_2 * x x_2 - x x_2 * x x_1) else 0 + 0) / 2 = (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>P : Type u_3<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>N : Submodule R M<VAR>hs : N.FG<VAR>t : Set M<VAR>ht : t.Finite ∧ span R t = N<GOAL>span R (⇑f '' t) = Submodule.map f N
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.coeff n ≠ 0<GOAL>p.coeff n ∈ p.coeffs
<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>inst✝ : LawfulApplicative F<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → F β<VAR>x : Option α<GOAL>(fun {α} => η.app α) (Option.traverse f x) = Option.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>z w : ℂ<GOAL>¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>x ∈ interior s ↔ x ∈ {x | s ∈ 𝓝 x}
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<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>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M₁<VAR>h : Surjective ⇑f<GOAL>Module.rank R M = Module.rank R M₁ + Module.rank R ↥(LinearMap.ker f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>im ⟪x, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>I * ((starRingEnd 𝕜) ⟪x, x⟫_𝕜 - ⟪x, x⟫_𝕜) / 2 = ↑0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<VAR>A : Set G<GOAL>(Measure.map (fun h => g * h) μ) A = μ A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>s : Finset ℕ<GOAL>map Fin.valEmbedding (Finset.fin n s) = filter (fun x => x < n) s
<VAR>x n m : ℕ<GOAL>x ∣ n * x.gcd m ↔ x ∣ n * m
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational (1 / x)<GOAL>Irrational (↑1 / x)
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<GOAL>LinearIndependent ℝ G.lapMatrix_ker_basis_aux
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<GOAL>∀ (g : G.ConnectedComponent → ℝ), ∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i = 0 → ∀ (i : G.ConnectedComponent), g i = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>g : G.ConnectedComponent → ℝ<VAR>h0 : ∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i = 0<GOAL>∀ (i : G.ConnectedComponent), g i = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>g : G.ConnectedComponent → ℝ<VAR>h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0<GOAL>∀ (i : G.ConnectedComponent), g i = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>g : G.ConnectedComponent → ℝ<VAR>h0 : ↑(∑ i : G.ConnectedComponent, g i • G.lapMatrix_ker_basis_aux i) = ↑0<VAR>h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)<GOAL>∀ (i : G.ConnectedComponent), g i = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>g : G.ConnectedComponent → ℝ<VAR>h0 : (fun i => g (G.connectedComponentMk i)) = ↑0<VAR>h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)<VAR>c : G.ConnectedComponent<GOAL>g c = 0
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq G.ConnectedComponent<VAR>g : G.ConnectedComponent → ℝ<VAR>h0 : (fun i => g (G.connectedComponentMk i)) = ↑0<VAR>h : ↑(∑ c : G.ConnectedComponent, g c • G.lapMatrix_ker_basis_aux c) = fun i => g (G.connectedComponentMk i)<VAR>c : G.ConnectedComponent<VAR>i : V<VAR>h' : G.connectedComponentMk i = c<GOAL>g c = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : a₁ < b₁ ∨ a₂ < b₂<VAR>e : Ico a₁ b₁ = Ico a₂ b₂<GOAL>a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : a₁ < b₁ ∨ a₂ < b₂<VAR>e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁<GOAL>a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : a₁ < b₁ ∨ a₂ < b₂<VAR>e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁<GOAL>(a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>e : E ≃L[𝕜] F<GOAL>dimH univ = dimH univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a⁻¹ * b = c<GOAL>b = a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : b = a * c<GOAL>a⁻¹ * b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>g : γ → β<VAR>hg : Injective g<VAR>hf : ∀ x ∉ Set.range g, f x = 1<GOAL>HasProd (f ∘ g) a ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>mα : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (rangeSplitting f ⁻¹' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>b⁻¹ * a ≤ c ↔ a ≤ b * c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>a / b ≤ c ↔ a ≤ b * c
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝ : Inhabited Λ<VAR>M : Machine₀<GOAL>Supports M Set.univ
<VAR>α : Type w<VAR>inst✝ : Finite α<VAR>X : α → CompHaus<VAR>B : CompHaus<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (forget CompHaus).obj (X a)<GOAL>(ι X a ≫ desc X π) x = (π a) x
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s : AList β<GOAL>lookup a (insert a b s) = some b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>{a} ⊆ Iic a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>Iic a ≤ closure {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>↑(lowerClosure {a}) ≤ closure {a}
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>a b : Γ<VAR>L R : ListBlank Γ<GOAL>write b (mk' L (ListBlank.cons a R)) = mk' L (ListBlank.cons b R)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M✝<VAR>inst✝⁹ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R N<VAR>P : Type u_4<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>T : Type u_5<VAR>inst✝⁴ : AddCommGroup T<VAR>inst✝³ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝² : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → AddCommGroup (M i)<VAR>inst✝ : (i : ι) → Module R (M i)<VAR>j : ι<VAR>x : AdicCompletion I (M j)<GOAL>(sum I M) ((DirectSum.of (fun i => AdicCompletion I (M i)) j) x) = (map I (lof R ι M j)) x
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M✝<VAR>inst✝⁹ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R N<VAR>P : Type u_4<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>T : Type u_5<VAR>inst✝⁴ : AddCommGroup T<VAR>inst✝³ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝² : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝¹ : (i : ι) → AddCommGroup (M i)<VAR>inst✝ : (i : ι) → Module R (M i)<VAR>j : ι<VAR>x : AdicCompletion I (M j)<GOAL>(sum I M) ((lof R ι (fun i => AdicCompletion I (M i)) j) x) = (map I (lof R ι M j)) x
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i j : Fin (toList s).length<VAR>h : i < j<GOAL>(List.ofFn s.toFun).get i < (List.ofFn s.toFun).get j
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i j : Fin (toList s).length<VAR>h : i < j<GOAL>s.toFun (Fin.cast ⋯ i) < s.toFun (Fin.cast ⋯ j)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>f : A →ₐ[R] A'<VAR>hf_inj : InjOn ⇑f ↑(adjoin R (range x))<VAR>this : aeval (⇑f ∘ x) = f.comp (aeval x)<GOAL>AlgebraicIndependent R (⇑f ∘ x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>f : A →ₐ[R] A'<VAR>hf_inj : InjOn ⇑f ↑(adjoin R (range x))<VAR>this : aeval (⇑f ∘ x) = f.comp (aeval x)<VAR>h : ∀ (p : MvPolynomial ι R), (aeval x) p ∈ (aeval Subtype.val).range<GOAL>AlgebraicIndependent R (⇑f ∘ x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x✝ : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x✝<VAR>f : A →ₐ[R] A'<VAR>hf_inj : InjOn ⇑f ↑(adjoin R (range x✝))<VAR>this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)<VAR>h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range<VAR>x y : MvPolynomial ι R<VAR>hxy : (f.comp (aeval x✝)) x = (f.comp (aeval x✝)) y<GOAL>x = y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x✝ : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x✝<VAR>f : A →ₐ[R] A'<VAR>hf_inj : InjOn ⇑f ↑(aeval Subtype.val).range<VAR>this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)<VAR>h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range<VAR>x y : MvPolynomial ι R<VAR>hxy : (f.comp (aeval x✝)) x = (f.comp (aeval x✝)) y<GOAL>x = y
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<VAR>ho' : ω ≤ o<GOAL>∃ a, (aleph a).ord = o
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<VAR>ho' : ω ≤ o<VAR>a : Ordinal.{u_1}<VAR>ha : (aleph' a).ord = o<GOAL>∃ a, (aleph a).ord = o
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<VAR>ho' : ω ≤ o<VAR>a : Ordinal.{u_1}<VAR>ha : (aleph' a).ord = o<GOAL>(aleph (a - ω)).ord = o
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<VAR>ho' : ω ≤ o<VAR>a : Ordinal.{u_1}<VAR>ha : (aleph' a).ord = o<GOAL>(aleph' (ω + (a - ω))).ord = o
<VAR>o : Ordinal.{u_1}<VAR>ho : o.card.ord = o<VAR>ho' : ω ≤ o<VAR>a : Ordinal.{u_1}<VAR>ha : (aleph' a).ord = o<GOAL>ω ≤ a
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<GOAL>μ[f|m] = if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<GOAL>(if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0) = if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<GOAL>(if h : Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0) = if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable'.mk ↑↑(condexpL1 hm μ f) ⋯ else 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x y : MvPolynomial R ℚ<GOAL>teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x y : MvPolynomial R ℚ<GOAL>ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x * teichmullerFun p y)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x y : MvPolynomial R ℚ<GOAL>ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x y : MvPolynomial R ℚ<VAR>n : ℕ<GOAL>ghostMap (teichmullerFun p (x * y)) n = (ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)) n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b : R<VAR>s : S<VAR>inst✝³ : SMul R M<VAR>inst✝² : SMul R S<VAR>inst✝¹ : SMul S M<VAR>inst✝ : IsScalarTower R S M<VAR>a : R<VAR>ab : IsSMulRegular M (a • s)<VAR>c d : M<VAR>cd : ((fun m => a • m) ∘ fun x => s • x) c = ((fun m => a • m) ∘ fun x => s • x) d<GOAL>c = d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b : R<VAR>s : S<VAR>inst✝³ : SMul R M<VAR>inst✝² : SMul R S<VAR>inst✝¹ : SMul S M<VAR>inst✝ : IsScalarTower R S M<VAR>a : R<VAR>ab : IsSMulRegular M (a • s)<VAR>c d : M<VAR>cd : a • s • c = a • s • d<GOAL>c = d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b : R<VAR>s : S<VAR>inst✝³ : SMul R M<VAR>inst✝² : SMul R S<VAR>inst✝¹ : SMul S M<VAR>inst✝ : IsScalarTower R S M<VAR>a : R<VAR>ab : IsSMulRegular M (a • s)<VAR>c d : M<VAR>cd : (a • s) • c = (a • s) • d<GOAL>c = d
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<GOAL>∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<GOAL>(fun a => μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => μ {a_1 | a < f a_1} * ENNReal.ofReal (g a)
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>t : ℝ<VAR>ht : μ {a | t ≤ f a} = μ {a | t < f a}<GOAL>μ {a | t ≤ f a} * ENNReal.ofReal (g t) = μ {a | t < f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : (i : ι) → κ i → α<GOAL>a ≤ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ≤ f i j
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map f (posFittingComp R L M) ≤ posFittingComp R L M₂
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<GOAL>⨆ i, LieSubmodule.map f (posFittingCompOf R M i) ≤ ⨆ x, posFittingCompOf R M₂ x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>y : L<VAR>m : M<VAR>hm : m ∈ posFittingCompOf R M y<GOAL>m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>y : L<VAR>m : M<VAR>hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m<GOAL>m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>y : L<VAR>m : M<VAR>hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m<GOAL>∀ (k : ℕ), ∃ n, ((toEnd R L M₂) y ^ k) n = f m
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>y : L<VAR>m : M<VAR>hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m<VAR>k : ℕ<VAR>n : M<VAR>hn : ((toEnd R L M) y ^ k) n = m<GOAL>∃ n, ((toEnd R L M₂) y ^ k) n = f m
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>y : L<VAR>m : M<VAR>hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m<VAR>k : ℕ<VAR>n : M<VAR>hn : ((toEnd R L M) y ^ k) n = m<GOAL>((toEnd R L M₂) y ^ k) (f n) = f m