ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>h : IsClosed (range f)<VAR>t : Set Y<VAR>ht : IsClosed t<VAR>hs : IsClosed (f ⁻¹' t)<GOAL>IsClosed (t ∩ range f)
<VAR>a b c p q✝ q : ℚ<GOAL>|q| = ↑q.num.natAbs /. ↑q.den
<VAR>a b c p q✝ q : ℚ<VAR>hq : q ≤ 0<GOAL>|q| = ↑q.num.natAbs /. ↑q.den
<VAR>a b c p q✝ q : ℚ<VAR>hq : 0 ≤ q<GOAL>|q| = ↑q.num.natAbs /. ↑q.den
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i j k : Fin 2<VAR>hjk : 0 ≤ k<VAR>hij : 0 ≤ 0<GOAL>map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i j k : Fin 2<VAR>hjk : 1 ≤ k<VAR>hij : 0 ≤ 1<GOAL>map f 0 k ⋯ = map f 0 1 hij ≫ map f 1 k hjk
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i j : Fin 2<VAR>hij : 0 ≤ 1<VAR>hjk : 1 ≤ 1<GOAL>map f 0 1 ⋯ = map f 0 1 hij ≫ map f 1 1 hjk
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i j k : Fin 2<VAR>hjk : j ≤ k<VAR>hij : 1 ≤ j<GOAL>map f 1 k ⋯ = map f 1 j hij ≫ map f j k hjk
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i k : Fin 2<VAR>hjk : 1 ≤ k<VAR>hij : 1 ≤ 1<GOAL>map f 1 k ⋯ = map f 1 1 hij ≫ map f 1 k hjk
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i : Fin 2<VAR>hij hjk : 1 ≤ 1<GOAL>map f 1 1 ⋯ = map f 1 1 hij ≫ map f 1 1 hjk
<VAR>I : Type u<VAR>inst✝³ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X₁ X₂ : GradedObject I C<VAR>inst✝ : X₁.HasTensor X₂<VAR>A : C<VAR>k : I<VAR>f : (i₁ i₂ : I) → i₁ + i₂ = k → (X₁ i₁ ⊗ X₂ i₂ ⟶ A)<VAR>i₁ i₂ : I<VAR>hi : i₁ + i₂ = k<GOAL>ιTensorObj X₁ X₂ i₁ i₂ k hi ≫ tensorObjDesc f = f i₁ i₂ hi
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>IntervalIntegrable (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 Y
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>IntegrableOn (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (Ioc 0 Y) volume
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>HasFiniteIntegral (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>HasFiniteIntegral (fun a => ‖s * (↑(rexp (-a)) * ↑a ^ (s - 1))‖) (volume.restrict (Ioc 0 Y))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>HasFiniteIntegral (fun a => abs s * (abs ↑(rexp (-a)) * abs (↑a ^ (s - 1)))) (volume.restrict (Ioc 0 Y))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>(fun x => rexp (-x) * x ^ (s.re - 1)) =ᶠ[ae (volume.restrict (Ioc 0 Y))] fun a => abs ↑(rexp (-a)) * abs (↑a ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = abs ↑(rexp (-x)) * abs (↑x ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>Y : ℝ<VAR>hY : 0 ≤ Y<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))<GOAL>MeasurableSet (Ioc 0 Y)
<VAR>x y z : ZFSet<VAR>hy : y ∈ ⋂₀ x<VAR>hz : z ∈ x<GOAL>y ∈ z
<VAR>y z : ZFSet<VAR>hy : y ∈ ⋂₀ ∅<VAR>hz : z ∈ ∅<GOAL>y ∈ z
<VAR>x y z : ZFSet<VAR>hy : y ∈ ⋂₀ x<VAR>hz : z ∈ x<VAR>hx : x.Nonempty<GOAL>y ∈ z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set (Set α)<VAR>hs : s.Countable<GOAL>(⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing T<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁶ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra L F<VAR>inst✝² : Algebra R F<VAR>inst✝¹ : IsScalarTower R L F<VAR>inst✝ : FiniteDimensional L F<VAR>x : F<VAR>hx : IsIntegral R x<GOAL>IsIntegral R ((trace L F) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing T<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁶ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra L F<VAR>inst✝² : Algebra R F<VAR>inst✝¹ : IsScalarTower R L F<VAR>inst✝ : FiniteDimensional L F<VAR>x : F<VAR>hx : IsIntegral R x<VAR>hx' : IsIntegral L x<GOAL>IsIntegral R ((trace L F) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing T<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁶ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra L F<VAR>inst✝² : Algebra R F<VAR>inst✝¹ : IsScalarTower R L F<VAR>inst✝ : FiniteDimensional L F<VAR>x : F<VAR>hx : IsIntegral R x<VAR>hx' : IsIntegral L x<GOAL>IsIntegral R (finrank (↥L⟮x⟯) F • ((minpoly L x).aroots (AlgebraicClosure F)).sum)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing T<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁶ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : Algebra L F<VAR>inst✝² : Algebra R F<VAR>inst✝¹ : IsScalarTower R L F<VAR>inst✝ : FiniteDimensional L F<VAR>x : F<VAR>hx : IsIntegral R x<VAR>hx' : IsIntegral L x<GOAL>Splits (algebraMap L (AlgebraicClosure F)) (minpoly L x)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M✝ : Type u_2<VAR>inst✝⁷ : AddCommGroup M✝<VAR>inst✝⁶ : Module R M✝<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M✝<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M✝<VAR>M : ι → ι → R<GOAL>(basisFun R ι).det M = detRowAlternating M
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>(-p).leadingCoeff = -p.leadingCoeff
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>k : ℕ<VAR>habk : k ∣ p.count (a * b).factors<VAR>ha : ¬a = 0<GOAL>k ∣ p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>k : ℕ<VAR>habk : k ∣ p.count (a * b).factors<VAR>ha : ¬a = 0<VAR>hz : p.count a.factors = 0<GOAL>k ∣ p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>k : ℕ<VAR>habk : k ∣ p.count (a * b).factors<VAR>ha : ¬a = 0<VAR>h : p.count b.factors = 0<GOAL>k ∣ p.count a.factors
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q) = LinearMap.ker ((aeval f) (p * q))
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>LinearMap.ker ((aeval f) (p * q)) ≤ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<GOAL>v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<GOAL>∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<VAR>h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0<GOAL>∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<VAR>h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0<VAR>h_eval₂_pqq' : ((aeval f) (p * (q * q'))) v = 0<GOAL>∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<VAR>h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0<VAR>h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0<GOAL>∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<VAR>h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0<VAR>h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0<GOAL>((aeval f) (q * q')) v + ((aeval f) (p * p')) v = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) (p * q))<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<VAR>h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0<VAR>h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0<GOAL>((aeval f) (p' * p)) v + ((aeval f) (q' * q)) v = v
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>count a (l.erase a) = count a l - 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = (a ⊔ b) \ (a ⊓ b)
<VAR>a : ↥circle<GOAL>(↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0
<VAR>a : ↥circle<VAR>i j : Fin 2<GOAL>(LinearMap.toMatrix basisOneI basisOneI) (↑(rotation a).toLinearEquiv) i j = ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) i j
<VAR>a : ↥circle<VAR>i j : Fin 2<GOAL>![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re] i = Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i => ![(↑a).im, (↑a).re] j) i
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : UniformSpace δ<VAR>h : α ≃ᵤ β<GOAL>UniformInducing (⇑h.symm ∘ ⇑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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map ((((((η.hom.app X ≫ 𝟙 (G.obj (F.obj X))) ≫ G.map (ε.inv.app (F.obj X))) ≫ 𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫ 𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫ G.map (F.map (η.inv.app X))) ≫ 𝟙 (G.obj (F.obj X))) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map (η.hom.app X) ≫ F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<VAR>this : (G ⋙ F).map (F.map (η.inv.app X)) ≫ ε.hom.app (F.obj ((𝟭 C).obj X)) = ε.hom.app (F.obj ((F ⋙ G).obj X)) ≫ (𝟭 D).map (F.map (η.inv.app X))<GOAL>F.map (η.hom.app X) ≫ F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map (η.hom.app X) ≫ F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map (η.hom.app X) ≫ (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<VAR>this : (G ⋙ F).map (ε.inv.app (F.obj X)) ≫ ε.hom.app ((G ⋙ F).obj (F.obj X)) = ε.hom.app ((𝟭 D).obj (F.obj X)) ≫ (𝟭 D).map (ε.inv.app (F.obj X))<GOAL>F.map (η.hom.app X) ≫ (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<VAR>this : (ε.app (F.obj X)).hom ≫ (ε.app (F.obj X)).inv = 𝟙 ((G ⋙ F).obj (F.obj X))<GOAL>F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<GOAL>F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<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>G : D ⥤ C<VAR>η : 𝟭 C ≅ F ⋙ G<VAR>ε : G ⋙ F ≅ 𝟭 D<VAR>X : C<VAR>this : (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj ((𝟭 C).obj X))<GOAL>F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsLUB s b<GOAL>IsLUB ((fun b => a * b) '' s) (a * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>s : Set α<VAR>ha✝ : 0 ≤ a<VAR>hs : IsLUB s b<VAR>ha : 0 < a<GOAL>IsLUB ((fun b => a * b) '' s) (a * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>b c d : α<VAR>n : ℤ<VAR>s : Set α<VAR>hs : IsLUB s b<VAR>ha : 0 ≤ 0<GOAL>IsLUB ((fun b => 0 * b) '' s) (0 * b)
<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 : α →ₛ ℝ<GOAL>map norm (-f).posPart = (-f).posPart
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x y : ProjectiveSpectrum 𝒜<GOAL>x ≤ y ↔ y ∈ closure {x}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x y : ProjectiveSpectrum 𝒜<GOAL>x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : CompactSpace X<VAR>s : Set (X × Y)<VAR>hs : IsClosed s<GOAL>IsClosed (Prod.snd '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : CompactSpace X<VAR>s : Set (X × Y)<VAR>hs : IsClosed s<GOAL>∀ x ∈ (Prod.snd '' s)ᶜ, (Prod.snd '' s)ᶜ ∈ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : CompactSpace X<VAR>s : Set (X × Y)<VAR>hs : IsClosed s<VAR>y : Y<VAR>hy : y ∈ (Prod.snd '' s)ᶜ<VAR>this : univ ×ˢ {y} ⊆ sᶜ<GOAL>(Prod.snd '' s)ᶜ ∈ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : CompactSpace X<VAR>s : Set (X × Y)<VAR>hs✝ : IsClosed s<VAR>y : Y<VAR>hy : y ∈ (Prod.snd '' s)ᶜ<VAR>this : univ ×ˢ {y} ⊆ sᶜ<VAR>U : Set X<VAR>V : Set Y<VAR>hVo : IsOpen V<VAR>hU : univ ⊆ U<VAR>hV : {y} ⊆ V<VAR>hs : U ×ˢ V ⊆ sᶜ<GOAL>(Prod.snd '' s)ᶜ ∈ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : CompactSpace X<VAR>s : Set (X × Y)<VAR>hs✝ : IsClosed s<VAR>y : Y<VAR>hy : y ∈ (Prod.snd '' s)ᶜ<VAR>this : univ ×ˢ {y} ⊆ sᶜ<VAR>U : Set X<VAR>V : Set Y<VAR>hVo : IsOpen V<VAR>hU : univ ⊆ U<VAR>hV : {y} ⊆ V<VAR>hs : U ×ˢ V ⊆ sᶜ<GOAL>V ⊆ (Prod.snd '' s)ᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : CompactSpace X<VAR>s : Set (X × Y)<VAR>hs✝ : IsClosed s<VAR>y : Y<VAR>hy : y ∈ (Prod.snd '' s)ᶜ<VAR>this : univ ×ˢ {y} ⊆ sᶜ<VAR>U : Set X<VAR>V : Set Y<VAR>hVo : IsOpen V<VAR>hU : univ ⊆ U<VAR>hV : {y} ⊆ V<VAR>hs : U ×ˢ V ⊆ sᶜ<VAR>z : X × Y<VAR>hzs : z ∈ s<VAR>hzV : z.2 ∈ V<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : R[X]<GOAL>(lift i x hx h) (h.map z) = eval₂ i x z
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : R[X]<GOAL>{ toFun := fun z => eval₂ i x (h.repr z), map_one' := ⋯, map_mul' := ⋯ } (h.map z) = eval₂ i x z
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : R[X]<GOAL>eval₂ i x (h.repr (h.map z)) = eval₂ i x z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : ℕ → Set α<VAR>h : ∑' (i : ℕ), μ (s i) ≠ ⊤<GOAL>μ (liminf s atTop) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : ℕ → Set α<VAR>h : ∑' (i : ℕ), μ (s i) ≠ ⊤<GOAL>μ (liminf s atTop) ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : ℕ → Set α<VAR>h : ∑' (i : ℕ), μ (s i) ≠ ⊤<VAR>this : liminf s atTop ≤ limsup s atTop<GOAL>μ (liminf s atTop) ≤ 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x < x_1) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x x_1 => x < x_1) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace M✝<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : ContinuousMul M✝<VAR>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => mulSupport (f i)<VAR>x₀ : X<VAR>U : Set X<VAR>hxU : U ∈ 𝓝 x₀<VAR>hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite<GOAL>∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ ↑I
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace M✝<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : ContinuousMul M✝<VAR>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => mulSupport (f i)<VAR>x₀ : X<VAR>U : Set X<VAR>hxU : U ∈ 𝓝 x₀<VAR>hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite<VAR>y : X<VAR>hy : y ∈ U<VAR>i : ι<VAR>hi : i ∈ mulSupport fun i => f i y<GOAL>i ∈ ↑hUf.toFinset