ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : NormedAddCommGroup F✝<VAR>inst✝¹ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝ : SecondCountableTopology F✝<VAR>f : E → F✝<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F✝<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F✝) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0<VAR>hs : s.Nonempty<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>M : ℕ → ↑T → Set E := fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}<VAR>s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z<VAR>closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z<VAR>d : ℕ → E<VAR>hd : DenseRange d<VAR>K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)<VAR>K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))<VAR>K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)<VAR>F : ℕ → ℕ × ↑T × ℕ<VAR>hF : Function.Surjective F<VAR>x : E<VAR>xs : x ∈ s<GOAL>x ∈ ⋃ n, (fun q => K (F q).1 (F q).2.1 (F q).2.2) n
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : NormedAddCommGroup F✝<VAR>inst✝¹ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝ : SecondCountableTopology F✝<VAR>f : E → F✝<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F✝<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F✝) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0<VAR>hs : s.Nonempty<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>M : ℕ → ↑T → Set E := fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}<VAR>s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z<VAR>closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z<VAR>d : ℕ → E<VAR>hd : DenseRange d<VAR>K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)<VAR>K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))<VAR>K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)<VAR>F : ℕ → ℕ × ↑T × ℕ<VAR>hF : Function.Surjective F<VAR>x : E<VAR>xs : x ∈ s<VAR>n : ℕ<VAR>z : ↑T<VAR>hnz : x ∈ M n z<GOAL>x ∈ ⋃ n, (fun q => K (F q).1 (F q).2.1 (F q).2.2) n
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : NormedAddCommGroup F✝<VAR>inst✝¹ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝ : SecondCountableTopology F✝<VAR>f : E → F✝<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F✝<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F✝) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0<VAR>hs : s.Nonempty<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>M : ℕ → ↑T → Set E := fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}<VAR>s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z<VAR>closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z<VAR>d : ℕ → E<VAR>hd : DenseRange d<VAR>K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)<VAR>K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))<VAR>K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)<VAR>F : ℕ → ℕ × ↑T × ℕ<VAR>hF : Function.Surjective F<VAR>x : E<VAR>xs : x ∈ s<VAR>n : ℕ<VAR>z : ↑T<VAR>hnz : x ∈ M n z<VAR>p : ℕ<VAR>hp : x ∈ closedBall (d p) (u n / 3)<GOAL>x ∈ ⋃ n, (fun q => K (F q).1 (F q).2.1 (F q).2.2) n
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : NormedAddCommGroup F✝<VAR>inst✝¹ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝ : SecondCountableTopology F✝<VAR>f : E → F✝<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F✝<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F✝) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0<VAR>hs : s.Nonempty<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>M : ℕ → ↑T → Set E := fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}<VAR>s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z<VAR>closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z<VAR>d : ℕ → E<VAR>hd : DenseRange d<VAR>K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)<VAR>K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))<VAR>K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)<VAR>F : ℕ → ℕ × ↑T × ℕ<VAR>hF : Function.Surjective F<VAR>x : E<VAR>xs : x ∈ s<VAR>n : ℕ<VAR>z : ↑T<VAR>hnz : x ∈ M n z<VAR>p : ℕ<VAR>hp : x ∈ closedBall (d p) (u n / 3)<VAR>q : ℕ<VAR>hq : F q = (n, z, p)<GOAL>x ∈ ⋃ n, (fun q => K (F q).1 (F q).2.1 (F q).2.2) n
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : NormedAddCommGroup F✝<VAR>inst✝¹ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝ : SecondCountableTopology F✝<VAR>f : E → F✝<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F✝<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F✝) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0<VAR>hs : s.Nonempty<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>M : ℕ → ↑T → Set E := fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}<VAR>s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z<VAR>closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z<VAR>d : ℕ → E<VAR>hd : DenseRange d<VAR>K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)<VAR>K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))<VAR>K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)<VAR>F : ℕ → ℕ × ↑T × ℕ<VAR>hF : Function.Surjective F<VAR>x : E<VAR>xs : x ∈ s<VAR>n : ℕ<VAR>z : ↑T<VAR>hnz : x ∈ M n z<VAR>p : ℕ<VAR>hp : x ∈ closedBall (d p) (u n / 3)<VAR>q : ℕ<VAR>hq : F q = (n, z, p)<GOAL>x ∈ K (F q).1 (F q).2.1 (F q).2.2
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : NormedAddCommGroup F✝<VAR>inst✝¹ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝ : SecondCountableTopology F✝<VAR>f : E → F✝<VAR>s : Set E<VAR>f' : E → E →L[ℝ] F✝<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>r : (E →L[ℝ] F✝) → ℝ≥0<VAR>rpos : ∀ (A : E →L[ℝ] F✝), r A ≠ 0<VAR>hs : s.Nonempty<VAR>T : Set ↑s<VAR>T_count : T.Countable<VAR>hT : ⋃ x ∈ T, ball (f' ↑x) ↑(r (f' ↑x)) = ⋃ x, ball (f' ↑x) ↑(r (f' ↑x))<VAR>u : ℕ → ℝ<VAR>left✝ : StrictAnti u<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>M : ℕ → ↑T → Set E := fun n z => {x | x ∈ s ∧ ∀ y ∈ s ∩ ball x (u n), ‖f y - f x - (f' ↑↑z) (y - x)‖ ≤ ↑(r (f' ↑↑z)) * ‖y - x‖}<VAR>s_subset : ∀ x ∈ s, ∃ n z, x ∈ M n z<VAR>closure_M_subset : ∀ (n : ℕ) (z : ↑T), s ∩ closure (M n z) ⊆ M n z<VAR>d : ℕ → E<VAR>hd : DenseRange d<VAR>K : ℕ → ↑T → ℕ → Set E := fun n z p => closure (M n z) ∩ closedBall (d p) (u n / 3)<VAR>K_approx : ∀ (n : ℕ) (z : ↑T) (p : ℕ), ApproximatesLinearOn f (f' ↑↑z) (s ∩ K n z p) (r (f' ↑↑z))<VAR>K_closed : ∀ (n : ℕ) (z : ↑T) (p : ℕ), IsClosed (K n z p)<VAR>F : ℕ → ℕ × ↑T × ℕ<VAR>hF : Function.Surjective F<VAR>x : E<VAR>xs : x ∈ s<VAR>n : ℕ<VAR>z : ↑T<VAR>hnz : x ∈ M n z<VAR>p : ℕ<VAR>hp : x ∈ closedBall (d p) (u n / 3)<VAR>q : ℕ<VAR>hq : F q = (n, z, p)<GOAL>x ∈ closure (M n z)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MonoidWithZero M₀<VAR>l✝ : List M₀<VAR>a : M₀<VAR>l : List M₀<VAR>h : 0 ∈ a :: l<GOAL>(a :: l).prod = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MonoidWithZero M₀<VAR>l✝ : List M₀<VAR>a : M₀<VAR>l : List M₀<VAR>h : 0 ∈ a :: l<GOAL>a * l.prod = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MonoidWithZero M₀<VAR>l✝ : List M₀<VAR>a : M₀<VAR>l : List M₀<VAR>h : 0 ∈ a :: l<VAR>ha : 0 = a<GOAL>a * l.prod = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MonoidWithZero M₀<VAR>l✝ : List M₀<VAR>a : M₀<VAR>l : List M₀<VAR>h : 0 ∈ a :: l<VAR>hl : 0 ∈ l<GOAL>a * l.prod = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>inst✝² : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)<VAR>s : Set α<GOAL>Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>inst✝² : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)<VAR>s : Set α<GOAL>Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>inst✝² : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_6<VAR>f : α → G<VAR>hfi : Integrable f μ<VAR>F : ι → α → G<VAR>l : Filter ι<VAR>hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ<VAR>s : Set α<VAR>hF : Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)<GOAL>Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (𝓝 0)
<VAR>p q✝ : ℚ<VAR>q : ℚ≥0<VAR>hq : 0 < q<VAR>hp : p < 0<GOAL>q ≤ p.toNNRat ↔ ↑q ≤ p
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝ : K.HasTotal (up ℤ)<VAR>b n a' : ℤ<VAR>ha' : a' + b = n + x<VAR>h : a' - x + b = n<GOAL>(K.ιTotal (up ℤ) a' b (n + x) ha' ≫ 𝟙 ((K.total (up ℤ)).X (n + x)) ≫ K.totalDesc fun p q hpq => eqToHom ⋯ ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n ⋯) = eqToHom ⋯ ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (a' - x) b n h
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>hucard : u.card = m * 4 ^ P.parts.card + a<GOAL>(4 ^ P.parts.card - a) * m + a * (m + 1) = u.card
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>c c' c₀ : C<VAR>f : IsFiltered.max (F.obj c) (F.obj c') ⟶ F.obj c₀<GOAL>∃ Z x x, True
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>c c' : C<VAR>f g : c ⟶ c'<VAR>c₀ : C<VAR>f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀<GOAL>∃ Z h, f ≫ h = g ≫ h
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>c c' : C<VAR>f g : c ⟶ c'<VAR>c₀ : C<VAR>f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀<GOAL>F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) = F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>h : ∀ (e e' : PartialHomeomorph M H), e ∈ atlas H M → e' ∈ atlas H M → ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)<GOAL>∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid ⊤ I
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>h : ∀ (e e' : PartialHomeomorph M H), e ∈ atlas H M → e' ∈ atlas H M → ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)<VAR>this : HasGroupoid M (contDiffGroupoid ⊤ I)<GOAL>∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid ⊤ I
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h = (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h = F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ ((α_ f g h).hom ≫ (α_ f g h).inv)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : y ∈ interior s<VAR>t : 𝕜<VAR>ht : t ∈ Ioc 0 1<GOAL>x + t • (y - x) ∈ interior s
<VAR>T : ℝ<VAR>m n : ℤ<VAR>x : AddCircle T<GOAL>(fourier (m + n)) x = (fourier m) x * (fourier n) x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>m n : ℕ<VAR>s : Simplex ℝ P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).circumsphere = s.circumsphere
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>m n : ℕ<VAR>s : Simplex ℝ P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).circumsphere.center ∈ affineSpan ℝ (Set.range (s.reindex e).points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>m n : ℕ<VAR>s : Simplex ℝ P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<GOAL>mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom = (mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>b : B<GOAL>range (mk b) = proj ⁻¹' {b}
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>b : B<GOAL>range (mk b) ⊆ proj ⁻¹' {b}
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>E : B → Type u_3<VAR>b : B<GOAL>proj ⁻¹' {b} ⊆ range (mk b)
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>β : Type u_3<VAR>p : β → Prop<VAR>f : β → ℝ<VAR>hf₀ : ∀ (i : β), p i → 0 < f i<VAR>hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε<GOAL>(𝓤 α).HasBasis p fun i => {p | dist p.1 p.2 < f i}
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>β : Type u_3<VAR>p : β → Prop<VAR>f : β → ℝ<VAR>hf₀ : ∀ (i : β), p i → 0 < f i<VAR>hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε<VAR>s : Set (α × α)<GOAL>(∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>inst✝ : Nonempty Z<VAR>hε : 0 < ε<VAR>s : Set ((X ⊕ Y) × (X ⊕ Y))<GOAL>s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>inst✝ : Nonempty Z<VAR>hε : 0 < ε<VAR>s : Set ((X ⊕ Y) × (X ⊕ Y))<GOAL>((∃ ε > 0, ∀ {a b : X}, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧ ∃ ε > 0, ∀ {a b : Y}, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)<VAR>m : (i : Fin n) → M i.castSucc<VAR>x : M (last n)<GOAL>(f.uncurryRight.curryRight m) x = (f m) x
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)<VAR>m : (i : Fin n) → M i.castSucc<VAR>x : M (last n)<GOAL>(f (init (snoc m x))) x = (f m) x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>volume (fundamentalDomain (stdBasis K)) = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>NullMeasurableSet (Set.univ.pi fun x => Set.Ico 0 1) volume
<VAR>z y✝ x✝ : ℝ<VAR>x y : ℂ<GOAL>dist y x < 1 → dist (cexp y) (cexp x) ≤ 2 * ‖cexp x‖ * dist y x
<VAR>z y✝ x✝ : ℝ<VAR>x y : ℂ<VAR>a✝ : ‖y - x‖ < 1<GOAL>2 * ‖cexp x‖ * dist y x = (1 + 1) * ‖cexp x‖ * ‖y - x‖
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<GOAL>evenKernel (↑a) x = 1 / x ^ (1 / 2) * cosKernel (↑a) (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<GOAL>cexp (-↑π * ↑a ^ 2 * ↑x) * (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : I * ↑(1 / x) = -1 / (I * ↑x)<GOAL>cexp (-↑π * ↑a ^ 2 * ↑x) * (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : I * ↑(1 / x) = -1 / (I * ↑x)<VAR>hx' : I * ↑x ≠ 0<GOAL>cexp (-↑π * ↑a ^ 2 * ↑x) * (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : I * ↑(1 / x) = -1 / (I * ↑x)<VAR>hx' : I * ↑x ≠ 0<VAR>h2 : ↑a * I * ↑x / (I * ↑x) = ↑a<GOAL>cexp (-↑π * ↑a ^ 2 * ↑x) * (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : I * ↑(1 / x) = -1 / (I * ↑x)<VAR>hx' : I * ↑x ≠ 0<VAR>h2 : ↑a * I * ↑x / (I * ↑x) = ↑a<VAR>h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))<GOAL>cexp (-↑π * ↑a ^ 2 * ↑x) * (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : I * ↑(1 / x) = -1 / (I * ↑x)<VAR>hx' : I * ↑x ≠ 0<VAR>h2 : ↑a * I * ↑x / (I * ↑x) = ↑a<VAR>h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))<VAR>h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)<GOAL>cexp (-↑π * ↑a ^ 2 * ↑x) * (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
<VAR>z : ℂ<GOAL>(z * (starRingEnd ℂ) z).re = (↑(normSq z)).re ∧ (z * (starRingEnd ℂ) z).im = (↑(normSq z)).im
<VAR>S : Type u_1<VAR>inst✝ : UnitalShelf S<VAR>x y : S<GOAL>x ◃ x ◃ y = x ◃ y
<VAR>S : Type u_1<VAR>inst✝ : UnitalShelf S<VAR>x y : S<VAR>h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y<GOAL>x ◃ x ◃ y = x ◃ y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + k
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>t : Finset α<VAR>x✝ : t ∈ 𝒜<VAR>hst : t✝ ⊆ t<GOAL>(t \ t✝).card = k ↔ t.card = t✝.card + k