ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<VAR>h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)<VAR>i : ℕ<GOAL>↑|(minpoly ℤ x).coeff i| ≤ ↑↑C
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>B : ℝ<VAR>C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊<VAR>this : (⋃ f, ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C), ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite<VAR>x : K<VAR>hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}<VAR>h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)<VAR>i : ℕ<GOAL>↑|(minpoly ℤ x).coeff i| = ‖(minpoly ℚ x).coeff i‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>p : α → Prop<VAR>h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x<GOAL>∀ᶠ (x : α) in 𝓝[s] a, p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x<GOAL>∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x' x : α<VAR>h✝ : r x' x<VAR>a : α<VAR>h : a ∈ {x'}<GOAL>r a x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁ m₂ : M<GOAL>(ι Q) m₁ * (ι Q) m₂ ∈ LinearMap.range (ι Q) ^ ↑⟨2, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m₁ m₂ : M<GOAL>(ι Q) m₁ * (ι Q) m₂ ∈ LinearMap.range (ι Q) * LinearMap.range (ι Q)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>I : ↥(Ideal S)⁰<GOAL>∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>I : ↥(Ideal S)⁰<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z<GOAL>∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>I : ↥(Ideal S)⁰<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z<VAR>c : S<VAR>hc : c ∈ ↑I<VAR>lt : abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b)<GOAL>c = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>I : ↥(Ideal S)⁰<VAR>b : S<VAR>b_mem : b ∈ ↑I<VAR>b_ne_zero : b ≠ 0<VAR>min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z<VAR>c : S<VAR>hc : c ∈ ↑I<VAR>c_ne_zero : c ≠ 0<GOAL>abv ((Algebra.norm R) b) ≤ abv ((Algebra.norm R) c)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ZMod n →+* R<VAR>a : ZMod n<GOAL>f a = g a
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ZMod n →+* R<VAR>k : ℤ<GOAL>f ↑k = g ↑k
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ZMod n →+* R<VAR>k : ℤ<VAR>φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))<VAR>ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))<GOAL>φ k = ψ k
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s t : Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h : ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t<VAR>s1 t1 : Set Ω<VAR>hs1 : s1 ∈ {s}<VAR>ht1 : t1 ∈ {t}<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (s1 ∩ t1) = (κ a) s1 * (κ a) t1
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>i : m<VAR>hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0<GOAL>v i = 0 i
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>i : m<VAR>hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0<GOAL>v i * M.det = 0
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>i : m<VAR>hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0<GOAL>v i * M.det = v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1)
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>i : m<VAR>hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0<GOAL>v i * M.det = ∑ x : m, v x * (M.det * Pi.single i 1 x)
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>i : m<VAR>hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0<GOAL>∀ b ∈ Finset.univ, b ≠ i → v b * (M.det * Pi.single i 1 b) = 0
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>i : m<VAR>hv : v ⬝ᵥ M *ᵥ M.cramer (Pi.single i 1) = 0<GOAL>i ∉ Finset.univ → v i * (M.det * Pi.single i 1 i) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b✝ c✝ d : G<VAR>n : ℤ<VAR>a b c : G<GOAL>a / b * (b / c) = a / c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Preorder (π i)<VAR>a b c : (i : ι) → π i<VAR>inst✝ : Nonempty ι<VAR>h : a ≺ b<VAR>inhabited_h : Inhabited ι<GOAL>a < b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<GOAL>IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<GOAL>(∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>inst✝ : LinearOrder α<VAR>Ixx : α → α → Set α<VAR>p : α → α → Prop<VAR>Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b<VAR>Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)<VAR>f : ι → α<VAR>g : ι' → α<GOAL>IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>g : M ≃[L] N<VAR>φ : L.Formula α<VAR>v : α → M<GOAL>φ.Realize (⇑g ∘ v) ↔ φ.Realize v
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<GOAL>s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<GOAL>(∃ x, xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<VAR>x : Set α<VAR>x✝ : xᶜ ∈ f<GOAL>kernImage m xᶜ = s ↔ m '' x = sᶜ
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<GOAL>(T ^ n • z).re = z.re + ↑n
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β✝<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>β : Type u_5<VAR>inst✝ : NormedLatticeAddCommGroup β<VAR>f g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>Integrable (f ⊔ g) μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β✝<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>β : Type u_5<VAR>inst✝ : NormedLatticeAddCommGroup β<VAR>f g : α → β<VAR>hf : Memℒp f 1 μ<VAR>hg : Memℒp g 1 μ<GOAL>Memℒp (f ⊔ g) 1 μ
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f g : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hf : DiffContOnCl ℂ f U<VAR>hg : DiffContOnCl ℂ g U<VAR>hfg : EqOn f g (frontier U)<GOAL>EqOn f g (closure U)
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f g : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hf : DiffContOnCl ℂ f U<VAR>hg : DiffContOnCl ℂ g U<VAR>hfg : EqOn f g (frontier U)<GOAL>∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f g : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hf : DiffContOnCl ℂ f U<VAR>hg : DiffContOnCl ℂ g U<VAR>hfg : EqOn f g (frontier U)<VAR>z : E<VAR>hz : z ∈ closure U<VAR>w : E<VAR>hw : w ∈ frontier U<GOAL>‖(f - g) w‖ ≤ 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>hf : OpenEmbedding ⇑f<GOAL>CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>hf : OpenEmbedding ⇑f<VAR>this : Mono f<GOAL>CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>hf : OpenEmbedding ⇑f<VAR>this : Mono f<GOAL>{c : Opens ↑X} → {d : Opens ↑Y} → (d ⟶ ⋯.functor.obj c) → (c' : Opens ↑X) × (⋯.functor.obj c' ≅ d)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>hf : OpenEmbedding ⇑f<VAR>this : Mono f<VAR>U : Opens ↑X<VAR>V : Opens ↑Y<VAR>i : V ⟶ ⋯.functor.obj U<GOAL>(c' : Opens ↑X) × (⋯.functor.obj c' ≅ V)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>hf : OpenEmbedding ⇑f<VAR>this : Mono f<VAR>U : Opens ↑X<VAR>V : Opens ↑Y<VAR>i : V ⟶ ⋯.functor.obj U<VAR>x : ↑Y<VAR>h : x ∈ V.1<GOAL>x ∈ Set.range ⇑f
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>(ofSet s hs).trans e = e.restr (e.source ∩ s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>ha : Disjoint a c<VAR>hb : Disjoint b c<GOAL>Disjoint (a ∆ b) c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>ha : Disjoint a c<VAR>hb : Disjoint b c<GOAL>Disjoint ((a ⊔ b) \ (a ⊓ b)) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<GOAL>(¬∀ ⦃s' : Finset α⦄, s' ⊆ s → ∀ ⦃t' : Finset α⦄, t' ⊆ t → ↑s.card * ε ≤ ↑s'.card → ↑t.card * ε ≤ ↑t'.card → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε) ↔ ∃ s' ⊆ s, ∃ t' ⊆ t, ↑s.card * ε ≤ ↑s'.card ∧ ↑t.card * ε ≤ ↑t'.card ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝² : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i j : ι<VAR>a : α i<VAR>β✝¹ : Type u_5<VAR>inst✝ : CompleteLattice β✝¹<VAR>β✝ : Type u_6<VAR>β : ι → Type u_7<GOAL>(¬∃ i ∈ s, (t i).Nonempty) ↔ ∀ i ∈ s, t i = ∅
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>exp A * evalNegHom (exp A) = 1
<VAR>θ : Angle<GOAL>(θ + ↑π).cos = -θ.cos
<VAR>x✝ : ℝ<GOAL>(↑x✝ + ↑π).cos = -(↑x✝).cos
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F : J → C<VAR>K : Type w'<VAR>f : J → C<VAR>c : Bicone f<VAR>g : K ≃ J<VAR>k k' : K<GOAL>(fun k => c.ι (g k)) k ≫ (fun k => c.π (g k)) k' = if h : k = k' then eqToHom ⋯ else 0
<VAR>J : Type w<VAR>C : Type uC<VAR>inst✝³ : Category.{uC', uC} C<VAR>inst✝² : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>inst✝ : HasZeroMorphisms D<VAR>F : J → C<VAR>K : Type w'<VAR>f : J → C<VAR>c : Bicone f<VAR>g : K ≃ J<VAR>k k' : K<GOAL>(if h : g k = g k' then eqToHom ⋯ else 0) = if h : k = k' then eqToHom ⋯ else 0
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : LinearOrderedRing α<VAR>H₁ H₂ : FloorRing α<GOAL>H₁ = H₂
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : LinearOrderedRing α<VAR>H₁ H₂ : FloorRing α<VAR>this : FloorRing.floor = FloorRing.floor<GOAL>H₁ = H₂
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : LinearOrderedRing α<VAR>H₁ H₂ : FloorRing α<VAR>this✝ : FloorRing.floor = FloorRing.floor<VAR>this : FloorRing.ceil = FloorRing.ceil<GOAL>H₁ = H₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>s : Set ι'<VAR>t : (i : ι) → Set (α i)<GOAL>⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i => t (f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>s : Set ι'<VAR>t : (i : ι) → Set (α i)<GOAL>∀ (x : (a : ι') → α (f a)), x ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ x ∈ s.pi fun i => t (f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>s : Set ι'<VAR>t : (i : ι) → Set (α i)<GOAL>∀ (a : (b : ι) → α b), (piCongrLeft α f).symm a ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ (piCongrLeft α f).symm a ∈ s.pi fun i => t (f i)
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L (fun n => ↑(Λ n)) s = -deriv riemannZeta s / riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>deriv (L 1) s = deriv riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1
<VAR>a b : Cardinal.{u_1}<GOAL>a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
<VAR>a b : Cardinal.{u_1}<GOAL>a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<GOAL>Tendsto (fun n => ⇑(thickenedIndicator ⋯ E)) atTop (𝓝 ((closure E).indicator fun x => 1))
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<VAR>key : Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 ((closure E).indicator fun x => 1))<GOAL>Tendsto (fun n => ⇑(thickenedIndicator ⋯ E)) atTop (𝓝 ((closure E).indicator fun x => 1))
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<VAR>key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))<GOAL>∀ (x : α), Tendsto (fun i => (thickenedIndicator ⋯ E) x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<VAR>key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))<VAR>x : α<GOAL>Tendsto (fun i => (thickenedIndicator ⋯ E) x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<VAR>key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))<VAR>x : α<GOAL>Tendsto (fun i => (thickenedIndicator ⋯ E) x) atTop (𝓝 ((closure E).indicator (fun x => 1) x).toNNReal)
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<VAR>key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))<VAR>x : α<GOAL>(closure E).indicator (fun x => 1) x ≠ ⊤
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropWithinAt P g s x<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>LiftPropWithinAt P g' s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropWithinAt P g s x<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>P (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropWithinAt P g s x<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm =ᶠ[𝓝[↑(chartAt H x).symm ⁻¹' s] ↑(chartAt H x) x] ↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropWithinAt P g s x<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>∀ᶠ (x_1 : H) in 𝓝[↑(chartAt H x).symm ⁻¹' s] ↑(chartAt H x) x, ↑(chartAt H' (g' x)) (g' (↑(chartAt H x).symm x_1)) = ↑(chartAt H' (g x)) (g (↑(chartAt H x).symm x_1))
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropWithinAt P g s x<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>∀ᶠ (x_1 : M) in 𝓝[s] x, ↑(chartAt H' (g' x)) (g' x_1) = ↑(chartAt H' (g x)) (g x_1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<GOAL>toOpen R ⊤ = CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ toBasicOpen R 1 ≫ (structureSheaf R).val.map (eqToHom ⋯).op
<VAR>R : Type u<VAR>inst✝ : CommRing R<GOAL>toOpen R ⊤ = (CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ toBasicOpen R 1) ≫ (structureSheaf R).val.map (eqToHom ⋯).op
<VAR>R : Type u<VAR>inst✝ : CommRing R<GOAL>toOpen R ⊤ = (toBasicOpen R 1).comp (algebraMap R (Localization.Away 1)) ≫ (structureSheaf R).val.map (eqToHom ⋯).op