ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>l : Filter α<VAR>f : α → C(Y, Z)<VAR>g : C(Y, Z)<GOAL>Tendsto f l (𝓝 g) ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : α) in l, MapsTo (⇑(f a)) K U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : ContinuousOn g K<VAR>hg' : IntegrableOn g' A μ<VAR>hK : IsCompact K<VAR>hA : MeasurableSet A<VAR>hAK : A ⊆ K<GOAL>IntegrableOn (fun x => g x * g' x) A μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : ContinuousOn g K<VAR>hg' : IntegrableOn g' A μ<VAR>hK : IsCompact K<VAR>hA : MeasurableSet A<VAR>hAK : A ⊆ K<VAR>C : ℝ<VAR>hC : ∀ x ∈ K, ‖g x‖ ≤ C<GOAL>IntegrableOn (fun x => g x * g' x) A μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : ContinuousOn g K<VAR>hg' : Memℒp g' 1 (μ.restrict A)<VAR>hK : IsCompact K<VAR>hA : MeasurableSet A<VAR>hAK : A ⊆ K<VAR>C : ℝ<VAR>hC : ∀ x ∈ K, ‖g x‖ ≤ C<GOAL>Memℒp (fun x => g x * g' x) 1 (μ.restrict A)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>g g' : X → R<VAR>hg : ContinuousOn g K<VAR>hg' : Memℒp g' 1 (μ.restrict A)<VAR>hK : IsCompact K<VAR>hA : MeasurableSet A<VAR>hAK : A ⊆ K<VAR>C : ℝ<VAR>hC : ∀ x ∈ K, ‖g x‖ ≤ C<VAR>this : ∀ᵐ (x : X) ∂μ.restrict A, ‖g x * g' x‖ ≤ C * ‖g' x‖<GOAL>Memℒp (fun x => g x * g' x) 1 (μ.restrict A)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<GOAL>Injective ⇑(Quotient.lift I f H) ↔ ker f = I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<GOAL>ker f ≤ I ↔ ker f = I
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>i : α<VAR>β : α → Type u_2<VAR>f : β i × ((j : { j // j ≠ i }) → β ↑j)<GOAL>((fun f => (f i, fun j => f ↑j)) ((fun f j => if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩) f)).1 = f.1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>i : α<VAR>β : α → Type u_2<VAR>f : β i × ((j : { j // j ≠ i }) → β ↑j)<VAR>x : { j // j ≠ i }<GOAL>((fun f => (f i, fun j => f ↑j)) ((fun f j => if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩) f)).2 x = f.2 x
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<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 F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>one_le_p : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>f : α → F<VAR>hf : Memℒp f p (μ.trim hm)<GOAL>↑↑↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (Memℒp.toLp f hf)) =ᶠ[ae μ] ↑↑(Memℒp.toLp f ⋯)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<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 F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>one_le_p : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>f : α → F<VAR>hf : Memℒp f p (μ.trim hm)<GOAL>↑↑(Memℒp.toLp f hf) =ᶠ[ae μ] ↑↑(Memℒp.toLp f ⋯)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝ : atBot.IsMeasurablyGenerated<VAR>hf : LocallyIntegrableOn f (Iic a) μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<GOAL>IntegrableOn f (Iic a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝ : atBot.IsMeasurablyGenerated<VAR>hf : LocallyIntegrableOn f (Iic a) μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<GOAL>StronglyMeasurableAtFilter f atBot μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>h : _root_.Disjoint s t<GOAL>(↑s ∪ ↑t).offDiag = (↑s).offDiag ∪ (↑t).offDiag ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s
<VAR>n : ℕ<GOAL>0 ≤ ↑n
<VAR>n : ℕ<GOAL>0 ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>x₀ : E'<VAR>n m : ℕ<VAR>h : n < m<GOAL>Tendsto (fun x => ‖x - x₀‖) (𝓝 x₀) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>x₀ : E'<VAR>n m : ℕ<VAR>h : n < m<GOAL>Tendsto (fun x => x - x₀) (𝓝 x₀) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>x₀ : E'<VAR>n m : ℕ<VAR>h : n < m<GOAL>Tendsto (fun x => x - x₀) (𝓝 x₀) (𝓝 (x₀ - x₀))
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<GOAL>μ.everywherePosSubset s =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<GOAL>∀ i ⊆ s \ μ.everywherePosSubset s, IsCompact i → μ i = 0
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k✝ : Set α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.InnerRegular<VAR>hs : MeasurableSet s<VAR>k : Set α<VAR>hk : k ⊆ s \ μ.everywherePosSubset s<VAR>h'k : IsCompact k<GOAL>μ k = 0
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<GOAL>natSepDegree 1 = 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.ΨSq (-n) = W.ΨSq n
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ a<GOAL>z = ↑z.re
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ a<VAR>hu : NormedSpace.exp ℂ (I • a) ∈ unitary A<GOAL>z = ↑z.re
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ a<VAR>hu : NormedSpace.exp ℂ (I • a) ∈ unitary A<VAR>Iu : ℂˣ := Units.mk0 I I_ne_zero<GOAL>z = ↑z.re
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>z : ℂ<VAR>hz : z ∈ spectrum ℂ a<VAR>hu : NormedSpace.exp ℂ (I • a) ∈ unitary A<VAR>Iu : ℂˣ := Units.mk0 I I_ne_zero<VAR>this : NormedSpace.exp ℂ (I • z) ∈ spectrum ℂ (NormedSpace.exp ℂ (I • a))<GOAL>z = ↑z.re
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>h : dist x y < (1 / 2) ^ n<VAR>i : ℕ<VAR>hi : i ≤ n<GOAL>x i = y i
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>n i : ℕ<VAR>hi : i ≤ n<VAR>h : dist x x < (1 / 2) ^ n<GOAL>x i = x i
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>h : dist x y < (1 / 2) ^ n<VAR>i : ℕ<VAR>hi : i ≤ n<VAR>hne : x ≠ y<GOAL>x i = y i
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>h : dist x y < (1 / 2) ^ n<VAR>i : ℕ<VAR>hi : i ≤ n<VAR>hne : x ≠ y<VAR>this : n < firstDiff x y<GOAL>x i = y i
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<GOAL>M.Basis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<GOAL>(∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e✝ : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>h : (∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E<VAR>e : α<VAR>he : e ∈ X \ I<VAR>hi : M.Indep (insert e I)<GOAL>e ∈ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J✝ X Y : Set α<VAR>e✝ : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>h : ∀ e ∈ X \ I, M.Dep (insert e I)<VAR>J : Set α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<VAR>e : α<VAR>heJ : e ∈ J<VAR>heI : e ∉ I<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>h : ∀ e ∈ X \ I, M.Dep (insert e I)<GOAL>X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>h : ∀ e ∈ X \ I, M.Dep (insert e I)<GOAL>X \ I ⊆ M.E
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I'✝ : Ideal R<VAR>J✝ J'✝ : Ideal S<VAR>I I' : Ideal R<VAR>J J' : Ideal S<GOAL>I.prod J = I'.prod J' ↔ I = I' ∧ J = J'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : OrderedCommSemiring α<VAR>inst✝² : OrderedSemiring β<VAR>inst✝¹ : Algebra α β<VAR>inst✝ : SMulPosMono α β<VAR>a a₁ a₂ : α<VAR>ha : a₁ ≤ a₂<GOAL>(algebraMap α β) a₁ ≤ (algebraMap α β) a₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝² : CommSemigroup R<VAR>inst✝¹ : SMul R M<VAR>inst✝ : IsScalarTower R R M<GOAL>IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝² : CommSemigroup R<VAR>inst✝¹ : SMul R M<VAR>inst✝ : IsScalarTower R R M<GOAL>IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>SS : Seq (Seq1 (Seq1 α))<GOAL>SS.join.join = (Seq.map join SS).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>SS : Seq (Seq1 (Seq1 α))<GOAL>Seq.IsBisimulation fun s1 s2 => ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>SS : Seq (Seq1 (Seq1 α))<GOAL>∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.60429, u_1} C<VAR>inst✝² : Category.{?u.60433, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S✝ S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>S : ShortComplex Cᵒᵖ<GOAL>S.g.unop ≫ S.f.unop = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.60429, u_1} C<VAR>inst✝² : Category.{?u.60433, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S✝ S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>S : ShortComplex Cᵒᵖ<GOAL>Quiver.Hom.unop 0 = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(map Prod.snd (μ.prod ν)) s = (μ univ • ν) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s✝ t : Set α<VAR>E : Type u_3<VAR>inst✝¹ : EquivLike E α β<VAR>inst✝ : OrderIsoClass E α β<VAR>e : E<VAR>s : Set α<VAR>hs : s.OrdConnected<GOAL>(⇑e '' s).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s✝ t : Set α<VAR>E : Type u_3<VAR>inst✝¹ : EquivLike E α β<VAR>inst✝ : OrderIsoClass E α β<VAR>e : E<VAR>s : Set α<VAR>hs : s.OrdConnected<GOAL>(⇑(↑e).symm ⁻¹' s).OrdConnected
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>s : Finset α<VAR>i : α → ℕ<VAR>is_prime : ∀ p ∈ s, Prime p<VAR>is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this : DecidableEq α := Classical.decEq α<GOAL>P (∏ p ∈ s, p ^ i p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>i : α → ℕ<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this : DecidableEq α := Classical.decEq α<VAR>is_prime : ∀ p ∈ ∅, Prime p<VAR>is_coprime : ∀ p ∈ ∅, ∀ q ∈ ∅, p ∣ q → p = q<GOAL>P (∏ p ∈ ∅, p ^ i p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>i : α → ℕ<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>f' : Finset α<VAR>hpf' : p ∉ f'<VAR>ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)<VAR>is_prime : ∀ p_1 ∈ insert p f', Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q<GOAL>P (∏ p ∈ insert p f', p ^ i p)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>i : α → ℕ<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this : DecidableEq α := Classical.decEq α<VAR>p : α<VAR>f' : Finset α<VAR>hpf' : p ∉ f'<VAR>ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)<VAR>is_prime : ∀ p_1 ∈ insert p f', Prime p_1<VAR>is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q<GOAL>P (p ^ i p * ∏ x ∈ f', x ^ i x)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>i : Fin 2 → ℤ<VAR>A : SL(2, ℤ)<VAR>z : ℍ<GOAL>eisSummand k i (A • z) = denom (↑A) z ^ k * eisSummand k (i ᵥ* ↑A) z
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>i : Fin 2 → ℤ<VAR>A : SL(2, ℤ)<VAR>z : ℍ<GOAL>(↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) = denom (↑A) z ^ k * (↑(i 0 * ↑A 0 0 + i 1 * ↑A 1 0) * ↑z + ↑(i 0 * ↑A 0 1 + i 1 * ↑A 1 1)) ^ (-k)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>k : ℤ<VAR>i : Fin 2 → ℤ<VAR>A : SL(2, ℤ)<VAR>z : ℍ<VAR>h : ∀ (a b c d u v : ℂ), c * ↑z + d ≠ 0 → (u * ((a * ↑z + b) / (c * ↑z + d)) + v) ^ (-k) = (c * ↑z + d) ^ k * ((u * a + v * c) * ↑z + (u * b + v * d)) ^ (-k)<GOAL>(↑(i 0) * ↑(A • z) + ↑(i 1)) ^ (-k) = denom (↑A) z ^ k * ((↑(i 0) * ↑(↑A 0 0) + ↑(i 1) * ↑(↑A 1 0)) * ↑z + (↑(i 0) * ↑(↑A 0 1) + ↑(i 1) * ↑(↑A 1 1))) ^ (-k)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>hp : ¬1 < p<GOAL>pNilradical R p = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>hs : NullMeasurableSet s μ<VAR>t : Set α<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>a : G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>ha : a ^ k = 1<GOAL>card ↥(zpowers a) ≤ k
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>a : G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>ha : a ^ k = 1<GOAL>orderOf a ≤ k
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : CommSemiring F<VAR>inst✝¹ : Semiring E<VAR>inst✝ : Algebra F E<VAR>b : F →ₗ[F] E<VAR>hb : Function.Surjective ⇑b<VAR>x y z : F<VAR>hz : b z = 1<VAR>hy : x • z • b y = x • z • (b 1 * b 1)<GOAL>(algebraMap F E) (x * y) = b x
<VAR>α✝ β α : Type u<GOAL>#α < ℵ₀ ↔ Finite α
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<GOAL>(M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ≤ a ∆ b ↔ Disjoint a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>h : a ≤ a ∆ b<GOAL>Disjoint a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>h : a ≤ (a ⊔ b) \ (a ⊓ b)<GOAL>Disjoint a b
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>hk : k < (ofFn.go f i j h).length<GOAL>(ofFn.go f i j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. β<VAR>g : α → β →. σ<VAR>hf : Partrec f<VAR>hg : Partrec₂ g<VAR>n : ℕ<GOAL>(((↑(decode n)).bind fun y => map (Nat.pair n) (map encode (f y))).bind fun n => (↑((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a => map encode (g a.1 a.2)) = (↑(decode n)).bind fun a => (f a).bind fun y => map encode (g a y)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>H K : Subgroup G<GOAL>map f H = map f K ↔ H ⊔ f.ker = K ⊔ f.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>H : Subgroup G<GOAL>map f H = f.range ↔ Codisjoint H f.ker
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<GOAL>((listTransvecCol M).prod * M) (inl i) (inr ()) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<GOAL>∀ k ≤ r, ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())