ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<VAR>hfg' : UniformCauchySeqOnFilter f' l (𝓝 x)<GOAL>∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<VAR>hfg' : TendstoUniformlyOnFilter (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (𝓝 x)<GOAL>∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<VAR>hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<GOAL>∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<VAR>hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<VAR>hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℚ<VAR>hqpos : 0 < q<VAR>hqε : ↑q < ε<GOAL>∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℚ<VAR>hqpos : 0 < q<VAR>hqε : ↑q < ε<VAR>hfg' : ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ↑q<GOAL>∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this✝ : l.NeBot<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℚ<VAR>hqpos : 0 < q<VAR>hqε : ↑q < ε<VAR>hfg' : ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ↑q<VAR>this : ∀ᶠ (x : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1) (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧ HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1) (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2<GOAL>∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this✝ : l.NeBot<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℚ<VAR>hqpos : 0 < q<VAR>hqε : ↑q < ε<VAR>hfg' : ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ↑q<VAR>this : ∀ᶠ (x : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1) (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧ HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1) (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2<VAR>a : ι × ι → Prop<VAR>b : ∀ᶠ (x : ι × ι) in l ×ˢ l, a x<VAR>c : E → Prop<VAR>d : ∀ᶠ (y : E) in 𝓝 x, c y<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hr' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x r → c x_1<VAR>n : ι × ι<VAR>hn : a n<VAR>y : E<VAR>hy : (fun e => Metric.ball x r e) y<VAR>hyz' : ¬x = y<VAR>hyz : 0 < ‖y - x‖<VAR>e : ∀ {x : ι × ι}, a x → ∀ {y : E}, c y → ‖f' x.1 y - f' x.2 y‖ < ↑q ∧ HasFDerivAt (f x.1) (f' x.1 y) y ∧ HasFDerivAt (f x.2) (f' x.2 y) y<GOAL>‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ ≤ ↑q * ‖y - x‖
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>h : Function.Surjective ⇑f<VAR>x : ↑↑(Spec S).toPresheafedSpace<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap (Spec.map f) x)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>h : Function.Surjective ⇑f<VAR>x : ↑↑(Spec S).toPresheafedSpace<VAR>this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap (Spec.map f) x)
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>h : Function.Surjective ⇑f<VAR>x : ↑↑(Spec S).toPresheafedSpace<VAR>this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso<GOAL>RingHom.toMorphismProperty (fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f) (CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap f) x).asIdeal x.asIdeal f ⋯))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : ℝ<VAR>x : G<GOAL>(compLpL 2 μ (toSpanSingleton ℝ (c • x))) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) = c • (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : IsEmpty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖1‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : IsEmpty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ ‖1‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : IsEmpty ι<GOAL>‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>0 ⨳ a = 0
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>he : e ≠ 0<VAR>this : NeZero e := { out := he }<GOAL>Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>he : e ≠ 0<VAR>this✝ : NeZero e := { out := he }<VAR>this : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ 0)) = (e - 0) • Module.rank (R ⧸ p) (S ⧸ P)<GOAL>Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>he : e ≠ 0<VAR>this✝ : NeZero e := { out := he }<VAR>this : Module.rank (R ⧸ p) ↥⊤ = e • Module.rank (R ⧸ p) (S ⧸ P)<GOAL>Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m : ℤ<VAR>n : ℕ<GOAL>fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m : ℤ<GOAL>fract (↑m / ↑0) = ↑(m % ↑0) / ↑0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : n > 0<GOAL>fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<GOAL>fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<VAR>m₀ : ℕ<GOAL>fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<VAR>m₀ : ℕ<GOAL>fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<VAR>m₀ : ℕ<VAR>q : ℤ := ⌈↑m₀ / ↑n⌉<VAR>m₁ : ℤ := q * ↑n - ↑m₀<GOAL>fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<VAR>m₀ : ℕ<VAR>q : ℤ := ⌈↑m₀ / ↑n⌉<VAR>m₁ : ℤ := q * ↑n - ↑m₀<VAR>hm₁ : 0 ≤ m₁<GOAL>fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<VAR>m₀ : ℕ<VAR>q : ℤ := ⌈↑m₀ / ↑n⌉<VAR>m₁ : ℤ := q * ↑n - ↑m₀<VAR>hm₁ : 0 ≤ m₁<GOAL>fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b : k<VAR>n : ℕ<VAR>hn : 0 < ↑n<VAR>this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n<VAR>m₀ : ℕ<VAR>q : ℤ := ⌈↑m₀ / ↑n⌉<VAR>m₁ : ℤ := q * ↑n - ↑m₀<VAR>hm₁ : 0 ≤ m₁<GOAL>↑(m₁ % ↑n) / ↑n = ↑(-↑m₀ % ↑n) / ↑n
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k x : ℕ<GOAL>x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<GOAL>IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<GOAL>(∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)) → IsClosedMap f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>IsClosed (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>∀ (i : ι), IsClosed (Subtype.val ⁻¹' (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsClosed s<VAR>i : ι<GOAL>IsClosed (Subtype.val ⁻¹' (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsClosed s<VAR>i : ι<VAR>e_1✝ : ↥(U i) = ↑(U i).carrier<GOAL>Subtype.val ⁻¹' (f '' s) = (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' sᶜ)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsClosed s<VAR>i : ι<VAR>e_1✝ : ↥(U i) = ↑(U i).carrier<VAR>x : β<VAR>hx : x ∈ U i<GOAL>⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' s) ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' sᶜ)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsClosed s<VAR>i : ι<VAR>e_1✝ : ↥(U i) = ↑(U i).carrier<VAR>x : β<VAR>hx : x ∈ U i<GOAL>(∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<GOAL>cs.IsReflection t⁻¹
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : ι → E<VAR>inst✝ : Fintype ι'<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>e : ι ≃ ι'<VAR>x : E<VAR>i' : ι'<GOAL>(b.reindex e).repr x i' = b.repr x (e.symm i')
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>h : ∃ n a, a ∈ f n<GOAL>(rfindOpt f).Dom
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>h : ∃ n a, a ∈ f n<VAR>h' : ∃ n, (f n).isSome = true<GOAL>(rfindOpt f).Dom
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>h : ∃ n a, a ∈ f n<VAR>h' : ∃ n, (f n).isSome = true<VAR>s : (f (Nat.find h')).isSome = true<GOAL>(rfindOpt f).Dom
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>h : ∃ n a, a ∈ f n<VAR>h' : ∃ n, (f n).isSome = true<VAR>s : (f (Nat.find h')).isSome = true<VAR>fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom<GOAL>(rfindOpt f).Dom
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>h : ∃ n a, a ∈ f n<VAR>h' : ∃ n, (f n).isSome = true<VAR>s : (f (Nat.find h')).isSome = true<VAR>fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom<GOAL>((fun b => (fun n => ↑(f n)) ((rfind fun n => ↑(Option.some (f n).isSome)).get b)) fd).Dom
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>h : ∃ n a, a ∈ f n<VAR>h' : ∃ n, (f n).isSome = true<VAR>s : (f (Nat.find h')).isSome = true<VAR>fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom<VAR>this : true ∈ ↑(Option.some (f ((rfind fun n => ↑(Option.some (f n).isSome)).get fd)).isSome)<GOAL>((fun b => (fun n => ↑(f n)) ((rfind fun n => ↑(Option.some (f n).isSome)).get b)) fd).Dom
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>((↑s).drop n).head = Computation.pure (s.get? n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<GOAL>↑s.card * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<GOAL>s.card • ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<GOAL>σ 0 = {0}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<GOAL>σ 0 ⊆ {0}