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✝ : TopologicalSpace α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>u₂ : Set (β × β)<VAR>h₂ : u₂ ∈ 𝓤 β<VAR>hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂<VAR>u₂₁ : u₂ ○ u₂ ⊆ u₁<VAR>t : Set α<VAR>tx : t ∈ 𝓝[s] x<VAR>F : α → β<VAR>hFc : ContinuousWithinAt F s x<VAR>hF : ∀ y ∈ t, (f y, F y) ∈ u₂<VAR>A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂<VAR>B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂<VAR>C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
<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✝ : TopologicalSpace α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>u₂ : Set (β × β)<VAR>h₂ : u₂ ∈ 𝓤 β<VAR>hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂<VAR>u₂₁ : u₂ ○ u₂ ⊆ u₁<VAR>t : Set α<VAR>tx : t ∈ 𝓝[s] x<VAR>F : α → β<VAR>hFc : ContinuousWithinAt F s x<VAR>hF : ∀ y ∈ t, (f y, F y) ∈ u₂<VAR>A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂<VAR>B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂<VAR>C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁<VAR>this : (F x, f x) ∈ u₁<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>ι : Type u_3<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>r : ι ↪ M<VAR>c : ι → Dual R M<VAR>hfin : (range ⇑r).Finite<VAR>h_two : ∀ (i : ι), (c i) (r i) = 2<VAR>h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)<VAR>i j : ι<VAR>hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)<GOAL>i = j
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>ι : Type u_3<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>r : ι ↪ M<VAR>c : ι → Dual R M<VAR>hfin : (range ⇑r).Finite<VAR>h_two : ∀ (i : ι), (c i) (r i) = 2<VAR>h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)<VAR>i j : ι<VAR>hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)<GOAL>∀ (k : ι), (c i) (r k) = (c j) (r k)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>ι : Type u_3<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>r : ι ↪ M<VAR>c : ι → Dual R M<VAR>hfin : (range ⇑r).Finite<VAR>h_two : ∀ (i : ι), (c i) (r i) = 2<VAR>h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)<VAR>i j : ι<VAR>hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)<VAR>k : ι<GOAL>(c i) (r k) = (c j) (r k)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>motive : (m : ℕ) → m ≤ n → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯<VAR>self : motive n ⋯<VAR>smn : m + 1 ≤ n<VAR>mn : m ≤ n<GOAL>decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M × M'<GOAL>(chartAt H x.1).prod (chartAt H' x.2).toPartialEquiv ≫ I.prod I'.toPartialEquiv = ((chartAt H x.1).toPartialEquiv ≫ I.toPartialEquiv).prod ((chartAt H' x.2).toPartialEquiv ≫ I'.toPartialEquiv)
<VAR>x : ℝ*<GOAL>x⁻¹⁻¹.Infinitesimal ∧ 0 < x⁻¹⁻¹ ↔ x.Infinitesimal ∧ 0 < x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : n ∉ p.support<GOAL>p.content ∣ p.coeff n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.coeff n = 0<GOAL>p.content ∣ p.coeff n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : p.coeff n = 0<GOAL>p.content ∣ 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p q : Seminorm 𝕜 E<VAR>a b : ℝ≥0<VAR>hpq : p ≤ q<VAR>hab : a ≤ b<GOAL>a • p ≤ b • q
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p q : Seminorm 𝕜 E<VAR>a b : ℝ≥0<VAR>hpq : p ≤ q<VAR>hab : a ≤ b<GOAL>∀ (x : E), (a • p) x ≤ (b • q) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p q : Seminorm 𝕜 E<VAR>a b : ℝ≥0<VAR>hpq : p ≤ q<VAR>hab : a ≤ b<VAR>x : E<GOAL>(a • p) x ≤ (b • q) x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y : E<GOAL>∀ (r : ℝ), inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y : E<GOAL>(fun r => inner_ 𝕜 (↑r • x) y) = fun r => (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y : E<GOAL>Continuous fun r => inner_ 𝕜 (↑r • x) y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y : E<GOAL>Continuous fun r => (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y : E<VAR>X : ℚ<GOAL>((fun r => inner_ 𝕜 (↑r • x) y) ∘ Rat.cast) X = ((fun r => (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y) ∘ Rat.cast) X
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>p : P<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁ : p ∈ altitude t i₁<VAR>h₂ : p ∈ altitude t i₂<VAR>i₃ : Fin 3<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<GOAL>p = t.orthocenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>p : P<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₂ : p ∈ altitude t i₂<VAR>i₃ : Fin 3<VAR>h₁ : p ∈ mongePlane t i₃ i₂<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<GOAL>p = t.orthocenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>p : P<VAR>h₁₂ : i₁ ≠ i₂<VAR>i₃ : Fin 3<VAR>h₂ : p ∈ mongePlane t i₃ i₁<VAR>h₁ : p ∈ mongePlane t i₃ i₂<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<GOAL>p = t.orthocenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>p : P<VAR>h₁₂ : i₁ ≠ i₂<VAR>i₃ : Fin 3<VAR>h₂ : p ∈ mongePlane t i₃ i₁<VAR>h₁ : p ∈ mongePlane t i₃ i₂<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<GOAL>p = mongePoint t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>p : P<VAR>h₁₂ : i₁ ≠ i₂<VAR>i₃ : Fin 3<VAR>h₂ : p ∈ mongePlane t i₃ i₁<VAR>h₁ : p ∈ mongePlane t i₃ i₂<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁₃ : i₁ ≠ i₃<VAR>ha : ∀ (i : Fin 3), i₃ ≠ i → p ∈ mongePlane t i₃ i<GOAL>p = mongePoint t
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>‖Polynomial.eval a F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Ring T<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S T<VAR>inst✝⁵ : Algebra R T<VAR>inst✝⁴ : IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<VAR>i : m<VAR>k : n<VAR>j : m<VAR>k' : n<GOAL>(leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = blockDiagonal (fun x_1 => (leftMulMatrix b) x) (i, k) (j, k')
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Ring T<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S T<VAR>inst✝⁵ : Algebra R T<VAR>inst✝⁴ : IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<VAR>i : m<VAR>k : n<VAR>j : m<VAR>k' : n<GOAL>(leftMulMatrix b) (if (i, k).2 = (j, k').2 then (algebraMap S S) x else 0) (i, k).1 (j, k').1 = if (i, k).2 = (j, k').2 then (leftMulMatrix b) x (i, k).1 (j, k').1 else 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : finrank K V = 1<VAR>x : V<VAR>hx : x ≠ 0<VAR>y : V<GOAL>∃ c, c • x = y
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : finrank K V = 1<VAR>x : V<VAR>hx : x ≠ 0<VAR>y : V<VAR>this : span K {x} = ⊤<GOAL>∃ c, c • x = y
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : finrank K V = 1<VAR>x : V<VAR>hx : x ≠ 0<VAR>y : V<VAR>this✝ : span K {x} = ⊤<VAR>this : y ∈ span K {x}<GOAL>∃ c, c • x = y
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝¹ : Nontrivial L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>e : H = ⊥<GOAL>False
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝¹ : Nontrivial L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>e : H = ⊥<VAR>x : L<VAR>hx : x ≠ 0<GOAL>False
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝¹ : Nontrivial L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>e : H = ⊥<VAR>x : L<VAR>hx : x ≠ 0<VAR>this : x ∈ H.normalizer<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>s : Finset V<VAR>h : G.IsClique ↑s<GOAL>↑s.card ≤ G.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>hc : G.chromaticNumber = ⊤<GOAL>↑s.card ≤ G.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>hc : G.chromaticNumber ≠ ⊤<GOAL>↑s.card ≤ G.chromaticNumber
<VAR>a b : ℤ<GOAL>a.natAbs = b.natAbs ↔ Associated a b
<VAR>a b : ℤ<GOAL>a = b ∨ a = -b ↔ Associated a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>Nat.card ↑s = s.toFinset.card
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) ((proj i).comp Φ') x
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>((fun p => Φ p.1 - Φ p.2 - Φ' (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2) ↔ ∀ (i : ι), (fun p => Φ p.1 i - Φ p.2 i - ((proj i).comp Φ') (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<VAR>hBU : ⋃ n, F ∩ s n = F<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<VAR>hBU : ⋃ n, F ∩ s n = F<VAR>this : μ F = ⨆ n, μ (F ∩ s n)<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < ⨆ n, μ (F ∩ s n)<VAR>hBU : ⋃ n, F ∩ s n = F<VAR>this : μ F = ⨆ n, μ (F ∩ s n)<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < ⨆ n, μ (F ∩ s n)<VAR>hBU : ⋃ n, F ∩ s n = F<VAR>this : μ F = ⨆ n, μ (F ∩ s n)<VAR>n : ℕ<VAR>hn : r < μ (F ∩ s n)<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < ⨆ n, μ (F ∩ s n)<VAR>hBU : ⋃ n, F ∩ s n = F<VAR>this : μ F = ⨆ n, μ (F ∩ s n)<VAR>n : ℕ<VAR>hn : r < (μ.restrict (s n)) F<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>μ : Measure α<VAR>s : ℕ → Set α<VAR>h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet<VAR>hs : univ ⊆ ⋃ n, s n<VAR>hmono : Monotone s<VAR>F : Set α<VAR>hF : MeasurableSet F<VAR>r : ℝ≥0∞<VAR>hr : r < ⨆ n, μ (F ∩ s n)<VAR>hBU : ⋃ n, F ∩ s n = F<VAR>this : μ F = ⨆ n, μ (F ∩ s n)<VAR>n : ℕ<VAR>hn : r < (μ.restrict (s n)) F<VAR>K : Set α<VAR>KF : K ⊆ F<VAR>hKp : p K<VAR>hK : r < (μ.restrict (s n)) K<GOAL>∃ K ⊆ F, p K ∧ r < μ K
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>a b : α<GOAL>𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>a b : α<GOAL>((𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ ball b t) = (𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>a b : α<GOAL>Monotone fun s => {y | (y, a) ∈ s}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>a b : α<GOAL>Monotone (ball b)
<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>A : Type u_8<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module.Finite A (A ⊗[R] M)<VAR>inst✝ : Module.Free A (A ⊗[R] M)<VAR>x : ι → A<GOAL>Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) = ((tensorProduct R A M M ∘ₗ baseChange A φ) ((basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly
<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>A : Type u_8<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module.Finite A (A ⊗[R] M)<VAR>inst✝ : Module.Free A (A ⊗[R] M)<VAR>x : ι → A<GOAL>Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) = Polynomial.map ((MvPolynomial.eval x).comp (MvPolynomial.map (algebraMap R A))) (φ.polyCharpolyAux b bₘ)
<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>A : Type u_8<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module.Finite A (A ⊗[R] M)<VAR>inst✝ : Module.Free A (A ⊗[R] M)<VAR>x : ι → A<GOAL>(MvPolynomial.aeval x).toRingHom = (MvPolynomial.eval x).comp (MvPolynomial.map (algebraMap R A))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → Module R (M i)<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R N<VAR>β : ι → Type u_6<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (β₁ i)<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (β₂ i)<VAR>inst✝³ : (i : ι) → Module R (β i)<VAR>inst✝² : (i : ι) → Module R (β₁ i)<VAR>inst✝¹ : (i : ι) → Module R (β₂ i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → β₁ i →ₗ[R] β₂ i<VAR>h : (i : ι) → β₂ i →ₗ[R] N<VAR>l : Π₀ (i : ι), β₁ i<GOAL>((lsum ℕ) h) ((mapRange.linearMap f) l) = ((lsum ℕ) fun i => h i ∘ₗ f i) l
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>F : Set (Set E)<VAR>hF : F.Nonempty<VAR>hA : ∀ B ∈ F, IsExtreme 𝕜 A B<GOAL>IsExtreme 𝕜 A (⋂ B ∈ F, B)