ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>hδ : (1 + C' * ‖f‖) * δ < ε<VAR>g : G<VAR>hg : ‖hatg - ↑G g‖ < δ<VAR>g' : G<VAR>hgg' : f g' = f g<VAR>hfg : ‖g'‖ ≤ C' * ‖f g‖<VAR>mem_ker : g - g' ∈ f.ker<GOAL>∃ b ∈ ↑(toCompl.comp (incl f.ker)).range, ‖hatg - b‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>hδ : (1 + C' * ‖f‖) * δ < ε<VAR>g : G<VAR>hg : ‖hatg - ↑G g‖ < δ<VAR>g' : G<VAR>hgg' : f g' = f g<VAR>hfg : ‖g'‖ ≤ C' * ‖f g‖<VAR>mem_ker : g - g' ∈ f.ker<GOAL>‖hatg - (toCompl.comp (incl f.ker)).toAddMonoidHom ⟨g - g', mem_ker⟩‖ < ε
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>C : ℝ<VAR>h : f.SurjectiveOnWith f.range C<VAR>hatg : Completion G<VAR>hatg_in : f.completion hatg = 0<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>C' : ℝ<VAR>C'_pos : C' > 0<VAR>hC' : f.SurjectiveOnWith f.range C'<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>hδ : (1 + C' * ‖f‖) * δ < ε<VAR>g : G<VAR>hg : ‖hatg - ↑G g‖ < δ<VAR>g' : G<VAR>hgg' : f g' = f g<VAR>hfg : ‖g'‖ ≤ C' * ‖f g‖<VAR>mem_ker : g - g' ∈ f.ker<VAR>this : ‖f g‖ ≤ ‖f‖ * δ<GOAL>‖hatg - (toCompl.comp (incl f.ker)).toAddMonoidHom ⟨g - g', mem_ker⟩‖ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s ×ˢ s \ s.diag = s.offDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ di : DenseInducing i<VAR>s : Set α<GOAL>Dense (i '' s) ↔ Dense s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ di : DenseInducing i<VAR>s : Set α<VAR>H : Dense (i '' s)<VAR>x : α<GOAL>x ∈ closure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ di : DenseInducing i<VAR>s : Set α<VAR>H : Dense (i '' s)<VAR>x : α<GOAL>x ∈ univ
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>1 ^ ↑n = 1
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>1 ^ -[n+1] = 1
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>inst✝ : RegularSpace X✝<VAR>x : X✝<VAR>s : Set X✝<VAR>X : Type u_3<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : RegularSpace X<VAR>h₂ : RegularSpace X<GOAL>RegularSpace X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a✝ b : α<VAR>f : α → β<VAR>a : α<GOAL>(map f (char a)).matches' = (Language.map f) (char a).matches'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a✝ b : α<VAR>f : α → β<VAR>a : α<GOAL>(Language.map f) (char a).matches' = (map f (char a)).matches'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R S : RegularExpression α<GOAL>(map f (R + S)).matches' = (Language.map f) (R + S).matches'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R S : RegularExpression α<GOAL>(Language.map f) R.matches' + (Language.map f) S.matches' = (Language.map f) (R.matches' + S.matches')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R S : RegularExpression α<GOAL>(map f (R.comp S)).matches' = (Language.map f) (R.comp S).matches'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R S : RegularExpression α<GOAL>(Language.map f) R.matches' * (Language.map f) S.matches' = (Language.map f) (R.comp S).matches'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R : RegularExpression α<GOAL>((Language.map f) R.matches')∗ = (Language.map f) R.matches'∗
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R : RegularExpression α<GOAL>⨆ i, (Language.map f) R.matches' ^ i = (Language.map f) (⨆ i, R.matches' ^ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>f : α → β<VAR>R : RegularExpression α<GOAL>⨆ i, (Language.map f) (R.matches' ^ i) = (Language.map f) (⨆ i, R.matches' ^ i)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t✝ u t : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<GOAL>(condCount s) t + (condCount s) tᶜ = 1
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>m : M<VAR>a : α<VAR>n : ℕ<GOAL>IsPeriodicPt (fun x => m • x) n a ↔ m ^ n • a = a
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ u v : Set α<VAR>inst✝ : Countable ι<VAR>t : ι → Set α<GOAL>AEDisjoint μ s (⋃ i, t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)
<VAR>n : ℕ<VAR>x : PartENat<GOAL>↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ x.get h
<VAR>n : ℕ<VAR>x : PartENat<GOAL>(∀ (hy : x.Dom), (↑n).get ⋯ ≤ x.get hy) ↔ ∀ (h : x.Dom), n ≤ x.get h
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.negAddY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.negAddY P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>-(u ^ 3 * P y) * (v ^ 2 * Q x) ^ 3 * (u * P z) ^ 3 + 2 * (u ^ 3 * P y) * (v ^ 3 * Q y) ^ 2 * (u * P z) ^ 3 - 3 * (u ^ 2 * P x) ^ 2 * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 2 * (v * Q z) + 3 * (u ^ 2 * P x) * (u ^ 3 * P y) * (v ^ 2 * Q x) ^ 2 * (u * P z) * (v * Q z) ^ 2 + (u ^ 2 * P x) ^ 3 * (v ^ 3 * Q y) * (v * Q z) ^ 3 - 2 * (u ^ 3 * P y) ^ 2 * (v ^ 3 * Q y) * (v * Q z) ^ 3 + W'.a₁ * (u ^ 2 * P x) * (v ^ 3 * Q y) ^ 2 * (u * P z) ^ 4 + W'.a₁ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 3 * (v * Q z) - W'.a₁ * (u ^ 2 * P x) * (u ^ 3 * P y) * (v ^ 3 * Q y) * (u * P z) * (v * Q z) ^ 3 - W'.a₁ * (u ^ 3 * P y) ^ 2 * (v ^ 2 * Q x) * (v * Q z) ^ 4 - 2 * W'.a₂ * (u ^ 2 * P x) * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) + 2 * W'.a₂ * (u ^ 2 * P x) * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) * (v * Q z) ^ 4 + W'.a₃ * (v ^ 3 * Q y) ^ 2 * (u * P z) ^ 6 - W'.a₃ * (u ^ 3 * P y) ^ 2 * (v * Q z) ^ 6 - W'.a₄ * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 6 * (v * Q z) - W'.a₄ * (u ^ 2 * P x) * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) ^ 3 + W'.a₄ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) ^ 3 * (v * Q z) ^ 4 + W'.a₄ * (u ^ 2 * P x) * (u ^ 3 * P y) * (u * P z) * (v * Q z) ^ 6 - 2 * W'.a₆ * (v ^ 3 * Q y) * (u * P z) ^ 6 * (v * Q z) ^ 3 + 2 * W'.a₆ * (u ^ 3 * P y) * (u * P z) ^ 3 * (v * Q z) ^ 6 = ((u * v) ^ 2) ^ 3 * (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z + 3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 + P x ^ 3 * Q y * Q z ^ 3 - 2 * P y ^ 2 * Q y * Q z ^ 3 + W'.a₁ * P x * Q y ^ 2 * P z ^ 4 + W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z - W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 - W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 - 2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z + 2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 + W'.a₃ * Q y ^ 2 * P z ^ 6 - W'.a₃ * P y ^ 2 * Q z ^ 6 - W'.a₄ * Q x * Q y * P z ^ 6 * Q z - W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 + W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 + W'.a₄ * P x * P y * P z * Q z ^ 6 - 2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 + 2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>N₁ : Type u_6<VAR>inst✝⁶ : AddCommMonoid N₁<VAR>inst✝⁵ : Module R N₁<VAR>N₂ : Type u_7<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N₂<VAR>N : Type u_8<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>inst✝ : DecidableEq (ι₁ ⊕ ι₂)<VAR>x✝ : ι₁ ⊕ ι₂ → N<VAR>i : ι₁ ⊕ ι₂<VAR>p q : N<GOAL>(fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) = (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i p) + (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i q)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>N₁ : Type u_6<VAR>inst✝⁶ : AddCommMonoid N₁<VAR>inst✝⁵ : Module R N₁<VAR>N₂ : Type u_7<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N₂<VAR>N : Type u_8<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>inst✝ : DecidableEq (ι₁ ⊕ ι₂)<VAR>x✝ : ι₁ ⊕ ι₂ → N<VAR>i : ι₁ ⊕ ι₂<VAR>p q : N<VAR>this : DecidableEq ι₁ := ⋯.decidableEq<GOAL>(fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) = (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i p) + (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i q)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>N₁ : Type u_6<VAR>inst✝⁶ : AddCommMonoid N₁<VAR>inst✝⁵ : Module R N₁<VAR>N₂ : Type u_7<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N₂<VAR>N : Type u_8<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>inst✝ : DecidableEq (ι₁ ⊕ ι₂)<VAR>x✝ : ι₁ ⊕ ι₂ → N<VAR>i : ι₁ ⊕ ι₂<VAR>p q : N<VAR>this✝ : DecidableEq ι₁ := ⋯.decidableEq<VAR>this : DecidableEq ι₂ := ⋯.decidableEq<GOAL>(fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i (p + q)) = (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i p) + (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i q)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>N₁ : Type u_6<VAR>inst✝⁶ : AddCommMonoid N₁<VAR>inst✝⁵ : Module R N₁<VAR>N₂ : Type u_7<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N₂<VAR>N : Type u_8<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>inst✝ : DecidableEq (ι₁ ⊕ ι₂)<VAR>x✝ : ι₁ ⊕ ι₂ → N<VAR>i : ι₁ ⊕ ι₂<VAR>c : R<VAR>p : N<GOAL>(fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) = c • (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i p)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>N₁ : Type u_6<VAR>inst✝⁶ : AddCommMonoid N₁<VAR>inst✝⁵ : Module R N₁<VAR>N₂ : Type u_7<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N₂<VAR>N : Type u_8<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>inst✝ : DecidableEq (ι₁ ⊕ ι₂)<VAR>x✝ : ι₁ ⊕ ι₂ → N<VAR>i : ι₁ ⊕ ι₂<VAR>c : R<VAR>p : N<VAR>this : DecidableEq ι₁ := ⋯.decidableEq<GOAL>(fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) = c • (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i p)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>N₁ : Type u_6<VAR>inst✝⁶ : AddCommMonoid N₁<VAR>inst✝⁵ : Module R N₁<VAR>N₂ : Type u_7<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N₂<VAR>N : Type u_8<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>inst✝ : DecidableEq (ι₁ ⊕ ι₂)<VAR>x✝ : ι₁ ⊕ ι₂ → N<VAR>i : ι₁ ⊕ ι₂<VAR>c : R<VAR>p : N<VAR>this✝ : DecidableEq ι₁ := ⋯.decidableEq<VAR>this : DecidableEq ι₂ := ⋯.decidableEq<GOAL>(fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i (c • p)) = c • (fun v => (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)) (Function.update x✝ i p)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(ρ_ (X₁ ⊗ X₂)).hom = (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv ≫ X₁ ◁ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<VAR>this : (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv = (α_ X₁ X₂ (𝟙_ C)).hom ≫ X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C<GOAL>(ρ_ (X₁ ⊗ X₂)).hom = (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv ≫ X₁ ◁ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<VAR>this : (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv = (α_ X₁ X₂ (𝟙_ C)).hom ≫ X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C<GOAL>(ρ_ (X₁ ⊗ X₂)).hom = (((((α_ X₁ X₂ (𝟙_ C)).hom ≫ X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) ≫ X₁ ◁ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ C) ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(ρ_ (X₁ ⊗ X₂)).hom = (((((α_ X₁ X₂ (𝟙_ C)).hom ≫ X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) ≫ X₁ ◁ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ C) ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(ρ_ (X₁ ⊗ X₂)).hom = (α_ X₁ X₂ (𝟙_ C)).hom ≫ ((X₁ ◁ (λ_ X₂).inv ▷ 𝟙_ C ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : Subsingleton R<VAR>p : MvPolynomial σ R<GOAL>p.coeffs = ∅
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : LinearOrder E<VAR>inst✝¹ : Zero E<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ ℝ<VAR>a✝ : α<GOAL>↑(map norm f.posPart) a✝ = ↑f.posPart a✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : LinearOrder E<VAR>inst✝¹ : Zero E<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ ℝ<VAR>a✝ : α<GOAL>0 ≤ ↑f.posPart a✝
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<GOAL>EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<VAR>this : Inducing (⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)<GOAL>EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<VAR>this : Inducing (⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)<GOAL>ContinuousWithinAt ((⇑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑UniformFun.ofFun ∘ swap F) S x₀ ↔ ContinuousWithinAt (⇑UniformFun.ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) S x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<GOAL>𝓝[∅] a = ⊥
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℕ → ℝ<VAR>cone : ∀ (n : ℕ), 1 < c n<VAR>clim : Tendsto c atTop (𝓝 1)<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℕ → ℝ<VAR>cone : ∀ (n : ℕ), 1 < c n<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>this : ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<GOAL>∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℕ → ℝ<VAR>cone : ∀ (n : ℕ), 1 < c n<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>this : ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), Tendsto (fun n => (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<GOAL>Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℕ → ℝ<VAR>cone : ∀ (n : ℕ), 1 < c n<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>this : ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), Tendsto (fun n => (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<GOAL>Monotone fun n => ∑ i ∈ range n, X i ω
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℕ → ℝ<VAR>cone : ∀ (n : ℕ), 1 < c n<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>this : ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), Tendsto (fun n => (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))<GOAL>∀ (k : ℕ), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
<VAR>a x z✝ z : ℂ<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : 0 ≤ z.re<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : 0 ≤ z.im<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.im
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im < 0<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.im
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>(s ○ t).Nonempty → t.Nonempty
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>(∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ t
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>h : x ≠ 0<GOAL>∃ x_1 y, x_1 ≠ y