ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<VAR>this : ((f fun i => x) fun i => s.piecewise (fun x_1 => x) (fun x => y) ((sᶜ.orderEmbOfFin hl) i)) = (f fun i => x) fun x => y<GOAL>((f fun x_1 => x) fun i => s.piecewise (fun x_1 => x) (fun x => y) ((sᶜ.orderEmbOfFin hl) i)) = (f fun x_1 => x) fun x => y
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Fintype σ<VAR>f : MvPolynomial σ R<VAR>n : ℕ<VAR>h : f.totalDegree < n * Fintype.card σ<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<GOAL>∃ i, d i < n
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Fintype σ<VAR>f : MvPolynomial σ R<VAR>n : ℕ<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<VAR>h : ∀ (i : σ), n ≤ d i<GOAL>n * Fintype.card σ ≤ f.totalDegree
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : Matrix n n R[X]<VAR>r : R<VAR>i j : n<GOAL>eval ((scalar n) r) (matPolyEquiv M) i j = eval r (M i j)
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹² : Fintype m<VAR>inst✝¹¹ : Fintype m₁<VAR>inst✝¹⁰ : Fintype m₂<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype n₁<VAR>inst✝⁷ : Fintype n₂<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : DecidableEq m₁<VAR>inst✝⁴ : DecidableEq m₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq n₁<VAR>inst✝¹ : DecidableEq n₂<VAR>inst✝ : Semiring R<VAR>A₁ : Matrix n₁ n R<VAR>A₂ : Matrix n₂ n R<VAR>B₁₁ : Matrix m₁ n₁ R<VAR>B₁₂ : Matrix m₁ n₂ R<VAR>B₂₁ : Matrix m₂ n₁ R<VAR>B₂₂ : Matrix m₂ n₂ R<GOAL>fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>a b : ℕ<GOAL>eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>he : MapsTo f s e.source<GOAL>ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔ ContMDiffOn IM IB n (fun x => (f x).proj) s ∧ ContMDiffOn IM 𝓘(𝕜, F) n (fun x => (↑e (f x)).2) s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²² : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²¹ : NormedAddCommGroup EB<VAR>inst✝²⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁸ : TopologicalSpace B<VAR>inst✝¹⁷ : ChartedSpace HB B<VAR>inst✝¹⁶ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁵ : NormedAddCommGroup EM<VAR>inst✝¹⁴ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹³ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹² : TopologicalSpace M<VAR>inst✝¹¹ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹⁰ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁹ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜 F E<VAR>inst✝² : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : MemTrivializationAtlas e<VAR>inst✝ : MemTrivializationAtlas e'<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>he : MapsTo f s e.source<GOAL>(∀ x ∈ s, ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x) ↔ ∀ x ∈ s, ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x => (↑e (f x)).2) s x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : FunLike F ℚ≥0 α<VAR>inst✝ : RingHomClass F ℚ≥0 α<VAR>f : F<VAR>q : ℚ≥0<GOAL>f q = ↑q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>g : B →+* C<VAR>f : A →+* B<VAR>hg : g.FiniteType<VAR>hf : f.FiniteType<VAR>x✝² : Algebra A B := f.toAlgebra<VAR>x✝¹ : Algebra A C := (g.comp f).toAlgebra<VAR>x✝ : Algebra B C := g.toAlgebra<GOAL>(g.comp f).FiniteType
<VAR>x✝ y✝ z x : ℝ<VAR>hx : x ≤ 0<VAR>y : ℝ<GOAL>x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)
<VAR>x✝ y✝ z x : ℝ<VAR>hx : x ≤ 0<VAR>y : ℝ<VAR>h : ¬x = 0<GOAL>(↑x ^ ↑y).re = rexp (log x * y) * cos (y * π)
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖y‖₊ < ‖f y‖₊<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖y‖₊ < ‖f y‖₊<VAR>hy' : ‖y‖₊ ≠ 0<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖y‖₊ < ‖f y‖₊<VAR>hy' : ‖y‖₊ ≠ 0<VAR>hfy : ‖f y‖₊ ≠ 0<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹<VAR>hy' : ‖y‖₊ ≠ 0<VAR>hfy : ‖f y‖₊ ≠ 0<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹<VAR>hy' : ‖y‖₊ ≠ 0<VAR>hfy : ‖f y‖₊ ≠ 0<VAR>k : 𝕜<VAR>hk₁ : r * ‖f y‖₊⁻¹ < ‖k‖₊<VAR>hk₂ : ‖k‖₊ < ‖y‖₊⁻¹<GOAL>∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹<VAR>hy' : ‖y‖₊ ≠ 0<VAR>hfy : ‖f y‖₊ ≠ 0<VAR>k : 𝕜<VAR>hk₁ : r * ‖f y‖₊⁻¹ < ‖k‖₊<VAR>hk₂ : ‖k‖₊ < ‖y‖₊⁻¹<GOAL>r < ‖f (k • y)‖₊
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<VAR>y : E<VAR>hy : r * ‖f y‖₊⁻¹ < ‖y‖₊⁻¹<VAR>hy' : ‖y‖₊ ≠ 0<VAR>hfy : ‖f y‖₊ ≠ 0<VAR>k : 𝕜<VAR>hk₁ : r * ‖f y‖₊⁻¹ < ‖k‖₊<VAR>hk₂ : ‖k‖₊ < ‖y‖₊⁻¹<VAR>this : ‖σ₁₂ k‖₊ = ‖k‖₊<GOAL>r < ‖f (k • y)‖₊
<VAR>R : Type u_1<VAR>inst✝²³ : CommSemiring R<VAR>R₂ : Type u_2<VAR>inst✝²² : CommSemiring R₂<VAR>R₃ : Type u_3<VAR>inst✝²¹ : CommSemiring R₃<VAR>R₄ : Type u_4<VAR>inst✝²⁰ : CommSemiring R₄<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Q : Type u_8<VAR>Mₗ : Type u_9<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>Qₗ : Type u_12<VAR>Qₗ' : Type u_13<VAR>inst✝¹⁹ : AddCommMonoid M<VAR>inst✝¹⁸ : AddCommMonoid N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : AddCommMonoid Q<VAR>inst✝¹⁵ : AddCommMonoid Mₗ<VAR>inst✝¹⁴ : AddCommMonoid Nₗ<VAR>inst✝¹³ : AddCommMonoid Pₗ<VAR>inst✝¹² : AddCommMonoid Qₗ<VAR>inst✝¹¹ : AddCommMonoid Qₗ'<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R₂ N<VAR>inst✝⁸ : Module R₃ P<VAR>inst✝⁷ : Module R₄ Q<VAR>inst✝⁶ : Module R Mₗ<VAR>inst✝⁵ : Module R Nₗ<VAR>inst✝⁴ : Module R Pₗ<VAR>inst✝³ : Module R Qₗ<VAR>inst✝² : Module R Qₗ'<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>σ₄₂ : R₄ →+* R₂<VAR>σ₄₃ : R₄ →+* R₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃<VAR>f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>((f.compl₂ id) x✝¹) x✝ = (f x✝¹) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ t : Set α<VAR>inst✝² : Fintype α<VAR>s : Set α<VAR>inst✝¹ : Fintype ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a✝ : α<GOAL>a✝ ∈ filter (fun x => x ∈ s) Finset.univ ↔ a✝ ∈ s.toFinset
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>x y : WithLp p ((i : ι) → β i)<GOAL>edist x y ≤ ↑(↑(Fintype.card ι) ^ (1 / p).toReal) * edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝² : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Fact (1 ≤ ⊤)<VAR>x y : WithLp ⊤ ((i : ι) → β i)<GOAL>edist x y ≤ ↑(↑(Fintype.card ι) ^ (1 / ⊤).toReal) * edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) y)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p)<VAR>inst✝² : (i : ι) → PseudoMetricSpace (α i)<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)<VAR>inst✝ : Fintype ι<VAR>x y : WithLp p ((i : ι) → β i)<VAR>h : 1 ≤ p.toReal<GOAL>edist x y ≤ ↑(↑(Fintype.card ι) ^ (1 / p).toReal) * edist ((WithLp.equiv p ((i : ι) → β i)) x) ((WithLp.equiv p ((i : ι) → β i)) y)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A✝ : Matrix (l ⊕ l) (l ⊕ l) R<VAR>A : ↥(symplecticGroup l R)<GOAL>↑A⁻¹ = (↑A)⁻¹
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A✝ : Matrix (l ⊕ l) (l ⊕ l) R<VAR>A : ↥(symplecticGroup l R)<GOAL>-J l R * (↑A)ᵀ * J l R * ↑A = 1
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>f : ι → S[X]<GOAL>(∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (natDegree ∘ f) s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : T2Space R<GOAL>T2Space V
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : T2Space R<VAR>x y : V<VAR>hxy : x ≠ y<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : T2Space R<VAR>x y : V<VAR>hxy : x ≠ y<VAR>f : V →L[R] R<VAR>hf : f x ≠ f y<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<GOAL>DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x
<VAR>n₁ n₂ d₁ d₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ - n₂ /. d₂ = (n₁ * d₂ - n₂ * d₁) /. (d₁ * d₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (b : β), g b ∂(κ.withDensity f) a = ∫⁻ (b : β), f a b * g b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (a_1 : β), (f a * g) a_1 ∂κ a = ∫⁻ (b : β), f a b * g b ∂κ a
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 f<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖<VAR>x✝ : E × F<VAR>x : E<VAR>y : F<GOAL>‖f (x, y)‖ ≤ ?m.259612 C Cpos hC * ‖‖(x, y).1‖ * ‖(x, y).2‖‖
<VAR>m n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>n ∣ b + d - (a + c)
<VAR>m n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : c ≡ d [ZMOD n]<GOAL>b + d - (a + c) = b - a + (d - c)
<VAR>α : Type u_1<VAR>n m : Nat<VAR>l : List α<GOAL>dropSlice n m l = dropSliceTR n m l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>m✝ : Nat<GOAL>dropSlice n 0 l = l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>m✝¹ m✝ : Nat<GOAL>dropSlice n m✝.succ l = dropSliceTR.go l m✝ l n #[]
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>m✝ m : Nat<GOAL>dropSlice n m.succ l = dropSliceTR.go l m l n #[]
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<GOAL>IsCoatom s ↔ ∃ x, s = {x}ᶜ
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<GOAL>(∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : gcd x y = 0<GOAL>x ∣ lcm x y