ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>x✝ : ↑m ≤ n<GOAL>Differentiable 𝕜 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>a ⊓ (a ⇨ b) ≤ b
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<GOAL>card ↑(derangements (Fin n)) = numDerangements n
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m<GOAL>card ↑(derangements (Fin n)) = numDerangements n
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>n : ℕ<VAR>hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m<GOAL>card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>A : Finset α<VAR>h : A ∈ ↑(∂ 𝒜)<GOAL>A.card = r - 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>A : Finset α<VAR>hA : A ∈ 𝒜<VAR>i : α<VAR>hi : i ∈ A<VAR>h : A.erase i ∈ ↑(∂ 𝒜)<GOAL>(A.erase i).card = r - 1
<VAR>α : Type u_1<VAR>a✝¹ a✝ : PosNum<GOAL>((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ ν : ProbabilityMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s<VAR>s : Set Ω<VAR>s_mble : MeasurableSet s<GOAL>↑μ s = ↑ν s
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.7784<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ IsClosed (Function.pullbackDiagonal f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.7784<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>(∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂) ↔ ∀ (a b : X) (b_1 : f a = f b), ⟨(a, b), b_1⟩ ∈ (Function.pullbackDiagonal f)ᶜ → (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 a ×ˢ 𝓝 b)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.7784<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>x₁ x₂ : X<VAR>x✝¹ : f x₁ = f x₂<VAR>x✝ : x₁ ≠ x₂<VAR>h : ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂<GOAL>(Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.7784<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>x₁ x₂ : X<VAR>x✝² : f x₁ = f x₂<VAR>x✝¹ : x₁ ≠ x₂<VAR>x✝ : (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)<VAR>t : Set (X × X)<VAR>ht : t ∈ 𝓝 x₁ ×ˢ 𝓝 x₂<VAR>t_sub : Subtype.val ⁻¹' t ⊆ (Function.pullbackDiagonal f)ᶜ<GOAL>∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
<VAR>R✝ : Type u_1<VAR>inst✝¹¹ : CommRing R✝<VAR>S : Submonoid R✝<VAR>P : Type u_2<VAR>inst✝¹⁰ : CommRing P<VAR>inst✝⁹ : Algebra R✝ P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁸ : CommRing R₁<VAR>K✝ : Type u_4<VAR>inst✝⁷ : Field K✝<VAR>inst✝⁶ : Algebra R₁ K✝<VAR>inst✝⁵ : IsFractionRing R₁ K✝<VAR>inst✝⁴ : IsDomain R₁<VAR>R : Type u_6<VAR>inst✝³ : CommRing R<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>h : Ideal.span {a} = 0<GOAL>False
<VAR>R✝ : Type u_1<VAR>inst✝¹¹ : CommRing R✝<VAR>S : Submonoid R✝<VAR>P : Type u_2<VAR>inst✝¹⁰ : CommRing P<VAR>inst✝⁹ : Algebra R✝ P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁸ : CommRing R₁<VAR>K✝ : Type u_4<VAR>inst✝⁷ : Field K✝<VAR>inst✝⁶ : Algebra R₁ K✝<VAR>inst✝⁵ : IsFractionRing R₁ K✝<VAR>inst✝⁴ : IsDomain R₁<VAR>R : Type u_6<VAR>inst✝³ : CommRing R<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>h : a = 0<GOAL>False
<VAR>R✝ : Type u_1<VAR>inst✝¹¹ : CommRing R✝<VAR>S : Submonoid R✝<VAR>P : Type u_2<VAR>inst✝¹⁰ : CommRing P<VAR>inst✝⁹ : Algebra R✝ P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁸ : CommRing R₁<VAR>K✝ : Type u_4<VAR>inst✝⁷ : Field K✝<VAR>inst✝⁶ : Algebra R₁ K✝<VAR>inst✝⁵ : IsFractionRing R₁ K✝<VAR>inst✝⁴ : IsDomain R₁<VAR>R : Type u_6<VAR>inst✝³ : CommRing R<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = 0<VAR>h : a = 0<GOAL>False
<VAR>x : ℝ<GOAL>|sin (x / 2)| = √((1 - cos x) / 2)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Ring B✝<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R A<VAR>inst✝¹⁰ : Algebra R B✝<VAR>f✝ : R →+* S<VAR>B : Type u_5<VAR>C : Type u_6<VAR>F : Type u_7<VAR>inst✝⁹ : Ring B<VAR>inst✝⁸ : Ring C<VAR>inst✝⁷ : Algebra R B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : Algebra R C<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : Algebra A C<VAR>inst✝² : IsScalarTower R A C<VAR>b : B<VAR>inst✝¹ : FunLike F B C<VAR>inst✝ : AlgHomClass F A B C<VAR>f : F<VAR>P : R[X]<VAR>hP : P.Monic ∧ eval₂ (algebraMap R B) b P = 0<GOAL>IsIntegral R (f b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Ring B✝<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R A<VAR>inst✝¹⁰ : Algebra R B✝<VAR>f✝ : R →+* S<VAR>B : Type u_5<VAR>C : Type u_6<VAR>F : Type u_7<VAR>inst✝⁹ : Ring B<VAR>inst✝⁸ : Ring C<VAR>inst✝⁷ : Algebra R B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : Algebra R C<VAR>inst✝⁴ : IsScalarTower R A B<VAR>inst✝³ : Algebra A C<VAR>inst✝² : IsScalarTower R A C<VAR>b : B<VAR>inst✝¹ : FunLike F B C<VAR>inst✝ : AlgHomClass F A B C<VAR>f : F<VAR>P : R[X]<VAR>hP : P.Monic ∧ eval₂ (algebraMap R B) b P = 0<GOAL>eval₂ (algebraMap R C) (f b) P = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : Fintype l<VAR>inst✝¹ : Fintype m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>A : Matrix n l α<VAR>B : Matrix n m α<VAR>C : Matrix o l α<VAR>D : Matrix o m α<VAR>A' : Matrix l p α<VAR>B' : Matrix l q α<VAR>C' : Matrix m p α<VAR>D' : Matrix m q α<VAR>i : n ⊕ o<VAR>j : p ⊕ q<GOAL>(fromBlocks A B C D * fromBlocks A' B' C' D') i j = fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>y₁ y₂ : F<GOAL>(fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>y₁ y₂ : F<GOAL>(fun x_1 => (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} = (fun p => p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>y₁ y₂ : F<VAR>a : 𝕜 × 𝕜<VAR>ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}<GOAL>(x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.11099, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p : ℤ<GOAL>(inr φ).f p ≫ (triangle φ).mor₃.f p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<GOAL>μ.singularPart 0 = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν μ : Measure α<GOAL>μ.singularPart 0 = μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>(X ^ n * p).natDegree = p.natDegree + n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>x y : α<VAR>hx : Irreducible x<GOAL>IsUnit (gcd x y) ↔ ¬x ∣ y
<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>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p p'<VAR>hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2<GOAL>TendstoUniformlyOnFilter F' f p p'
<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>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p p'<VAR>hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>n : ι × α<VAR>h : (f n.2, F n.1 n.2) ∈ u ∧ F n.1 n.2 = F' n.1 n.2<GOAL>(f n.2, F' n.1 n.2) ∈ u
<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>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p p'<VAR>hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>n : ι × α<VAR>h : (f n.2, F n.1 n.2) ∈ u ∧ F n.1 n.2 = F' n.1 n.2<GOAL>(f n.2, F n.1 n.2) ∈ u
<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>c : Set (Set α)<GOAL>⋃₀ c = univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>-((u ^ 4) ^ 3 * W'.negDblY P) - W'.a₁ * ((u ^ 4) ^ 2 * W'.dblX P) * (u ^ 4 * W'.dblZ P) - W'.a₃ * (u ^ 4 * W'.dblZ P) ^ 3 = (u ^ 4) ^ 3 * (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : MulOneClass G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x a : G<GOAL>1 * a = x ↔ a = x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<GOAL>T1Space E
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<VAR>this : TopologicalAddGroup E<GOAL>T1Space E
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<VAR>this : TopologicalAddGroup E<GOAL>IsClosed {0}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<VAR>this : TopologicalAddGroup E<GOAL>∀ x ∈ {0}ᶜ, ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<VAR>this : TopologicalAddGroup E<VAR>x : E<VAR>hx : x ≠ 0<VAR>i : ι<VAR>pi_nonzero : (p i) x ≠ 0<GOAL>∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0<VAR>this : TopologicalAddGroup E<VAR>x : E<VAR>hx : x ≠ 0<VAR>i : ι<VAR>pi_nonzero : (p i) x ≠ 0<GOAL>0 ∉ ({i}.sup p).ball x ((p i) x)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsDomain R<VAR>hM : M ≤ R⁰<VAR>p : Ideal S<VAR>hpp : p.IsPrime<VAR>hp0 : p ≠ ⊥<GOAL>⊥ < Ideal.comap (algebraMap R S) p
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsDomain R<VAR>hM : M ≤ R⁰<VAR>p : Ideal S<VAR>hpp : p.IsPrime<VAR>hp0 : p ≠ ⊥<VAR>this : IsDomain S<GOAL>⊥ < Ideal.comap (algebraMap R S) p
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsDomain R<VAR>hM : M ≤ R⁰<VAR>p : Ideal S<VAR>hpp : p.IsPrime<VAR>hp0 : p ≠ ⊥<VAR>this : IsDomain S<GOAL>Ideal.comap (algebraMap R S) ⊥ < Ideal.comap (algebraMap R S) p
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f ≠ 0<GOAL>f.eraseLead.support.card < f.support.card
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f ≠ 0<GOAL>(f.support.erase f.natDegree).card < f.support.card
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hxy : P x * Q z ^ 2 = Q x * P z ^ 2 → P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>toAffine W ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1] = toAffine W P + toAffine W Q
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Mᵢ i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (Nᵢ i)<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝³ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝² : Module R P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Invertible 2<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>⟨⅟2, ⋯⟩ • (pi Q).polarBilin = ∑ i : ι, LinearMap.compl₁₂ (⟨⅟2, ⋯⟩ • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Mᵢ i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (Nᵢ i)<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝³ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝² : Module R P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Invertible 2<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>∑ x : ι, ⟨⅟2, ⋯⟩ • LinearMap.compl₁₂ (Q x).polarBilin (LinearMap.proj x) (LinearMap.proj x) = ∑ i : ι, LinearMap.compl₁₂ (⟨⅟2, ⋯⟩ • (Q i).polarBilin) (LinearMap.proj i) (LinearMap.proj i)
<VAR>x : ℝ<GOAL>-↑x ∈ slitPlane ↔ x < 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α<VAR>a b c d : α<GOAL>a ⊔ b ≤ a ⊓ b ↔ a = b
<VAR>α✝ : Type u_1<VAR>inst✝² : MeasurableSpace α✝<VAR>inst✝¹ : CountablyGenerated α✝<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<GOAL>⨆ n, ↑(countableFiltration α) n = m
<VAR>α✝ : Type u_1<VAR>inst✝² : MeasurableSpace α✝<VAR>inst✝¹ : CountablyGenerated α✝<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<GOAL>⨆ n, ↑(countableFiltration α) n = ⨆ i, generateFrom (countablePartition α i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>a b x : α<VAR>inst✝ : SecondCountableTopology α<VAR>f g : δ → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => Max.max (f a) (g a)
<VAR>R : Type u_1<VAR>inst✝⁹ : Semiring R<VAR>M : Type u_2<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>M₂ : Type u_3<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>inst✝² : (i : ι) → TopologicalSpace (φ i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<GOAL>pi f = 0 ↔ ∀ (i : ι), f i = 0
<VAR>R : Type u_1<VAR>inst✝⁹ : Semiring R<VAR>M : Type u_2<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>M₂ : Type u_3<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>ι : Type u_4<VAR>φ : ι → Type u_5<VAR>inst✝² : (i : ι) → TopologicalSpace (φ i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>f : (i : ι) → M →L[R] φ i<GOAL>(∀ (x : M) (a : ι), (f a) x = 0 x a) ↔ ∀ (i : ι) (x : M), (f i) x = 0 x
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>(fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary) 1 = 1
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f g : C(↑(spectrum ℝ A), ℝ)<GOAL>{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯ }.toFun (f * g) = { toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯ }.toFun f * { toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯ }.toFun g
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f g : C(↑(spectrum ℝ A), ℝ)<VAR>this : ∀ {a b c d e f : Matrix n n 𝕜}, a * b * c * (d * e * f) = a * (b * (c * d) * e) * f<GOAL>{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯ }.toFun (f * g) = { toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯ }.toFun f * { toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯ }.toFun g
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f g : C(↑(spectrum ℝ A), ℝ)<VAR>this : ∀ {a b c d e f : Matrix n n 𝕜}, a * b * c * (d * e * f) = a * (b * (c * d) * e) * f<GOAL>↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ (⇑f * ⇑g) ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary = (↑hA.eigenvectorUnitary * diagonal fun i => ↑(f ⟨hA.eigenvalues i, ⋯⟩) * ↑(g ⟨hA.eigenvalues i, ⋯⟩)) * star ↑hA.eigenvectorUnitary
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>(↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f g : C(↑(spectrum ℝ A), ℝ)<GOAL>(↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯ }).toFun (f + g) = (↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯ }).toFun f + (↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯ }).toFun g
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f g : C(↑(spectrum ℝ A), ℝ)<GOAL>↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ (⇑f + ⇑g) ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary = (↑hA.eigenvectorUnitary * diagonal fun i => ↑(f ⟨hA.eigenvalues i, ⋯⟩) + ↑(g ⟨hA.eigenvalues i, ⋯⟩)) * star ↑hA.eigenvectorUnitary
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>r : ℝ<GOAL>(↑↑{ toFun := fun g => ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) * star ↑hA.eigenvectorUnitary, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap ℝ C(↑(spectrum ℝ A), ℝ)) r) = (algebraMap ℝ (Matrix n n 𝕜)) r
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>r : ℝ<GOAL>(↑hA.eigenvectorUnitary * diagonal fun x => ↑r) * star ↑hA.eigenvectorUnitary = (algebraMap ℝ (Matrix n n 𝕜)) r