ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>L : E ≃L[𝕜] F<VAR>φ : X → E<VAR>this : CompleteSpace E ↔ CompleteSpace F<VAR>left✝ : CompleteSpace E<VAR>right✝ : CompleteSpace F<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>L : E ≃L[𝕜] F<VAR>φ : X → E<VAR>this : CompleteSpace E ↔ CompleteSpace F<VAR>left✝ : ¬CompleteSpace E<VAR>right✝ : ¬CompleteSpace F<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>cos (arccos x) = x
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>inst✝⁶ : Free K V<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : M ≃ₗ[R] N<VAR>ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap<GOAL>Bijective ⇑(Dual.eval R N)
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>inst✝⁶ : Free K V<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : M ≃ₗ[R] N<VAR>ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap<VAR>this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm<GOAL>Bijective ⇑(Dual.eval R N)
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>inst✝⁶ : Free K V<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : M ≃ₗ[R] N<VAR>ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap<VAR>this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm<GOAL>Bijective (⇑(Dual.eval R M) ∘ ⇑e.symm)
<VAR>α : Type u<VAR>l l' : List α<VAR>x : α<GOAL>[x] ~r l ↔ [x] = l
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>s : Set V<GOAL>(induce s G).Connected ↔ (⊤.induce s).Connected
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : Mul M<VAR>inst✝² : Mul N<VAR>a x y : M<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulHomClass F M N<VAR>h : SemiconjBy a x y<VAR>f : F<GOAL>SemiconjBy (f a) (f x) (f y)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.101505<VAR>inst✝ : MulAction R X<VAR>r : R<VAR>s t : ↥S<GOAL>1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)
<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>s : Set H<GOAL>↑I '' s = ↑I.symm ⁻¹' s ∩ range ↑I
<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>s : Set H<GOAL>s ⊆ I.source
<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>s : Set H<GOAL>I.target ∩ ↑I.symm ⁻¹' s = ↑I.symm ⁻¹' s ∩ range ↑I
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B✝ A B : Matrix n n α<VAR>h : IsUnit A ↔ IsUnit B<GOAL>A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<GOAL>∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>hσ : ↑(f i) ^ 2 + ↑(f ((swap i 0) 1)) ^ 2 = 0 ∧ ↑(f ((swap i 0) 2)) ^ 2 + ↑(f ((swap i 0) 3)) ^ 2 = 0<GOAL>∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>σ : Perm (Fin 4) := swap i 0<VAR>hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0<GOAL>∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>σ : Perm (Fin 4) := swap i 0<VAR>hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0<VAR>x : ℤ<VAR>hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x<GOAL>∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>σ : Perm (Fin 4) := swap i 0<VAR>hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0<VAR>x : ℤ<VAR>hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x<VAR>y : ℤ<VAR>hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y<GOAL>∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>σ : Perm (Fin 4) := swap i 0<VAR>hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0<VAR>x : ℤ<VAR>hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x<VAR>y : ℤ<VAR>hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y<GOAL>((f (σ 0) - f (σ 1)) / 2) ^ 2 + ((f (σ 0) + f (σ 1)) / 2) ^ 2 + ((f (σ 2) - f (σ 3)) / 2) ^ 2 + ((f (σ 2) + f (σ 3)) / 2) ^ 2 = m
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>σ : Perm (Fin 4) := swap i 0<VAR>hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0<VAR>x : ℤ<VAR>hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x<VAR>y : ℤ<VAR>hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y<GOAL>2 * x + 2 * y = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2
<VAR>m a b c d : ℤ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m<VAR>this✝ : ∀ (f : Fin 4 → ZMod 2), f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0<VAR>f : Fin 4 → ℤ := ![a, b, c, d]<VAR>i : Fin 4<VAR>σ : Perm (Fin 4) := swap i 0<VAR>hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0<VAR>x : ℤ<VAR>hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x<VAR>y : ℤ<VAR>hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y<VAR>this : ∑ x : Fin 4, f (σ x) ^ 2 = ∑ x : Fin 4, f x ^ 2<GOAL>2 * x + 2 * y = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>T : s.tail.head.Terminates<GOAL>s.destruct.Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>T : s.tail.head.Terminates<VAR>a : Option (α × WSeq α)<VAR>h : a ∈ s.tail.destruct<GOAL>s.destruct.Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>T : s.tail.head.Terminates<VAR>a : Option (α × WSeq α)<VAR>h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> s.destruct >>= destruct<GOAL>s.destruct.Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>T : s.tail.head.Terminates<VAR>a : Option (α × WSeq α)<VAR>h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> s.destruct >>= destruct<VAR>s' : WSeq α<VAR>h1 : s' ∈ (fun o => Option.rec nil Prod.snd o) <$> s.destruct<VAR>right✝ : a ∈ s'.destruct<GOAL>s.destruct.Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>T : s.tail.head.Terminates<VAR>a : Option (α × WSeq α)<VAR>h : a ∈ (fun o => Option.rec nil Prod.snd o) <$> s.destruct >>= destruct<VAR>s' : WSeq α<VAR>h1 : s' ∈ Applicative.toFunctor.1 (fun o => Option.rec nil Prod.snd o) s.destruct<VAR>right✝ : a ∈ s'.destruct<GOAL>s.destruct.Terminates
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>hs : IsZlattice K L<GOAL>L.FG
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>hs : IsZlattice K L<GOAL>(AddSubgroup.toIntSubmodule L).FG
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>hs : IsZlattice K L<VAR>s : Set E<VAR>h_incl : s ⊆ ↑L<VAR>h_span : span K s = span K ↑L<VAR>h_lind : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>(AddSubgroup.toIntSubmodule L).FG
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>hs : IsZlattice K L<VAR>s : Set E<VAR>h_incl : s ⊆ ↑L<VAR>h_span : span K s = span K ↑L<VAR>h_lind : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>(map (span ℤ s).mkQ (AddSubgroup.toIntSubmodule L)).FG
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>hs : IsZlattice K L<VAR>s : Set E<VAR>h_incl : s ⊆ ↑L<VAR>h_span : span K s = span K ↑L<VAR>h_lind : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>(AddSubgroup.toIntSubmodule L ⊓ LinearMap.ker (span ℤ s).mkQ).FG
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>left✝ : SymmetricRel w<VAR>w_sub : w ○ w ⊆ s<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>left✝ : SymmetricRel w<VAR>w_sub : w ○ w ⊆ s<VAR>t : Set (α × α)<VAR>t_in : t ∈ 𝓤 α<VAR>t_symm : SymmetricRel t<VAR>t_sub : t ○ t ⊆ w<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>left✝ : SymmetricRel w<VAR>w_sub : w ○ w ⊆ s<VAR>t : Set (α × α)<VAR>t_in : t ∈ 𝓤 α<VAR>t_symm : SymmetricRel t<VAR>t_sub : t ○ t ⊆ w<GOAL>t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>left✝ : SymmetricRel w<VAR>w_sub : w ○ w ⊆ s<VAR>t : Set (α × α)<VAR>t_in : t ∈ 𝓤 α<VAR>t_symm : SymmetricRel t<VAR>t_sub : t ○ t ⊆ w<VAR>this : t ⊆ t ○ t<GOAL>t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>left✝ : SymmetricRel w<VAR>w_sub : w ○ w ⊆ s<VAR>t : Set (α × α)<VAR>t_in : t ∈ 𝓤 α<VAR>t_symm : SymmetricRel t<VAR>t_sub : t ○ t ⊆ w<VAR>this : t ⊆ t ○ t<VAR>ht : t ⊆ t<GOAL>t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>left✝ : SymmetricRel w<VAR>w_sub : w ○ w ⊆ s<VAR>t : Set (α × α)<VAR>t_in : t ∈ 𝓤 α<VAR>t_symm : SymmetricRel t<VAR>t_sub : t ○ t ⊆ w<VAR>this : t ⊆ t ○ t<VAR>ht : t ⊆ t<VAR>hw : w ⊆ w<GOAL>t ○ t ○ t ⊆ s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ |∫ (x : ℝ) in a..b, ‖f x‖ ∂μ|
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<GOAL>‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ ‖∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ‖
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H.toLieSubmodule<GOAL>x ∈ rootSpace H 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<GOAL>x ∈ rootSpace H 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<GOAL>∀ (x_1 : ↥H), ∃ k, ((toEnd R (↥H) L) x_1 ^ k) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<GOAL>∃ k, ((toEnd R (↥H) L) y ^ k) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<GOAL>((toEnd R (↥H) L) y ^ k) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<GOAL>((toEnd R (↥H) L) y ^ k) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<VAR>hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f<GOAL>((toEnd R (↥H) L) y ^ k) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<VAR>hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f<GOAL>((g ^ k) ∘ₗ H.subtype) ⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<VAR>hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f<GOAL>(H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<VAR>hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f<VAR>h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ ∈ lowerCentralSeries R (↥H) (↥H) k<GOAL>(H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<VAR>hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f<VAR>h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ = 0<GOAL>(H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>hx : x ∈ H<VAR>y : ↥H<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥H) (↥H) k = ⊥<VAR>f : Module.End R ↥H := (toEnd R ↥H ↥H) y<VAR>g : Module.End R L := (toEnd R (↥H) L) y<VAR>hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f<VAR>h : (⇑((toEnd R ↥H ↥H) y))^[k] ⟨x, hx⟩ = 0<GOAL>(⇑f)^[k] ⟨x, hx⟩ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ [[b, c]] → b ∈ [[a, c]] → a = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b
<VAR>α : Type u_1<VAR>m : Num<VAR>n : ℕ<GOAL>↑(m >>> n) = ↑m >>> n
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>↑0 = ↑zero >>> n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>m : PosNum<GOAL>↑(m >>> n) = ↑(pos m) >>> n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n<VAR>m : PosNum<GOAL>↑(m >>> (n + 1)) = ↑(pos m) >>> (n + 1)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n<VAR>m : PosNum<VAR>hdiv2 : ∀ (m : ℕ), (m + m).div2 = m<GOAL>↑(m >>> (n + 1)) = ↑(pos m) >>> (n + 1)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n<VAR>hdiv2 : ∀ (m : ℕ), (m + m).div2 = m<GOAL>↑0 = ↑(pos one) >>> (n + 1)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n<VAR>hdiv2 : ∀ (m : ℕ), (m + m).div2 = m<VAR>m : PosNum<GOAL>↑(m.shiftr n) = ↑(pos m.bit1) >>> (n + 1)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n<VAR>hdiv2 : ∀ (m : ℕ), (m + m).div2 = m<VAR>m : PosNum<GOAL>↑(m.shiftr n) = ↑(pos m.bit0) >>> (n + 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y < z \ x<VAR>hxz : x ≤ z<GOAL>x ⊔ y < z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y < z \ x<VAR>hxz : x ≤ z<GOAL>x ⊔ y < x ⊔ z \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y < z \ x<VAR>hxz : x ≤ z<VAR>h' : x ⊔ z \ x ≤ x ⊔ y<GOAL>z \ x ≤ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : y < z \ x<VAR>hxz : x ≤ z<VAR>h' : x ⊔ z \ x ≤ x ⊔ y<GOAL>(z \ x) \ x ≤ y
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a / b < c ↔ a < b * c
<VAR>x : ℤ<VAR>hx : x ≠ 0<VAR>n d : ℤ<GOAL>x /. n / (x /. d) = d /. n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>2 / (1 - 2 / rexp 1) ≤ 8
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>8 * 2 ≤ (8 - 2) * rexp 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>0 < 1 - 2 / rexp 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<GOAL>(∀ (x : Set Y), IsOpen xᶜ → IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)
<VAR>q : ℚ≥0<VAR>hq : q ≠ 0<GOAL>q⁻¹.num = q.den
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X✝ : Type w'<VAR>inst✝ : TopologicalSpace X✝<VAR>X : TopCat<GOAL>EqualizerCondition (yonedaPresheaf compHausToTop ↑X)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X✝ : Type w'<VAR>inst✝ : TopologicalSpace X✝<VAR>X : TopCat<GOAL>∀ (Z B : CompHaus) (π : Z ⟶ B) [inst : EffectiveEpi π], QuotientMap ⇑(compHausToTop.map π)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>G : C ⥤ TopCat<VAR>X✝ : Type w'<VAR>inst✝ : TopologicalSpace X✝<VAR>X : TopCat<VAR>Z B : CompHaus<VAR>π : Z ⟶ B<VAR>he : EffectiveEpi π<GOAL>QuotientMap ⇑(compHausToTop.map π)