ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<VAR>c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)<VAR>x : α<VAR>y : β x<GOAL>ωSup (c.map (evalOrderHom ⟨x, y⟩)) = ωSup (((c.map (monotoneCurry α β γ)).map (evalOrderHom x)).map (evalOrderHom y))
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<VAR>c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)<VAR>x : α<VAR>y : β x<GOAL>ωSup (c.map (evalOrderHom ⟨x, y⟩)) = ωSup (c.map (((evalOrderHom y).comp (evalOrderHom x)).comp (monotoneCurry α β γ)))
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x✝ c : ℂ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>r : ℂ<VAR>hr : r ≠ -1<GOAL>HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x✝ c : ℂ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<GOAL>HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x✝ c : ℂ<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hx : 0 < x<GOAL>HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x✝ c : ℂ<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>r : ℂ<VAR>hr : r + 1 ≠ 0<VAR>hx : 0 > x<GOAL>HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s✝ t : Set α<VAR>μ✝ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : Measure α<VAR>s : Set β<GOAL>IntegrableOn f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝¹ : Module.Free R ↥A<VAR>inst✝ : Module.Free R ↥B<VAR>a✝ : Nontrivial R<GOAL>Module.rank R ↥(A ⊔ B) ≤ Module.rank R ↥A * Module.rank R ↥B
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝¹ : Module.Free R ↥A<VAR>inst✝ : Module.Free R ↥B<VAR>a✝ : Nontrivial R<GOAL>Module.rank R ↥(A.mulMap B).range ≤ Module.rank R (↥A ⊗[R] ↥B)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : l₁.length = l₂.length<GOAL>(l₁.zip l₂).unzip = (l₁, l₂)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F✝ G H I : C ⥤ D<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : C ⥤ D ⥤ E<VAR>Z : D<GOAL>(F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 ((F.obj X).obj Z)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ bᶜ ↔ Disjoint a b
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>(insert a s).pi t = (t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>((insert a s).pi t).val = ((t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)).val
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>((insert a s).pi t).val.dedup = ((t a).biUnion fun b => image (Pi.cons s a b) (s.pi t)).val
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<VAR>s' : Multiset α<VAR>h : s' = a ::ₘ s.val<GOAL>(s'.pi fun a => (t a).val).dedup = ((t a).val.bind fun b => (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>((a ::ₘ s.val).pi fun a => (t a).val).dedup = ((t a).val.bind fun b => (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>((t a).val.bind fun b => Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a => (t a).val)).dedup = ((t a).val.bind fun b => (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup).dedup
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>(fun b => Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a => (t a).val)) = fun b => (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>δ : α → Sort v<VAR>inst✝¹ : DecidableEq α<VAR>s✝ : Finset α<VAR>t✝ : (a : α) → Finset (β a)<VAR>inst✝ : (a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<VAR>b : β a<GOAL>Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a => (t a).val) = (Multiset.map (fun f a' h' => Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a => (t a).val)).dedup
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : ProperSpace 𝕜<VAR>a : A<VAR>ha : (σ a).Nonempty<GOAL>∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : ProperSpace 𝕜<VAR>a : A<VAR>ha : (σ a).Nonempty<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>h : IsMaxOn (fun a => ‖a‖₊) (σ a) k<GOAL>∃ k ∈ σ a, ↑‖k‖₊ = spectralRadius 𝕜 a
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(inv f ⊗ g) ≫ (f ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>𝟙 W ⊗ g ≫ h = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : AddCommMonoid M<VAR>g : G<VAR>f : α →₀ M<VAR>a : α<GOAL>(g • f) a = f (g⁻¹ • a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : AddCommMonoid M<VAR>g : G<VAR>f : α →₀ M<VAR>a : α<GOAL>(g • f) (g • g⁻¹ • a) = f (g⁻¹ • a)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : F α<VAR>i : Fin2 n<GOAL>supp (g <$$> x) i = g i '' supp x i
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : F α<VAR>i : Fin2 n<GOAL>supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : F α<VAR>i : Fin2 n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<GOAL>supp (g <$$> abs ⟨a, f⟩) i = g i '' supp (abs ⟨a, f⟩) i
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : F α<VAR>i : Fin2 n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<GOAL>supp (abs ⟨a, g ⊚ f⟩) i = g i '' supp (abs ⟨a, f⟩) i
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>h : IsUniform<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>x : F α<VAR>i : Fin2 n<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<GOAL>(g ⊚ f) i '' univ = g i ∘ f i '' univ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : NonAssocSemiring S<VAR>ϕ : R →+* S<VAR>hϕ : Injective ⇑ϕ<VAR>hR : CharZero R<VAR>a b : ℕ<VAR>h : ↑a = ↑b<GOAL>a = b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>a : α<GOAL>l₁.length ≤ (l₁ ++ l₂).length
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x y : α<VAR>h : Commute x y<VAR>hxy : x ≠ y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x y : α<VAR>h : Commute x y<VAR>hxy : x ≠ y<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>this : x - y ≠ 0<GOAL>∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<GOAL>iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume<GOAL>iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume<VAR>B : AEStronglyMeasurable f volume<GOAL>iteratedDeriv n (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) ^ n • f x) x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume<VAR>B : AEStronglyMeasurable f volume<GOAL>(∫ (v : ℝ), 𝐞 (-⟪v, x⟫_ℝ) • (fourierPowSMulRight (innerSL ℝ) f v n) fun x => 1) = ∫ (v : ℝ), 𝐞 (-⟪v, x⟫_ℝ) • (-2 * ↑π * I * ↑v) ^ n • f v
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume<VAR>B : AEStronglyMeasurable f volume<VAR>y : ℝ<GOAL>(𝐞 (-⟪y, x⟫_ℝ) • (fourierPowSMulRight (innerSL ℝ) f y n) fun x => 1) = 𝐞 (-⟪y, x⟫_ℝ) • (-2 * ↑π * I * ↑y) ^ n • f y
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun x => x ^ n • f x) volume<VAR>hn : ↑n ≤ N<VAR>x : ℝ<VAR>A : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) volume<VAR>B : AEStronglyMeasurable f volume<VAR>y : ℝ<GOAL>(-(2 * ↑π * I)) ^ n • y ^ n • f y = (-(2 * ↑π * I * ↑y)) ^ n • f y
<VAR>q : ℚ≥0<VAR>r : ℝ<GOAL>↑(q • r) = q • ↑r
<VAR>z : ℂ<VAR>i j : Fin 2<GOAL>(leftMulMatrix basisOneI) z i j = !![z.re, -z.im; z.im, z.re] i j
<VAR>z : ℂ<VAR>i j : Fin 2<GOAL>![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i = ![![z.re, -z.im], ![z.im, z.re]] i j
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp = { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P✝ : Ideal S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : p.IsMaximal<VAR>P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }<GOAL>finrank (R ⧸ p) (S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P) = ramificationIdx (algebraMap R S) p ↑P * inertiaDeg (algebraMap R S) p ↑P
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P✝ : Ideal S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : p.IsMaximal<VAR>P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }<GOAL>↑P ≠ ⊥
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P✝ : Ideal S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : p.IsMaximal<VAR>P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }<GOAL>ramificationIdx (algebraMap R S) p ↑P ≠ 0
<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝ : T2Space M<GOAL>tsupport ↑f ⊆ (chartAt H c).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β<VAR>p : l.Palindrome<GOAL>(map f l).reverse = map f l
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s + -t)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>f : ι → α<GOAL>Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a
<VAR>n : ℕ<VAR>i : ZMod (2 * n)<GOAL>xa i ^ 4 = 1
<VAR>n : ℕ<VAR>i : ZMod (2 * n)<GOAL>a (↑n + ↑n) = 1
<VAR>n : ℕ<VAR>i : ZMod (2 * n)<GOAL>a ↑(n + n) = 1
<VAR>n : ℕ<VAR>i : ZMod (2 * n)<GOAL>a ↑(2 * n) = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²¹ : RCLike 𝕜<VAR>inst✝²⁰ : NormedAddCommGroup E<VAR>inst✝¹⁹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁸ : CompleteSpace E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁵ : CompleteSpace E'<VAR>inst✝¹⁴ : NormedSpace ℝ E'<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup G'<VAR>inst✝⁹ : NormedSpace ℝ G'<VAR>inst✝⁸ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁷ : RCLike 𝕜'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : InnerProductSpace 𝕜' E''<VAR>inst✝⁴ : CompleteSpace E''<VAR>inst✝³ : NormedSpace ℝ E''<VAR>inst✝² : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : 𝕜<VAR>x : F<GOAL>condexpIndSMul hm hs hμs (c • x) = c • condexpIndSMul hm hs hμs x
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>A : Set X<VAR>f : X → β<VAR>hf1 : Continuous f<VAR>hf2 : Function.Injective f<VAR>x : β<VAR>hx : x ∈ f '' derivedSet A<GOAL>x ∈ derivedSet (f '' A)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>A : Set X<VAR>f : X → β<VAR>hf1 : Continuous f<VAR>hf2 : Function.Injective f<VAR>x : β<VAR>hx : ∃ x_1, AccPt x_1 (𝓟 A) ∧ f x_1 = x<GOAL>x ∈ derivedSet (f '' A)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>A : Set X<VAR>f : X → β<VAR>hf1 : Continuous f<VAR>hf2 : Function.Injective f<VAR>y : X<VAR>hy1 : AccPt y (𝓟 A)<GOAL>f y ∈ derivedSet (f '' A)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>A : Set X<VAR>f : X → β<VAR>hf1 : Continuous f<VAR>hf2 : Function.Injective f<VAR>y : X<VAR>hy1 : AccPt y (𝓟 A)<GOAL>f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<GOAL>(p.takeUntil u h).length ≤ p.length
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length<GOAL>(p.takeUntil u h).length ≤ p.length
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>this : (p.takeUntil u h).length + (p.dropUntil u h).length = p.length<GOAL>(p.takeUntil u h).length ≤ p.length
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x✝ : S<VAR>g : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>s : R<GOAL>eval₂ g x (s • p) = g s * eval₂ g x p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x✝ : S<VAR>g : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>s : R<VAR>A : p.natDegree < p.natDegree.succ<GOAL>eval₂ g x (s • p) = g s * eval₂ g x p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x✝ : S<VAR>g : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>s : R<VAR>A : p.natDegree < p.natDegree.succ<VAR>B : (s • p).natDegree < p.natDegree.succ<GOAL>eval₂ g x (s • p) = g s * eval₂ g x p
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>type (Quotient.out o).r = o
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : SecondCountableTopology V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>μ : Measure V<VAR>N : ℕ∞<VAR>hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ<VAR>h'f : AEStronglyMeasurable f μ<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>w : W<GOAL>iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w = fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) w
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>f : P →ᵃ[R] P'<VAR>x y : P<GOAL>⇑f '' affineSegment R x y = affineSegment R (f x) (f y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>f : P →ᵃ[R] P'<VAR>x y : P<GOAL>(fun x_1 => f ((lineMap x y) x_1)) '' Set.Icc 0 1 = ⇑(f.comp (lineMap x y)) '' Set.Icc 0 1
<VAR>a b : Cardinal.{u_1}<GOAL>a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>i : ℤ<GOAL>((g * f * g⁻¹) ^ i) x = y ↔ (f ^ i) (g⁻¹ x) = g⁻¹ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>x y : α<GOAL>x ⩿ y ↔ ReflGen (fun x x_1 => x ⋖ x_1) x y
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>n : ℕ<VAR>hn : Odd n<VAR>hχ : χ ^ n = 1<GOAL>χ (-1) = 1
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>n : ℕ<VAR>hn : Odd n<VAR>hχ : χ ^ n = 1<GOAL>1 (-1) = 1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(colimitHomIsoLimitYoneda F A).inv ≫ (coyoneda.map (colimit.ι F i).op).app A = limit.π (F.op ⋙ yoneda.obj A) (op i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>r : β<VAR>s : Set α<VAR>f : α →ₛ β<VAR>hr : r ∈ (f.restrict s).range<VAR>h0 : r ≠ 0<VAR>hs : MeasurableSet s<GOAL>r ∈ ↑f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>r : β<VAR>s : Set α<VAR>f : α →ₛ β<VAR>hr : r ∈ (f.restrict s).range<VAR>h0 : r ≠ 0<VAR>hs : ¬MeasurableSet s<GOAL>r ∈ ↑f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>r : β<VAR>s : Set α<VAR>f : α →ₛ β<VAR>hr : r ∈ SimpleFunc.range 0<VAR>h0 : r ≠ 0<VAR>hs : ¬MeasurableSet s<GOAL>r ∈ ↑f '' s
<VAR>w x✝ y✝ z y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0<GOAL>(x ^ y⁻¹) ^ y = x