ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x y z : L<VAR>hx : x ∈ H.normalizer<VAR>hy : ∃ y_1 ∈ Submodule.span R {x}, ∃ z ∈ H.toSubmodule, y_1 + z = y<VAR>hz : ∃ y ∈ Submodule.span R {x}, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z<GOAL>⁅y, z⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>u₁ : L<VAR>hu₁ : u₁ ∈ Submodule.span R {x}<VAR>v : L<VAR>hv : v ∈ H<VAR>u₂ : L<VAR>hu₂ : u₂ ∈ Submodule.span R {x}<VAR>w : L<VAR>hw : w ∈ H<GOAL>⁅u₁ + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>v : L<VAR>hv : v ∈ H<VAR>u₂ : L<VAR>hu₂ : u₂ ∈ Submodule.span R {x}<VAR>w : L<VAR>hw : w ∈ H<VAR>t : R<VAR>hu₁ : t • x ∈ Submodule.span R {x}<GOAL>⁅t • x + v, u₂ + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>v : L<VAR>hv : v ∈ H<VAR>w : L<VAR>hw : w ∈ H<VAR>t : R<VAR>hu₁ : t • x ∈ Submodule.span R {x}<VAR>s : R<VAR>hu₂ : s • x ∈ Submodule.span R {x}<GOAL>⁅t • x + v, s • x + w⁆ ∈ Submodule.span R {x} ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>v : L<VAR>hv : v ∈ H<VAR>w : L<VAR>hw : w ∈ H<VAR>t : R<VAR>hu₁ : t • x ∈ Submodule.span R {x}<VAR>s : R<VAR>hu₂ : s • x ∈ Submodule.span R {x}<GOAL>⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>v : L<VAR>hv : v ∈ H<VAR>w : L<VAR>hw : w ∈ H<VAR>t : R<VAR>hu₁ : t • x ∈ Submodule.span R {x}<VAR>s : R<VAR>hu₂ : s • x ∈ Submodule.span R {x}<GOAL>s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>v : L<VAR>hv : v ∈ H<VAR>w : L<VAR>hw : w ∈ H<VAR>t : R<VAR>hu₁ : t • x ∈ Submodule.span R {x}<VAR>s : R<VAR>hu₂ : s • x ∈ Submodule.span R {x}<GOAL>⁅v, x⁆ ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>hx : x ∈ H.normalizer<VAR>v : L<VAR>hv : v ∈ H<VAR>w : L<VAR>hw : w ∈ H<VAR>t : R<VAR>hu₁ : t • x ∈ Submodule.span R {x}<VAR>s : R<VAR>hu₂ : s • x ∈ Submodule.span R {x}<GOAL>⁅x, w⁆ ∈ H
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>e e' : Trivialization F proj<VAR>h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'<GOAL>e.toPartialHomeomorph = e'.toPartialHomeomorph
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x : Z<VAR>e e' : Trivialization F proj<VAR>h : (fun e => e.toPretrivialization) e = (fun e => e.toPretrivialization) e'<GOAL>e.baseSet = e'.baseSet
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Semigroup α<VAR>x : Holor α ds₁<VAR>y : Holor α ds₂<VAR>z : Holor α ds₃<GOAL>HEq (x ⊗ y ⊗ z) (x ⊗ (y ⊗ z))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<GOAL>f =o[𝓝 b] g ↔ (f ∘ ⇑e) =o[𝓝 (e.symm b)] (g ∘ ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<GOAL>x.toReal = y.toReal ↔ x = y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>inst✝¹ : HasWidePushout B X f<VAR>inst✝ : PreservesColimit (wideSpan B X f) (forget C)<VAR>x : (forget C).obj (widePushout B X f)<GOAL>(∃ y, (head f) y = x) ∨ ∃ i y, (ι f i) y = x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>inst✝¹ : HasWidePushout B X f<VAR>inst✝ : PreservesColimit (wideSpan B X f) (forget C)<VAR>y : (forget C).obj ((wideSpan B X f).obj none)<GOAL>(∃ y_1, (head f) y_1 = (colimit.ι (wideSpan B X f) none) y) ∨ ∃ i y_1, (ι f i) y_1 = (colimit.ι (wideSpan B X f) none) y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>inst✝¹ : HasWidePushout B X f<VAR>inst✝ : PreservesColimit (wideSpan B X f) (forget C)<VAR>j : α<VAR>y : (forget C).obj ((wideSpan B X f).obj (some j))<GOAL>(∃ y_1, (head f) y_1 = (colimit.ι (wideSpan B X f) (some j)) y) ∨ ∃ i y_1, (ι f i) y_1 = (colimit.ι (wideSpan B X f) (some j)) y
<VAR>a r x : ℝ<VAR>hx : 0 ≤ x<GOAL>gammaPDF a r x = ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>f_lim : α → E<VAR>h_f_lim_meas : StronglyMeasurable f_lim<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>f_lim : α → E<VAR>h_f_lim_meas : StronglyMeasurable f_lim<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>h_tendsto' : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N<VAR>f_lim : α → E<VAR>h_f_lim_meas : StronglyMeasurable f_lim<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>h_tendsto' : Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>h_ℒp_lim : Memℒp f_lim p μ<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
<VAR>a b c d : Ordinal.{u}<VAR>h₁ : a ≤ b<VAR>h₂ : 0 ≤ c<GOAL>a ⨳ c ≤ b ⨳ c
<VAR>a b c d : Ordinal.{u}<VAR>h₁ : a ≤ b<VAR>h₂ : 0 ≤ c<GOAL>c ⨳ a ≤ c ⨳ b
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>↑m * ↑(↑m)⁻¹.val = 1
<VAR>m : ℕ<VAR>hmn : m.Coprime 0<GOAL>↑m * ↑(↑m)⁻¹.val = 1
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<VAR>hn : n ≠ 0<GOAL>↑m * ↑(↑m)⁻¹.val = 1
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<VAR>hn : n ≠ 0<VAR>this : NeZero n<GOAL>↑m * ↑(↑m)⁻¹.val = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁵ : Countable ι✝<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f✝ g : α → β<VAR>M : Type u_5<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>ι : Type u_6<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ<GOAL>AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i ≤ g i<VAR>i : ι<VAR>this : f i ≤ g i<GOAL>Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Zero α<VAR>inst✝ : One α<VAR>i✝ j✝ : V<GOAL>(adjMatrix α G)ᵀ i✝ j✝ = adjMatrix α G i✝ j✝
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L : Ideal R<VAR>x : R<VAR>I J : Ideal R<GOAL>(∀ {zI : R}, zI ∈ I → zI ∈ span {x} * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb✝ : ι' → Set β<VAR>f : α → β<VAR>p : ι → Prop<VAR>sb : ι → Set β<VAR>hla : la.HasBasis p sa<VAR>hlb : lb.HasBasis p sb<VAR>h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j<GOAL>(la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb✝ : ι' → Set β<VAR>f : α → β<VAR>p : ι → Prop<VAR>sb : ι → Set β<VAR>hla : la.HasBasis p sa<VAR>hlb : lb.HasBasis p sb<VAR>h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j<GOAL>∀ (t : Set (α × β)), (∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) ↔ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this : UpgradedPolishSpace γ := upgradePolishSpace γ<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝¹ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this✝ : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>this : ∀ (p : A), ∃ q, f '' ↑(↑p).1 ⊆ q ∧ Disjoint (f '' ↑(↑p).2) q ∧ MeasurableSet q<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<VAR>E : ↑b → Set β := fun s => closure (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<VAR>E : ↑b → Set β := fun s => closure (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩<VAR>u : ℕ → ℝ<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<VAR>E : ↑b → Set β := fun s => closure (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩<VAR>u : ℕ → ℝ<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>F : ℕ → Set β := fun n => ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s<GOAL>MeasurableSet (range f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<VAR>E : ↑b → Set β := fun s => closure (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩<VAR>u : ℕ → ℝ<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>F : ℕ → Set β := fun n => ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s<GOAL>range f = ⋂ n, F n
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<VAR>E : ↑b → Set β := fun s => closure (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩<VAR>u : ℕ → ℝ<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>F : ℕ → Set β := fun n => ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s<GOAL>range f ⊆ ⋂ n, F n
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>β : Type u_4<VAR>inst✝⁵ : TopologicalSpace γ<VAR>inst✝⁴ : PolishSpace γ<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>f : γ → β<VAR>f_cont : Continuous f<VAR>f_inj : Injective f<VAR>this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ<VAR>b : Set (Set γ)<VAR>b_count : b.Countable<VAR>b_nonempty : ∅ ∉ b<VAR>hb : IsTopologicalBasis b<VAR>this : Encodable ↑b<VAR>A : Type u_3 := { p // Disjoint ↑p.1 ↑p.2 }<VAR>q : A → Set β<VAR>hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p<VAR>hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)<VAR>q_meas : ∀ (p : A), MeasurableSet (q p)<VAR>E : ↑b → Set β := fun s => closure (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩<VAR>u : ℕ → ℝ<VAR>u_anti : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>F : ℕ → Set β := fun n => ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s<GOAL>⋂ n, F n ⊆ range f
<VAR>m n a b c d : ℕ<VAR>h : a ≤ b<GOAL>a ≡ b [MOD n] ↔ n ∣ b - a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<VAR>g : G<VAR>hg : g ∈ stabilizer G a<GOAL>g ∈ stabilizer G B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<VAR>g : G<VAR>hg : g ∈ stabilizer G a<GOAL>¬Disjoint (g • B) B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<VAR>g : G<VAR>hg : g ∈ stabilizer G a<GOAL>∃ x ∈ g • B, x ∈ B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<VAR>g : G<VAR>hg : g ∈ stabilizer G a<GOAL>a ∈ g • B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>a : X<VAR>ha : a ∈ B<VAR>g : G<VAR>hg : g ∈ stabilizer G a<GOAL>a ∈ B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝³ : DecidableRel r<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTotal α r<VAR>s : Finset α<GOAL>(↑(sort r s)).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝³ : DecidableRel r<VAR>inst✝² : IsTrans α r<VAR>inst✝¹ : IsAntisymm α r<VAR>inst✝ : IsTotal α r<VAR>s : Finset α<GOAL>s.val.Nodup
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<GOAL>LinearMap.range S.f = LinearMap.ker S.g
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : k ≠ 0<VAR>x✝ : E<GOAL>x✝ ∈ k • p.ball 0 r ↔ x✝ ∈ p.ball 0 (‖k‖ * r)