ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n m : ℕ<VAR>hm : NeZero m<VAR>h : n ∣ m<VAR>x : ℕ<VAR>hx : x.Coprime n<VAR>ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors<GOAL>∃ k, (x + k * n).Coprime m
<VAR>n m : ℕ<VAR>hm : NeZero m<VAR>h : n ∣ m<VAR>x : ℕ<VAR>hx : x.Coprime n<VAR>ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors<GOAL>(x + ps.prod id * n).Coprime m
<VAR>n m : ℕ<VAR>hm : NeZero m<VAR>h : n ∣ m<VAR>x : ℕ<VAR>hx : x.Coprime n<VAR>ps : Finset ℕ := Finset.filter (fun p => ¬p ∣ x) m.primeFactors<GOAL>∀ (k : ℕ), Nat.Prime k → k ∣ x + ps.prod id * n → ¬k ∣ m
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g₁ g₂ : G<GOAL>(hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g₁ g₂ : G<GOAL>(hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ g₁⁻¹ * g₂ ∈ K
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<GOAL>f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<GOAL>(f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))) = Y.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<GOAL>f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) = f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (homOfLE ⋯).op
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : F →ₛₗᵢ[σ₂₃] G<VAR>g : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖(f.toContinuousLinearMap.comp g) x‖ = ‖g x‖
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>hgi : IntegrableOn g k volume<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>hgi : IntegrableOn g k volume<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k<VAR>hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k<VAR>hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k<VAR>hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<VAR>hsub : [[c, d]] ⊆ k<VAR>hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<VAR>hsub : [[c, d]] ⊆ k<VAR>hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<VAR>hsub : [[c, d]] ⊆ k<VAR>hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hg_ae : ∀ᵐ (x : ℝ) ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<VAR>hsub : [[c, d]] ⊆ k<VAR>hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hg_ae : ∀ᵐ (x : ℝ) ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hsub' : Ι c d ⊆ k<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<VAR>hsub : [[c, d]] ⊆ k<VAR>hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hg_ae : ∀ᵐ (x : ℝ) ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hsub' : Ι c d ⊆ k<VAR>hfi : IntervalIntegrable (deriv f) volume c d<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>g : ℝ → F<VAR>k : Set ℝ<VAR>l : Filter ℝ<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : TendstoIxxClass Icc l l<VAR>hl : k ∈ l<VAR>hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x<VAR>hf : Tendsto (fun x => ‖f x‖) l atTop<VAR>hfg : deriv f =O[l] g<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>s : Set ℝ<VAR>hsl : s ∈ l<VAR>hgi : IntegrableOn (fun x => C * ‖g x‖) k volume<VAR>c : ℝ<VAR>hc : c ∈ s<VAR>d : ℝ<VAR>hd : d ∈ s<VAR>hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖<VAR>hsub : [[c, d]] ⊆ k<VAR>hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z<VAR>hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hg_ae : ∀ᵐ (x : ℝ) ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖<VAR>hsub' : Ι c d ⊆ k<VAR>hfi : IntervalIntegrable (deriv f) volume c d<GOAL>‖f d‖ - ‖f c‖ ≤ ∫ (y : ℝ) in k, C * ‖g y‖
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : PartialOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>hn : 0 < a<VAR>hm : 1 < b<GOAL>a < a * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : PartialOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>hn : 0 < a<VAR>hm : 1 < b<GOAL>a = a * 1
<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>rexp (-π * t) < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>∑' (n : ℕ), C * r ^ n ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>C * (1 - r)⁻¹ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<GOAL>1 - r ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>round x = ⌊x + 1 / 2⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>(if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>hx : fract x < 1 / 2<GOAL>(if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>hx : 1 / 2 ≤ fract x<GOAL>(if fract x < 1 / 2 then ⌊x⌋ else ⌈x⌉) = ⌊x + 1 / 2⌋
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>ht : TopologicalSpace α<VAR>h : PolishSpace α<GOAL>CompleteSpace α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>ht : TopologicalSpace α<VAR>h : PolishSpace α<GOAL>polishSpaceMetric α = ⋯.choose
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Iio a ⊆ Iio b ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : Iio a ⊆ Iio b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : Iio a ⊆ Iio b<VAR>ab : ¬a ≤ b<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>c : Set (Set α)<VAR>hs : IsCompact s<VAR>hc₁ : ∀ t ∈ c, IsOpen t<VAR>hc₂ : s ⊆ ⋃₀ c<GOAL>∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>c : Set (Set α)<VAR>hs : IsCompact s<VAR>hc₁ : ∀ t ∈ c, IsOpen t<VAR>hc₂ : s ⊆ ⋃ i, ↑i<GOAL>∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>inst✝³ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : SMulCommClass 𝕜 ℂ E<VAR>a : 𝕜<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hs : s ∈ (if hUcard : U.card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card) then equitabilise ⋯ else equitabilise ⋯).parts<GOAL>s.card = m ∨ s.card = m + 1
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<GOAL>∃ K', IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<GOAL>∃ K', IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<GOAL>∃ K', IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<GOAL>∃ K', IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<GOAL>∃ K', IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<GOAL>∃ K', IsEngelian R ↥K' ∧ K < K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<GOAL>IsEngelian R ↥K'
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule (↥K') M<VAR>_i4 : LieModule R (↥K') M<VAR>h : ∀ (x : ↥K'), _root_.IsNilpotent ((toEnd R (↥K') M) x)<GOAL>LieModule.IsNilpotent R (↥K') M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule (↥K') M<VAR>_i4 : LieModule R (↥K') M<VAR>h : ∀ (x : ↥K'), _root_.IsNilpotent ((toEnd R (↥K') M) x)<VAR>I : LieIdeal R ↥K'<VAR>hI₁ : lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'<GOAL>LieModule.IsNilpotent R (↥K') M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule (↥K') M<VAR>_i4 : LieModule R (↥K') M<VAR>h : ∀ (x : ↥K'), _root_.IsNilpotent ((toEnd R (↥K') M) x)<VAR>I : LieIdeal R ↥K'<VAR>hI₁ : lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'<VAR>hI₂ : Submodule.span R {⟨x, hxK'⟩} ⊔ ↑I = ⊤<GOAL>LieModule.IsNilpotent R (↥K') M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule (↥K') M<VAR>_i4 : LieModule R (↥K') M<VAR>h : ∀ (x : ↥K'), _root_.IsNilpotent ((toEnd R (↥K') M) x)<VAR>I : LieIdeal R ↥K'<VAR>hI₁ : lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'<VAR>hI₂ : Submodule.span R {⟨x, hxK'⟩} ⊔ ↑I = ⊤<VAR>e : ↥K ≃ₗ⁅R⁆ ↥↑I<GOAL>LieModule.IsNilpotent R (↥K') M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>K : LieSubalgebra R L<VAR>hK₁ : IsEngelian R ↥K<VAR>hK₂ : K < K.normalizer<VAR>x : L<VAR>hx₁ : x ∈ K.normalizer<VAR>hx₂ : x ∉ K<VAR>K' : LieSubalgebra R L := let __src := Submodule.span R {x} ⊔ K.toSubmodule; { toSubmodule := __src, lie_mem' := ⋯ }<VAR>hxK' : x ∈ K'<VAR>hKK' : K ≤ K'<VAR>hK' : K' ≤ K.normalizer<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule (↥K') M<VAR>_i4 : LieModule R (↥K') M<VAR>h : ∀ (x : ↥K'), _root_.IsNilpotent ((toEnd R (↥K') M) x)<VAR>I : LieIdeal R ↥K'<VAR>hI₁ : lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'<VAR>hI₂ : Submodule.span R {⟨x, hxK'⟩} ⊔ ↑I = ⊤<VAR>e : ↥K ≃ₗ⁅R⁆ ↥↑I<VAR>hI₃ : IsEngelian R ↥↑I<GOAL>LieModule.IsNilpotent R (↥K') M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ≃ β<VAR>D : Set β<GOAL>(M.mapEquiv f).Dep D ↔ M.Dep (⇑f.symm '' D)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ≃ β<VAR>D : Set β<GOAL>(∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a✝ b : ι → ℝ<VAR>f : ℝ → E<VAR>a : ℝ<VAR>hfi : IntegrableOn f (Ioi a) μ<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Iic (b i)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))