ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<GOAL>WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<GOAL>WithTop.map (⇑ofDual) s.min = s.sup (WithBot.some ∘ ⇑ofDual)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<GOAL>Disjoint (Finset.filter IsPrimePow a.divisors) (Finset.filter IsPrimePow b.divisors)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<GOAL>∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k a b : ℕ<VAR>hab : a.Coprime b<VAR>n : ℕ<VAR>han : n ∣ a<VAR>_ha : a ≠ 0<VAR>hn : IsPrimePow n<VAR>hbn : n ∣ b<VAR>_hb : b ≠ 0<GOAL>False
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) W.polynomialZ = P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 - (W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) (X 1 ^ 2 + C W.a₁ * X 0 * X 1 + C (2 * W.a₃) * X 1 * X 2 - (C W.a₂ * X 0 ^ 2 + C (2 * W.a₄) * X 0 * X 2 + C (3 * W.a₆) * X 2 ^ 2)) = P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 - (W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hs : s.Nonempty<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<GOAL>(ω f ϕ s).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hs : s.Nonempty<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<GOAL>(⋂ u, closure (image2 ϕ (↑u ∩ v) s)).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hs : s.Nonempty<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<GOAL>Directed (fun x x_1 => x ⊇ x_1) fun i => closure (image2 ϕ (↑i ∩ v) s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hs : s.Nonempty<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<GOAL>∀ (i : ↑f.sets), (closure (image2 ϕ (↑i ∩ v) s)).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hs : s.Nonempty<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<GOAL>∀ (i : ↑f.sets), IsCompact (closure (image2 ϕ (↑i ∩ v) s))
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>inst✝ : f.NeBot<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>hs : s.Nonempty<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<GOAL>∀ (i : ↑f.sets), IsClosed (closure (image2 ϕ (↑i ∩ v) s))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>s : Subgroup G<VAR>hx : x ∈ s<GOAL>orderOf x ∣ Nat.card ↥s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>E : Set α<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδ_pos : 0 < δ<VAR>hδε : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : (μ.restrict E) s ≤ ENNReal.ofReal δ<GOAL>eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>E : Set α<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ<VAR>hδ_pos : 0 < δ<VAR>hδε : ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ<GOAL>eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
<VAR>m n : ℕ<VAR>h : m.Coprime n<GOAL>m.lcm n = m * n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>M : Type u_5<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, StronglyMeasurable f<GOAL>StronglyMeasurable fun x => (Multiset.map (fun f => f x) s).prod
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit b<GOAL>a / b = c ↔ a = c * b
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>m : ℝ<VAR>hf' : ∀ x ∈ s, f' x ≠ m<GOAL>(∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>m : ℝ<VAR>hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m<GOAL>∃ x ∈ s, f' x = m
<VAR>a✝ b✝ : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : Convex ℝ s<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>m b : ℝ<VAR>hb : b ∈ s<VAR>hmb : m ≤ f' b<VAR>a : ℝ<VAR>ha : a ∈ s<VAR>hma : f' a ≤ m<GOAL>∃ x ∈ s, f' x = m
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>L'' : Filter E<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L''<VAR>hL : Tendsto f L'' L'<GOAL>HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>L'' : Filter E<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L''<VAR>hL : Tendsto f L'' L'<GOAL>HSMul.hSMul h₂' = (ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝² : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x✝¹ : E<VAR>L'' : Filter E<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (f x✝¹) L'<VAR>hf : HasFDerivAtFilter f f' x✝¹ L''<VAR>hL : Tendsto f L'' L'<VAR>x : E →L[𝕜] 𝕜'<VAR>x✝ : E<GOAL>(h₂' • x) x✝ = ((ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp x) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s✝ t s : Set α<GOAL>∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s✝ t s : Set α<GOAL>Injective Subtype.val
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝⁹ : CommRing Rₛ<VAR>inst✝⁸ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup Mₛ<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ inst✝³ : Module R Mₛ<VAR>inst✝² : Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<GOAL>span R (Set.range ⇑(ofIsLocalizedModule Rₛ S f b)) = LinearMap.range f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>f : Filter α<VAR>g : Filter β<GOAL>0 • g ≤ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set β<VAR>hs : s ∈ 0<GOAL>(fun x => 0 • x) ⁻¹' s ∈ g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set β<VAR>hs : s ∈ 0<GOAL>(fun x => 0 • x) ⁻¹' s = univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set β<VAR>hs : s ∈ 0<VAR>a : β<GOAL>a ∈ (fun x => 0 • x) ⁻¹' s
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>c⁻¹ * a ≤ b ↔ a ≤ b * c
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>inst✝⁷ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁶ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<VAR>inst✝⁵ : HasCokernel f<VAR>inst✝⁴ : HasCokernel (G.map f)<VAR>inst✝³ : PreservesColimit (parallelPair f 0) G<VAR>X' Y' : C<VAR>g : X' ⟶ Y'<VAR>inst✝² : HasCokernel g<VAR>inst✝¹ : HasCokernel (G.map g)<VAR>inst✝ : PreservesColimit (parallelPair g 0) G<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>G.map f ≫ G.map q = G.map p ≫ G.map g
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁸ : Category.{v₂, u₂} D<VAR>inst✝⁷ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝⁶ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<VAR>inst✝⁵ : HasCokernel f<VAR>inst✝⁴ : HasCokernel (G.map f)<VAR>inst✝³ : PreservesColimit (parallelPair f 0) G<VAR>X' Y' : C<VAR>g : X' ⟶ Y'<VAR>inst✝² : HasCokernel g<VAR>inst✝¹ : HasCokernel (G.map g)<VAR>inst✝ : PreservesColimit (parallelPair g 0) G<VAR>p : X ⟶ X'<VAR>q : Y ⟶ Y'<VAR>hpq : f ≫ q = p ≫ g<GOAL>(PreservesCokernel.iso G f).hom ≫ cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ = G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁷ : Ring K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V'<VAR>inst✝ : Nontrivial K<GOAL>rank 0 = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c d : α<GOAL>↑(Ico a b * Ioc c d) ⊆ ↑(Ioo (a * c) (b * d))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>sign σ = (Multiset.map (fun n => -(-1) ^ n) σ.cycleType).prod
<VAR>z w : ℂ<VAR>h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0<VAR>h₂ : 0 < (z, w).2.re<GOAL>ContinuousAt (fun x => x.1 ^ x.2) (z, w)
<VAR>z w : ℂ<VAR>h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0<VAR>h₂ : 0 < (z, w).2.re<GOAL>ContinuousAt (fun x => x.1 ^ x.2) (z, w)
<VAR>z w : ℂ<VAR>h₂ : 0 < (z, w).2.re<VAR>h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0<GOAL>ContinuousAt (fun x => x.1 ^ x.2) (z, w)
<VAR>w : ℂ<VAR>h₂ : 0 < (0, w).2.re<GOAL>ContinuousAt (fun x => x.1 ^ x.2) (0, w)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<GOAL>Derivation R A ↥I ≃ { f // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) }
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>d : Derivation R A ↥I<GOAL>(Ideal.Quotient.mkₐ R I).comp (liftOfDerivationToSquareZero I hI d) = IsScalarTower.toAlgHom R A (B ⧸ I)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<GOAL>Function.LeftInverse (fun f => derivationToSquareZeroOfLift I hI ↑f ⋯) fun d => ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<GOAL>Function.RightInverse (fun f => derivationToSquareZeroOfLift I hI ↑f ⋯) fun d => ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype p<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : AddCommMonoidWithOne R<GOAL>trace 1 = ↑(Fintype.card n)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.17551<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>y : Y<GOAL>DiscreteTopology X ↔ IsLocallyInjective fun x => y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.17551<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>y : Y<GOAL>(∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.17551<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>y : Y<VAR>x : X<VAR>x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>inj : Set.InjOn (fun x => y) U<GOAL>{x} ∈ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.17551<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>y : Y<VAR>x : X<VAR>x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>inj : Set.InjOn (fun x => y) U<VAR>x' : X<GOAL>x' ∈ {x} ↔ x' ∈ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.17551<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>y : Y<VAR>x : X<VAR>x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x => y) U<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>inj : Set.InjOn (fun x => y) U<VAR>x' : X<GOAL>x' ∈ {x} → x' ∈ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.17551<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>y : Y<VAR>U : Set X<VAR>inj : Set.InjOn (fun x => y) U<VAR>x' : X<VAR>x✝ : ∃ U ∈ 𝓝 x', Set.InjOn (fun x => y) U<VAR>hU : U ∈ 𝓝 x'<GOAL>x' ∈ U
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖₊) '' ball 0 1) = ‖f‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>∀ a ∈ (fun x => ‖f x‖₊) '' ball 0 1, a ≤ ‖f‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>ub : ℝ≥0<VAR>hub : ub < ‖f‖₊<GOAL>∃ a ∈ (fun x => ‖f x‖₊) '' ball 0 1, ub < a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x n r<VAR>hg : HasFiniteFPowerSeriesOnBall g pg x m r<VAR>N : ℕ<VAR>hN : max n m ≤ N<GOAL>(pf + pg) N = 0
<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 y : M<VAR>hy : y ∈ (extChartAt I x).source<GOAL>y ∈ (chartAt H x).source
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f : G → E<VAR>g : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>hf' : ∀ (x : G), f (x * g) = -f x<GOAL>∫ (x : G), f x ∂μ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>a : ι → ι → 𝕜<GOAL>∑ i ∈ s, ∑ j ∈ s, a i j • ⟪v j, v i⟫_𝕜 = ∑ k ∈ s, a k k
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<VAR>ε : ℝ<VAR>H : ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)<VAR>r : ℚ<VAR>hr : r.den ≤ n<GOAL>ε ≤ dist x ↑r
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : AddCircle T<GOAL>(fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)
<VAR>T : ℝ<VAR>n : ℤ<VAR>z✝ : ℝ<GOAL>(fourier (-n)) ↑z✝ = (starRingEnd ℂ) ((fourier n) ↑z✝)
<VAR>T : ℝ<VAR>n : ℤ<VAR>z✝ : ℝ<GOAL>↑(⋯.lift (-n • ↑z✝)) = (starRingEnd ℂ) ↑(⋯.lift (n • ↑z✝))
<VAR>T : ℝ<VAR>n : ℤ<VAR>z✝ : ℝ<GOAL>↑(⋯.lift ↑(-n • z✝)) = (starRingEnd ℂ) ↑(⋯.lift ↑(n • z✝))
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>u : 𝕜 → E<VAR>v : 𝕜 → F<VAR>u' : E<VAR>v' : F<VAR>hu : HasDerivWithinAt u u' s x<VAR>hv : HasDerivWithinAt v v' s x<GOAL>HasDerivWithinAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x
<VAR>x : ℝ<GOAL>cos (π / 3) = 1 / 2
<VAR>x : ℝ<VAR>h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0<GOAL>cos (π / 3) = 1 / 2