ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ (p q : ℝ≥0), p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>s : Set ℝ≥0∞<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>left✝ : 0 ∉ s<VAR>s_top : ⊤ ∉ s<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ (p q : ℝ≥0), p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>s : Set ℝ≥0∞<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>left✝ : 0 ∉ s<VAR>s_top : ⊤ ∉ s<VAR>I : ∀ x ∈ s, x ≠ ⊤<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ (p q : ℝ≥0), p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>s : Set ℝ≥0∞<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>left✝ : 0 ∉ s<VAR>s_top : ⊤ ∉ s<VAR>I : ∀ x ∈ s, x ≠ ⊤<GOAL>∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∀ (p q : ℝ≥0), p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>s : Set ℝ≥0∞<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>left✝ : 0 ∉ s<VAR>s_top : ⊤ ∉ s<VAR>I : ∀ x ∈ s, x ≠ ⊤<VAR>p : ℝ≥0<VAR>hp : ↑p ∈ s<VAR>q : ℝ≥0<VAR>hq : ↑q ∈ s<VAR>hpq : ↑p < ↑q<GOAL>∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>↑n ≤ (C a * X ^ n).trailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>↑n ≤ ((monomial n) a).trailingDegree
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩<GOAL>(range f).WellFoundedOn r ↔ WellFounded (r on f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩<VAR>h : WellFounded (r on f)<GOAL>∀ (a : ↑(range f)), Acc (fun a b => r ↑a ↑b) a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩<VAR>h : WellFounded (r on f)<VAR>c : β<GOAL>Acc (fun a b => r ↑a ↑b) ⟨f c, ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩<VAR>h : WellFounded (r on f)<VAR>c : β<GOAL>∀ {a : β} {b : ↑(range f)}, r ↑b ↑(f' a) → ∃ c, f' c = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<VAR>f' : β → ↑(range f) := fun c => ⟨f c, ⋯⟩<VAR>h : WellFounded (r on f)<VAR>c : β<GOAL>Acc (InvImage (fun a b => r ↑a ↑b) f') c
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a : ℝ<GOAL>Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b b₀ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a : ℝ<GOAL>∀ (x : ℝ), ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) x
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a b₀ : ℝ<GOAL>ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b b₀✝ b₁✝ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a b₀ b₁ : ℝ<VAR>hb₁ : b₁ < b₀<GOAL>ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b b₀✝ b₁✝ b₂✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a b₀ b₁ : ℝ<VAR>hb₁ : b₁ < b₀<VAR>b₂ : ℝ<VAR>hb₂ : b₀ < b₂<GOAL>ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b b₀✝ b₁✝ b₂✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : NoAtoms μ<VAR>h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b<VAR>a b₀ b₁ : ℝ<VAR>hb₁ : b₁ < b₀<VAR>b₂ : ℝ<VAR>hb₂ : b₀ < b₂<GOAL>ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : Nontrivial S<VAR>pb : PowerBasis K S<GOAL>(Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : Nontrivial S<VAR>pb : PowerBasis K S<VAR>d_pos : 0 < pb.dim<GOAL>(Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : Nontrivial S<VAR>pb : PowerBasis K S<VAR>d_pos : 0 < pb.dim<VAR>d_pos' : 0 < (minpoly K pb.gen).natDegree<VAR>this : Nonempty (Fin pb.dim)<GOAL>(Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r<GOAL>hausdorffDist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r<GOAL>∀ x ∈ s, infDist x t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r<GOAL>∀ x ∈ t, infDist x s ≤ r
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝² : OrderedCommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>hf : HasProd f a<VAR>i : ι<VAR>hb : ∀ (j : ι), j ≠ i → 1 ≤ f j<GOAL>f i = ∏ i ∈ {i}, f i
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<GOAL>∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<GOAL>⨆ i, ∑ a ∈ range i.succ, 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑' (k : ℕ), f k
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ a ∈ range n.succ, 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑ x ∈ Ico 2 (2 ^ n + 1), f x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y : C<VAR>h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f<VAR>h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f<GOAL>EckmannHilton.IsUnital (fun x x_1 => rightAdd X Y x x_1) 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>normEDS b c d 4 = d * b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h₀ : 0 < a<VAR>h₁ : a ≠ 1<GOAL>Injective fun x => a ^ x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h₀ : 0 < a<VAR>h₁ : a ≠ 1<VAR>H : a < 1<GOAL>Injective fun x => a ^ x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h₀ : 0 < a<VAR>h₁ : a ≠ 1<VAR>H : 1 < a<GOAL>Injective fun x => a ^ x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Tendsto u atTop atTop<GOAL>∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x y z : M<VAR>hxy : x ∈ span R {y}<VAR>hyz : y ∈ span R {z}<GOAL>x ∈ span R {z}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x y z : M<VAR>hxy : {x} ⊆ ↑(span R {y})<VAR>hyz : {y} ⊆ ↑(span R {z})<GOAL>{x} ⊆ ↑(span R {z})
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : Semigroup S<VAR>a b x y z x' y' : S<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>a * (x * x') = y * y' * a
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>h : preStoneCechUnit a = preStoneCechUnit b<GOAL>g a = g b
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>h : preStoneCechUnit a = preStoneCechUnit b<VAR>e : Ultrafilter.extend g ∘ pure = g<GOAL>g a = g b
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>h : preStoneCechUnit a = preStoneCechUnit b<VAR>e : Ultrafilter.extend g ∘ pure = g<GOAL>Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>h : EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) (pure b)<VAR>e : Ultrafilter.extend g ∘ pure = g<GOAL>Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>e : Ultrafilter.extend g ∘ pure = g<VAR>F G : Ultrafilter α<VAR>h : EqvGen (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) F G<GOAL>Ultrafilter.extend g F = Ultrafilter.extend g G
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>h : x ∈ span R {y}<GOAL>∃ a, a • y = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>h : x ∈ span R {y}<GOAL>∀ x ∈ {y}, ∃ a, a • y = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>h : x ∈ span R {y}<GOAL>∃ a, a • y = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>h : x ∈ span R {y}<GOAL>∀ (x y_1 : M), (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>h : x ∈ span R {y}<GOAL>∀ (a : R) (x : M), (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>y : M<VAR>a : R<GOAL>a • y ∈ span R {y}
<VAR>x✝ y x : ℝ<GOAL>cosh x * 2 = rexp x + rexp (-x)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b c d : α<GOAL>min a c < min b c ↔ a < b ∧ a < c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b c d : α<GOAL>(a < b ∨ c < b) ∧ a < c ↔ a < b ∧ a < c
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₃ : X₂₁ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃<VAR>t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₃ : X₂₁ ⟶ X₂₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃<VAR>t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>h₁₂ ≫ v₁₃ = v₁₂ ≫ t.desc (h₁₂ ≫ v₁₃) h₂₃ ⋯
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.φ 0 = 1
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(A.updateColumn i fun k => A k i + A k j).det = A.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(Aᵀ.updateRow i fun k => A k i + A k j).det = Aᵀ.det
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>ha : a ≠ 0<VAR>x✝ : p ∣ q<VAR>r : R[X]<VAR>hr : q = p * r<GOAL>q = C a * p * (C a⁻¹ * r)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>t : Set α<GOAL>ν t = ∑' (g : G), ν (t ∩ g • s)
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H✝<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H✝ β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>hν : ν ≪ μ<VAR>t : Set α<VAR>H : ν.restrict t ≪ μ<GOAL>ν t = ∑' (g : G), ν (t ∩ g • s)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁴ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra A K<VAR>inst✝⁸ : Algebra A L<VAR>inst✝⁷ : IsFractionRing A K<VAR>C : Type u_7<VAR>inst✝⁶ : CommRing C<VAR>inst✝⁵ : IsDomain C<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic A L<VAR>inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0<VAR>z : L<VAR>x : ↥(integralClosure A L)<VAR>y : A<VAR>hy : y ≠ 0<VAR>hxy : z * (algebraMap A L) y = ↑x<VAR>h : (algebraMap A C) y = 0<GOAL>(algebraMap A L) y = 0
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁴ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra A K<VAR>inst✝⁸ : Algebra A L<VAR>inst✝⁷ : IsFractionRing A K<VAR>C : Type u_7<VAR>inst✝⁶ : CommRing C<VAR>inst✝⁵ : IsDomain C<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic A L<VAR>inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0<VAR>z : L<VAR>x : ↥(integralClosure A L)<VAR>y : A<VAR>hy : y ≠ 0<VAR>hxy : z * (algebraMap A L) y = ↑x<GOAL>z * (algebraMap C L) ((algebraMap A C) y) = (algebraMap C L) (mk' C ↑x ⋯)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁴ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝¹³ : CommRing A<VAR>inst✝¹² : IsDomain A<VAR>L : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra A K<VAR>inst✝⁸ : Algebra A L<VAR>inst✝⁷ : IsFractionRing A K<VAR>C : Type u_7<VAR>inst✝⁶ : CommRing C<VAR>inst✝⁵ : IsDomain C<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic A L<VAR>inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0<VAR>x y : C<VAR>h : (algebraMap C L) x = (algebraMap C L) y<GOAL>↑1 * x = ↑1 * y
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<GOAL>μ (limsup s atTop) = 1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<GOAL>μ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} = 1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<GOAL>{ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} =ᶠ[ae μ] Set.univ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : BorelSpace β<VAR>f : ι → Ω → β<VAR>i j : ι<VAR>s✝ : ι → Set Ω<VAR>s : ℕ → Set Ω<VAR>hsm : ∀ (n : ℕ), MeasurableSet (s n)<VAR>hs : iIndepSet s μ<VAR>hs' : ∑' (n : ℕ), μ (s n) = ⊤<VAR>this : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), (μ[(s (n + 1)).indicator 1|↑(filtrationOfSet hsm) n]) ω = (fun x => (μ (s (n + 1))).toReal) ω<GOAL>{ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} =ᶠ[ae μ] Set.univ