ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g g' : G<GOAL>g • (∑ c ∈ s, l c • (toFun G F) c) (g⁻¹ * g') = (∑ c ∈ s, l c • (toFun G F) c) g'
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : a < c<VAR>h : b ≤ c<GOAL>a < min b c
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : a < c<VAR>h : b > c<GOAL>a < min b c
<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'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<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'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContinuousWithinAt f s x ∧ ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<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>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p μ) → UnifTight f p μ<VAR>f : Fin (n + 1) → α → β<VAR>hfLp : ∀ (i : Fin (n + 1)), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<VAR>g : Fin n → α → β := fun k => f ↑↑k<VAR>hgLp : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>S : Set α<VAR>hμS : μ S ≠ ⊤<VAR>hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f 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>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), Memℒp (f i) p μ) → UnifTight f p μ<VAR>f : Fin (n + 1) → α → β<VAR>hfLp : ∀ (i : Fin (n + 1)), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<VAR>g : Fin n → α → β := fun k => f ↑↑k<VAR>hgLp : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>S : Set α<VAR>hμS : μ S ≠ ⊤<VAR>hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε<VAR>s : Set α<VAR>left✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hfε : eLpNorm (sᶜ.indicator (f ↑n)) p μ < ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>a₀ : α<VAR>l : Filter α<VAR>h : pure a₀ ≤ l<VAR>b : α<GOAL>𝓝 b = update pure a₀ l b
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>a₀ : α<VAR>l : Filter α<VAR>h : pure a₀ ≤ l<VAR>b a : α<VAR>s : Set α<VAR>hs : s ∈ update pure a₀ l a<GOAL>∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>l : Filter α<VAR>b a : α<VAR>s : Set α<VAR>h : pure a ≤ l<VAR>hs : s ∈ update pure a l a<GOAL>∀ᶠ (y : α) in update pure a l a, s ∈ update pure a l y
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>a₀ : α<VAR>l : Filter α<VAR>h : pure a₀ ≤ l<VAR>b a : α<VAR>s : Set α<VAR>hs : s ∈ update pure a₀ l a<VAR>ha : a ≠ a₀<GOAL>∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<GOAL>∀ (t : Set α), (⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<GOAL>(⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<VAR>h : t = ∅<GOAL>(⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t<VAR>t : Set α<VAR>h : t.Nonempty<GOAL>(⨆ (_ : (t ∩ s).Nonempty), m (t ∩ s)) + ⨆ (_ : (t \ s).Nonempty), m (t \ s) ≤ ⨆ (_ : t.Nonempty), m t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<GOAL>AffineIndependent k ![p₁, p₂, p₃]
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<VAR>ha : AffineIndependent k fun x => ![p₁, p₂, p₃] ↑x<GOAL>AffineIndependent k ![p₁, p₂, p₃]
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<VAR>ha : AffineIndependent k fun x => ![p₁, p₂, p₃] ↑x<GOAL>![p₁, p₂, p₃] 2 ∉ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<VAR>ha : AffineIndependent k fun x => ![p₁, p₂, p₃] ↑x<VAR>h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<VAR>ha : AffineIndependent k fun x => ![p₁, p₂, p₃] ↑x<VAR>h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})<GOAL>affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2}) ≤ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<VAR>ha : AffineIndependent k fun x => ![p₁, p₂, p₃] ↑x<VAR>h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})<GOAL>∀ x ∈ {x | x ≠ 2}, ![p₁, p₂, p₃] x ∈ ↑s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>hp0s1 : p0 ∈ affineSpan k (p '' s1)<VAR>hp0s2 : p0 ∈ affineSpan k (p '' s2)<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>hp0s1 : p0 ∈ affineSpan k (Set.range fun x => p ↑x)<VAR>hp0s2 : p0 ∈ affineSpan k (Set.range fun x => p ↑x)<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>hp0s1 : ∃ fs, ↑fs ⊆ s1 ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w<VAR>hp0s2 : ∃ fs, ↑fs ⊆ s2 ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>ha : ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k), ∑ i ∈ s1, w1 i = 1 → ∑ i ∈ s2, w2 i = 1 → (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<VAR>ha : (↑fs1).indicator w1 = (↑fs2).indicator w2<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<VAR>ha : (↑fs1).indicator w1 = (↑fs2).indicator w2<VAR>hnz : ∑ i ∈ fs1, w1 i ≠ 0<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<VAR>ha : (↑fs1).indicator w1 = (↑fs2).indicator w2<VAR>hnz : ∑ i ∈ fs1, w1 i ≠ 0<VAR>i : ι<VAR>hifs1 : i ∈ fs1<VAR>hinz : w1 i ≠ 0<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<VAR>ha : (↑fs1).indicator w1 = (↑fs2).indicator w2<VAR>hnz : ∑ i ∈ fs1, w1 i ≠ 0<VAR>i : ι<VAR>hifs1 : i ∈ fs1<VAR>hinz : (↑fs2).indicator w2 i ≠ 0<GOAL>∃ i, i ∈ s1 ∩ s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>inst✝ : Nontrivial k<VAR>p : ι → P<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>fs1 : Finset ι<VAR>hfs1 : ↑fs1 ⊆ s1<VAR>w1 : ι → k<VAR>hw1 : ∑ i ∈ fs1, w1 i = 1<VAR>hp0s1 : p0 = (affineCombination k fs1 p) w1<VAR>fs2 : Finset ι<VAR>hfs2 : ↑fs2 ⊆ s2<VAR>w2 : ι → k<VAR>hw2 : ∑ i ∈ fs2, w2 i = 1<VAR>hp0s2 : p0 = (affineCombination k fs2 p) w2<VAR>ha : (↑fs1).indicator w1 = (↑fs2).indicator w2<VAR>hnz : ∑ i ∈ fs1, w1 i ≠ 0<VAR>i : ι<VAR>hifs1 : i ∈ fs1<VAR>hinz : (↑fs2).indicator w2 i ≠ 0<GOAL>i ∈ s2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>u : H →L[𝕜] K<GOAL>(∀ (x : H), ‖u x‖ = ‖x‖) ↔ (adjoint u).comp u = 1
<VAR>c : ℝ<GOAL>∫ (x : ℝ) in Ioi c, rexp (-x) = rexp (-c)
<VAR>x y : ℝ<GOAL>Tendsto log (𝓝[≠] 0) atBot
<VAR>x y : ℝ<GOAL>Tendsto (fun x => log |x|) (𝓝[≠] 0) atBot
<VAR>x y : ℝ<GOAL>Tendsto log (𝓝[>] 0) atBot
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ inst✝ : IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(fun ω => (((condexpKernel μ m) ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ inst✝ : IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>h : (fun a => (((condDistrib id id μ) (id a)) s).toReal) =ᶠ[ae μ] μ[(id ⁻¹' s).indicator fun ω => 1|MeasurableSpace.comap id (m ⊓ mΩ)]<GOAL>(fun ω => (((condexpKernel μ m) ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ inst✝ : IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>h : (fun a => (((condDistrib id id μ) a) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]<GOAL>(fun ω => (((condexpKernel μ m) ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ inst✝ : IsFiniteMeasure μ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>h : (fun a => (((condDistrib id id μ) a) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]<GOAL>(fun ω => (((condDistrib id id μ) (id ω)) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m ⊓ mΩ]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Subsingleton A<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<VAR>this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<VAR>this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim<GOAL>∑ x ∈ Finset.range pb.dim, ((pb.basis.constr A) fun i => y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff x • pb.gen ^ x) = ∑ i ∈ Finset.range pb.dim, (f %ₘ minpoly A pb.gen).coeff i • y ^ i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<VAR>this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim<VAR>i : ℕ<VAR>hi : i ∈ Finset.range pb.dim<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) = (f %ₘ minpoly A pb.gen).coeff i • y ^ i