ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<VAR>x : α<VAR>n : ι<VAR>hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t<VAR>hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)<GOAL>∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this✝ : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<VAR>x : α<VAR>n : ι<VAR>hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t<VAR>hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)<VAR>this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t<GOAL>∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this✝ : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<VAR>x : α<VAR>n : ι<VAR>hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t<VAR>hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)<VAR>this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t<VAR>m : ι<VAR>hm : (F n x, F m x) ∈ t ∧ (fun x_1 => (f x, F x_1 x)) m ∈ t<GOAL>∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<GOAL>f '' s ∪ f '' sᶜ = range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set α<VAR>t : Set β<GOAL>𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set α<VAR>t : Set β<GOAL>Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s.prod t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(map f (ν.withDensity (μ.rnDeriv ν))) s = ((map f ν).withDensity ((map f μ).rnDeriv (map f ν))) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ∫⁻ (x : α) in f ⁻¹' s, (map f μ).rnDeriv (map f ν) (f x) ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂ν, x ∈ f ⁻¹' s → μ.rnDeriv ν x = (map f μ).rnDeriv (map f ν) (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>h : ¬μ.HaveLebesgueDecomposition ν<GOAL>μ.singularPart ν = 0
<VAR>b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm<GOAL>discr ℚ = 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>l : α →₀ R<VAR>s : Finset α<VAR>hs : l ∈ supported R R ↑s<VAR>x : α<VAR>x✝ : x ∈ s<VAR>hxg : x ∉ l.support<GOAL>l x • v x = 0
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : OrderBot L<VAR>inst✝ : ContinuousSup L<VAR>hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))<GOAL>Tendsto (s.sup f) l (𝓝 (s.sup g))
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : OrderBot L<VAR>inst✝ : ContinuousSup L<VAR>hs : ∀ i ∈ ∅, Tendsto (f i) l (𝓝 (g i))<GOAL>Tendsto (∅.sup f) l (𝓝 (∅.sup g))
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : OrderBot L<VAR>inst✝ : ContinuousSup L<VAR>hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))<VAR>hne : s.Nonempty<GOAL>Tendsto (s.sup f) l (𝓝 (s.sup g))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>r : R<GOAL>(liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>inst✝¹ : Pow M ℕ+<VAR>inst✝ : PNatPowAssoc M<VAR>k m n : ℕ+<VAR>x : M<GOAL>x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>y : L₂<VAR>hy : y ∈ f.range<GOAL>∃ a, f.rangeRestrict a = ⟨y, hy⟩
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>y : L₂<VAR>hy✝ : y ∈ f.range<VAR>hy : ∃ y_1, f y_1 = y<GOAL>∃ a, f.rangeRestrict a = ⟨y, hy✝⟩
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>x : L<VAR>hy : f x ∈ f.range<GOAL>∃ a, f.rangeRestrict a = ⟨f x, hy⟩
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>x : L<VAR>hy : f x ∈ f.range<GOAL>f.rangeRestrict x = ⟨f x, hy⟩
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>comp 1 p = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>η : ℝ≥0∞<VAR>hη_pos : 0 < η<VAR>hη : ∀ (f g : α → β), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>η : ℝ≥0∞<VAR>hη_pos : 0 < η<VAR>hη : ∀ (f g : α → β), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε<VAR>hη_top : ¬η = ⊤<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>η : ℝ≥0∞<VAR>hη_pos : 0 < η<VAR>hη : ∀ (f g : α → β), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε<VAR>hη_top : ¬η = ⊤<VAR>s : Set α<VAR>hμs : s ∈ μ.cofinite<VAR>hsm : MeasurableSet s<VAR>hfs : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ η<VAR>hgs : ∀ (i : ι), eLpNorm (s.indicator (g i)) p μ ≤ η<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>η : ℝ≥0∞<VAR>hη_pos : 0 < η<VAR>hη : ∀ (f g : α → β), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε<VAR>hη_top : ¬η = ⊤<VAR>s : Set α<VAR>hμs : s ∈ μ.cofinite<VAR>hsm : MeasurableSet s<VAR>hfs : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ η<VAR>hgs : ∀ (i : ι), eLpNorm (s.indicator (g i)) p μ ≤ η<VAR>i : ι<GOAL>eLpNorm (sᶜᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>η : ℝ≥0∞<VAR>hη_pos : 0 < η<VAR>hη : ∀ (f g : α → β), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε<VAR>hη_top : ¬η = ⊤<VAR>s : Set α<VAR>hμs : s ∈ μ.cofinite<VAR>hsm : MeasurableSet s<VAR>hfs : ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ η<VAR>hgs : ∀ (i : ι), eLpNorm (s.indicator (g i)) p μ ≤ η<VAR>i : ι<VAR>η_cast : ↑η.toNNReal = η<GOAL>eLpNorm (sᶜᶜ.indicator ((f + g) i)) p μ ≤ ↑ε
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<GOAL>ContMDiffOn 𝓘(𝕜, E) I n (↑(extChartAt I x).symm) (extChartAt I x).target
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<GOAL>(extChartAt I x).target = ↑I '' (chartAt H x).target
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)), IsIntegral F α
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : F), IsIntegral F ((algebraMap F ↥(solvableByRad F E)) α)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α β : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F β → IsIntegral F (α + β)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F (-α)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α β : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F β → IsIntegral F (α * β)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)), IsIntegral F α → IsIntegral F α⁻¹
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<GOAL>∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → IsIntegral F (α ^ n) → IsIntegral F α
<VAR>α : Type u_1<VAR>s t : Set α<VAR>x : α × α<VAR>a : α<GOAL>s.offDiag = ∅ ↔ s.Subsingleton
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Matrix V V α<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i j : V<VAR>hij : (fun i j => A i j = 1) i j<GOAL>A j i = 1
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hsum : Summable fun x => ‖f x‖<GOAL>(1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hsum : Summable fun x => ‖f x‖<GOAL>(1 - f p)⁻¹ = ∑' (e : ℕ), f p ^ e
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hsum : Summable fun x => ‖f x‖<GOAL>Summable fun n => f p ^ n
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hsum : Summable fun x => ‖f x‖<GOAL>Summable fun a => ‖f p ^ a‖
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝ : f.IsCountablyGenerated<VAR>u : ℕ → α<VAR>hx : (f ⊓ map u atTop).NeBot<GOAL>∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝ : f.IsCountablyGenerated<VAR>u : ℕ → α<VAR>hx : (comap u f ⊓ atTop).NeBot<GOAL>∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝ : f.IsCountablyGenerated<VAR>u : ℕ → α<VAR>hx : (comap u f ⊓ atTop).NeBot<VAR>φ : ℕ → ℕ<VAR>hφ : Tendsto φ atTop (comap u f ⊓ atTop)<GOAL>∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝ : f.IsCountablyGenerated<VAR>u : ℕ → α<VAR>hx : (comap u f ⊓ atTop).NeBot<VAR>φ : ℕ → ℕ<VAR>hφ : Tendsto (u ∘ φ) atTop f ∧ Tendsto φ atTop atTop<GOAL>∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝ : f.IsCountablyGenerated<VAR>u : ℕ → α<VAR>hx : (comap u f ⊓ atTop).NeBot<VAR>φ : ℕ → ℕ<VAR>hφ : Tendsto (u ∘ φ) atTop f ∧ Tendsto φ atTop atTop<VAR>ψ : ℕ → ℕ<VAR>hψ : StrictMono ψ<VAR>hψφ : StrictMono (φ ∘ ψ)<GOAL>∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>e : A ≅ B<GOAL>e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 A.obj₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>𝓤 α = comap (fun x => x.1⁻¹ * x.2) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>comap (unop ∘ (fun x => x.2 / x.1) ∘ fun p => (op p.1, op p.2)) (𝓝 1) = comap (fun x => x.1⁻¹ * x.2) (𝓝 1)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ≥0∞<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U : Comonad C<VAR>X Y x✝ : Cokleisli U<VAR>f : X ⟶ Y<VAR>g : Y ⟶ x✝<GOAL>U.δ.app X ≫ U.map (U.δ.app X ≫ U.map f ≫ g) = (U.δ.app X ≫ U.map f) ≫ U.δ.app Y ≫ U.map g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U : Comonad C<VAR>X Y x✝ : Cokleisli U<VAR>f : X ⟶ Y<VAR>g : Y ⟶ x✝<GOAL>((U.δ.app X ≫ U.map (U.δ.app X)) ≫ U.map (U.map f)) ≫ U.map g = ((U.δ.app X ≫ U.map f) ≫ U.δ.app Y) ≫ U.map g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U : Comonad C<VAR>X Y x✝ : Cokleisli U<VAR>f : X ⟶ Y<VAR>g : Y ⟶ x✝<GOAL>((U.δ.app X ≫ U.δ.app (U.obj X)) ≫ U.map (U.map f)) ≫ U.map g = ((U.δ.app X ≫ U.map f) ≫ U.δ.app Y) ≫ U.map g
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<VAR>h : r > 0<GOAL>j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<VAR>h : r > 0<VAR>h✝ : ↑⌊(↑j + 1) / r⌋ * r ≤ ↑j<GOAL>j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<VAR>h : r > 0<VAR>h✝ : ↑⌊(↑j + 1) / r⌋ * r > ↑j<GOAL>j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup L<VAR>inst✝⁸ : Module R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : Fintype ιM<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<VAR>i : ℕ<GOAL>(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = ((toMatrix bₘ bₘ) (φ x)).charpoly.coeff i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<GOAL>(⋃₀ S).Nonempty ↔ ∃ s ∈ S, s.Nonempty
<VAR>a b✝ c d m n b : ℤ<VAR>hb : 0 < b<VAR>a✝ : ℕ<VAR>h : (ofNat a✝).toNat < b.toNat<GOAL>ofNat a✝ < b
<VAR>a b✝ c d m n b : ℤ<VAR>hb : 0 < b<VAR>a✝ : ℕ<VAR>h : -[a✝+1].toNat < b.toNat<GOAL>-[a✝+1] < b
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>hb : 0 < b<VAR>h : a < b<GOAL>a.toNat < b.toNat
<VAR>a✝ b✝ c d m n a b : ℤ<VAR>hb : 0 < b<VAR>h : a < b<GOAL>↑a.toNat < b
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>f : X →ᵇ ℝ≥0<VAR>x : X<GOAL>f x ≤ nndist 0 f
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>f : X →ᵇ ℝ≥0<VAR>x : X<GOAL>f x = nndist (0 x) (f x)
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x / y) ≤ f x + f y
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f (x * y⁻¹) ≤ f x + f y⁻¹
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<GOAL>Continuous (inducedMap A).snd
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<GOAL>∀ (a : ↑(inducedMap A).fst), ∀ ε > 0, ∀ᶠ (x : ↑(inducedMap A).fst) in 𝓝 a, dist ((inducedMap A).snd x) ((inducedMap A).snd a) < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>ε : ℝ<VAR>ε_pos : ε > 0<GOAL>∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 ⟨x, hx⟩, dist ((inducedMap A).snd x_1) ((inducedMap A).snd ⟨x, hx⟩) < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>n : ℕ<VAR>hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε<GOAL>∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 ⟨x, hx⟩, dist ((inducedMap A).snd x_1) ((inducedMap A).snd ⟨x, hx⟩) < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>n : ℕ<VAR>hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε<GOAL>∃ t, (∀ y ∈ t, dist ((inducedMap A).snd y) ((inducedMap A).snd ⟨x, hx⟩) < ε) ∧ IsOpen t ∧ ⟨x, hx⟩ ∈ t
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : DiscreteTopology β<VAR>hA : VanishingDiam A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>ε : ℝ<VAR>ε_pos : ε > 0<VAR>n : ℕ<VAR>hn : ∀ y ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε<GOAL>IsOpen (Subtype.val ⁻¹' cylinder x n)