ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Summable fun n => ↑n ^ k * rexp (-r * ↑n)
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Summable fun n => ↑n ^ k * rexp (-r) ^ n
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>‖rexp (-r)‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(image Subtype.val s.attach).val = s.val
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>s : Set G<VAR>g : G<VAR>S : Set G<VAR>hS : closure S = ⊤<GOAL>center G = ⨅ g ∈ S, centralizer ↑(zpowers g)
<VAR>α : Type u_1<VAR>f g : α → ℝ<VAR>s : Set α<GOAL>regionBetween f g s ⊆ s ×ˢ univ
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he : ∀ (x y : ℝ), ↑x + ↑y * I = e (x, y)<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) - I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<VAR>hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<VAR>hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R<VAR>htc : ContinuousOn F R<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<VAR>hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R<VAR>htc : ContinuousOn F R<VAR>htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) - I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<VAR>hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R<VAR>htc : ContinuousOn F R<VAR>htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p<GOAL>(((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) + ∫ (x : ℝ) in w.im..z.im, -(I • f (e (w.re, x)))) - ∫ (x : ℝ) in w.im..z.im, -(I • f (e (z.re, x))) = ∫ (x : ℝ) in z.re..w.re, ∫ (x_1 : ℝ) in w.im..z.im, (-(I • F' (x, x_1))) (1, 0) + (F' (x, x_1)) (0, 1)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<VAR>hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R<VAR>htc : ContinuousOn F R<VAR>htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p<GOAL>IntegrableOn (fun x => ((fun p => -(I • F' p)) x) (1, 0) + (F' x) (0, 1)) ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>f' : ℂ → ℂ →L[ℝ] E<VAR>z w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])<VAR>Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn ((fun z => I • (f' z) 1 - (f' z) I) ∘ ⇑measurableEquivRealProd.symm) (⇑measurableEquivRealProd.symm ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]])) volume<VAR>e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm<VAR>he₁ : e (1, 0) = 1<VAR>he₂ : e (0, 1) = I<VAR>he : ℝ → ℝ → True<VAR>F : ℝ × ℝ → E := f ∘ ⇑e<VAR>F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e<VAR>hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)<VAR>R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]<VAR>t : Set (ℝ × ℝ) := ⇑e ⁻¹' s<VAR>hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R<VAR>htc : ContinuousOn F R<VAR>htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p<GOAL>IntegrableOn (fun x => ((fun p => -(I • F' p)) x) (1, 0) + (F' x) (0, 1)) ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<GOAL>Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l<VAR>s : Set β<VAR>hs : s ∈ l<GOAL>s ∈ map f k
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>s : Set β<VAR>hs : s ∈ l<VAR>H : s ∉ map f k<GOAL>∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>s : Set β<VAR>hs : s ∈ l<VAR>H : s ∉ map f k<VAR>this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot<GOAL>∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>s : Set β<VAR>hs : s ∈ l<VAR>H : s ∉ map f k<VAR>this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot<VAR>x : ℕ → α<VAR>hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))<GOAL>∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>s : Set β<VAR>hs : s ∈ l<VAR>H : s ∉ map f k<VAR>this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot<VAR>x : ℕ → α<VAR>hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ<GOAL>∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>s : Set β<VAR>hs : s ∈ l<VAR>H : s ∉ map f k<VAR>this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot<VAR>x : ℕ → α<VAR>hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ<VAR>h : Tendsto (f ∘ x) atTop l<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>inst✝ : k.IsCountablyGenerated<VAR>s : Set β<VAR>hs : s ∈ l<VAR>H : s ∉ map f k<VAR>this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot<VAR>x : ℕ → α<VAR>hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ<VAR>h : Tendsto (f ∘ x) atTop l<VAR>N : ℕ<VAR>hnmem : x N ∈ f ⁻¹' sᶜ<VAR>hmem : (f ∘ x) N ∈ s<GOAL>False
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hij : i ≠ j<GOAL>(interpolate s v) r = (interpolate (s.erase j) v) r * basisDivisor (v i) (v j) + (interpolate (s.erase i) v) r * basisDivisor (v j) (v i)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hij : i ≠ j<GOAL>{i, j} ⊆ s
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>x : E<GOAL>x ∈ adjoin F S ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>x : E<GOAL>(∃ a a_1, (MvPolynomial.aeval Subtype.val) a / (MvPolynomial.aeval Subtype.val) a_1 = x) ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G : OplaxFunctor B C<VAR>η θ ι : F ⟶ G<VAR>Γ : Modification η θ<VAR>a b c : B<VAR>a' : C<VAR>f : a ⟶ b<VAR>g : G.obj b ⟶ a'<GOAL>F.map f ◁ Γ.app b ▷ g ≫ (α_ (F.map f) (θ.app b) g).inv ≫ θ.naturality f ▷ g = (α_ (F.map f) (η.app b) g).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g
<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>x y : E<GOAL>⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜
<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>x y : E<GOAL>(starRingEnd 𝕜) (-⟪y, x⟫_𝕜) = -⟪x, y⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : Group α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>ha : 1 ≤ a ^ 2<GOAL>1 ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : Group α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>ha : 1 ≤ a ^ 2<GOAL>(a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : EvenHom Q A<VAR>m₁ m₂ : M<GOAL>(((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (((foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ((CliffordAlgebra.ι Q) m₂))) ((CliffordAlgebra.ι Q) m₁)).1 = (f.bilin m₁) m₂
<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : EvenHom Q A<VAR>m₁ m₂ : M<GOAL>(((CliffordAlgebra.even.lift.fFold f) m₁) (((CliffordAlgebra.even.lift.fFold f) m₂) (1, 0))).1 = (f.bilin m₁) m₂
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>k m n : ℕ<VAR>h : m ≤ n + 1<GOAL>∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>k m n : ℕ<VAR>h : m ≤ n + 1<VAR>this : ∀ i < m, i ≤ n<GOAL>∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>k m n : ℕ<VAR>h : m ≤ n + 1<VAR>this : ∀ i < m, i ≤ n<VAR>hkm : k < m<GOAL>∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>k m n : ℕ<VAR>h : m ≤ n + 1<VAR>this : ∀ i < m, i ≤ n<VAR>hkm : m ≤ k<GOAL>∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝ : Semigroup G<VAR>a b c : G<VAR>h : SemiconjBy a b c<VAR>j : G<GOAL>(fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)
<VAR>q a b c : ℚ<VAR>n : ℤ<GOAL>mkRat n 1 = ↑n
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x y : O<VAR>h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)<VAR>hy : (algebraMap O F) y ≠ 0<GOAL>v (((algebraMap O F) y)⁻¹ * (algebraMap O F) x) ≤ 1
<VAR>F : Type u<VAR>Γ₀ : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation F Γ₀<VAR>O : Type w<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O F<VAR>hv : v.Integers O<VAR>x y : O<VAR>h : v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)<VAR>hy : (algebraMap O F) y ≠ 0<GOAL>v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) x) ≤ v ((algebraMap O F) y)⁻¹ * v ((algebraMap O F) y)
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Monoid G✝<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<GOAL>IsTorsionFree G ↔ CommGroup.torsion G = ⊥
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Monoid G✝<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<GOAL>(∀ (g : G), g ≠ 1 → ¬IsOfFinOrder g) ↔ ∀ ⦃x : G⦄, x ∈ CommGroup.torsion G → x ∈ ⊥