ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<VAR>obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass<VAR>lim_pair : Tendsto (fun i => (↑(nndist f 0), ↑(μs i).mass)) F (𝓝 (↑(nndist f 0), 0))<GOAL>Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<VAR>obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass<VAR>lim_pair : Tendsto (fun i => (↑(nndist f 0), ↑(μs i).mass)) F (𝓝 (↑(nndist f 0), 0))<VAR>key : Tendsto ((fun p => p.1 * p.2) ∘ fun i => (↑(nndist f 0), ↑(μs i).mass)) F (𝓝 (↑(nndist f 0) * 0))<GOAL>Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>o.oangle (r • x) y = o.oangle x y
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : NonAssocRing α<VAR>a✝ b : α<VAR>n✝ : ℤ<VAR>a : α<VAR>n : ℕ<GOAL>↑n • a = ↑↑n * a
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : NonAssocRing α<VAR>a✝ b : α<VAR>n✝ : ℤ<VAR>a : α<VAR>n : ℕ<GOAL>-[n+1] • a = ↑-[n+1] * a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>b⁻¹ * a ≤ c ↔ a ≤ c * b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C D : G.ComponentCompl K<VAR>ne : C ≠ D<GOAL>Disjoint ↑C ↑D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C D : G.ComponentCompl K<VAR>ne : C ≠ D<GOAL>↑C ∩ ↑D ⊆ ∅
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>f : X → 𝕜<VAR>hf : Integrable f μ<GOAL>↑(∫ (x : X), re (f x) ∂μ) + ↑(∫ (x : X), im (f x) ∂μ) * I = ∫ (x : X), f x ∂μ
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x✝ x y z : C<GOAL>z ∈ closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x✝ x y z : C<GOAL>(∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : 1 < finrank ℚ K<GOAL>2 < |discr K|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : Nat.succ 1 ≤ finrank ℚ K<GOAL>2 < |discr K|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : Nat.succ 1 ≤ finrank ℚ K<GOAL>2 < |↑(discr K)|
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n✝ : ℕ<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n % ↑(card G)) = a ^ n
<VAR>α : Type u_1<VAR>I B X : Set α<VAR>M : IndepMatroid α<GOAL>∀ ⦃I : Set α⦄, M.Indep I ↔ ∃ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) B ∧ I ⊆ B
<VAR>α : Type u_1<VAR>I✝ B X : Set α<VAR>M : IndepMatroid α<VAR>I : Set α<VAR>h : M.Indep I<GOAL>∃ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) B ∧ I ⊆ B
<VAR>α : Type u_1<VAR>I✝ B✝ X : Set α<VAR>M : IndepMatroid α<VAR>I : Set α<VAR>h : M.Indep I<VAR>B : Set α<VAR>hB : B ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ M.E}<GOAL>∃ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) B ∧ I ⊆ B
<VAR>α : Type u_1<VAR>I✝ B✝ X : Set α<VAR>M : IndepMatroid α<VAR>I : Set α<VAR>h : M.Indep I<VAR>B : Set α<VAR>hB : (M.Indep B ∧ I ⊆ B ∧ B ⊆ M.E) ∧ ∀ ⦃y : Set α⦄, M.Indep y → I ⊆ y → y ⊆ M.E → B ⊆ y → B = y<GOAL>∃ B, (M.Indep B ∧ ∀ ⦃y : Set α⦄, M.Indep y → B ⊆ y → B = y) ∧ I ⊆ B
<VAR>α : Type u_1<VAR>I B X : Set α<VAR>M : IndepMatroid α<GOAL>∃ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) B
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B : Set α<VAR>hB₁ : ∀ ⦃b : Set α⦄, b ∈ {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ M.E} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB : M.Indep B<GOAL>∃ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) B
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<GOAL>∃ b ∈ B' \ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert b (B \ {e}))
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>f : α<VAR>hf : f ∈ B' \ (B \ {e})<VAR>hfB : M.Indep (insert f (B \ {e}))<GOAL>∃ b ∈ B' \ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert b (B \ {e}))
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>f : α<VAR>hfB : M.Indep (insert f (B \ {e}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = e)<GOAL>∃ b ∈ B' \ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert b (B \ {e}))
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>f : α<VAR>hfB : M.Indep (insert f (B \ {e}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = e)<VAR>hfB' : f ∉ B<GOAL>∃ b ∈ B' \ B, (fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert b (B \ {e}))
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>f : α<VAR>hfB : M.Indep (insert f (B \ {e}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = e)<VAR>hfB' : f ∉ B<VAR>hnot : ¬(fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert f (B \ {e}))<GOAL>False
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>f : α<VAR>hfB : M.Indep (insert f (B \ {e}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = e)<VAR>hfB' : f ∉ B<VAR>hnot : ¬(fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert f (B \ {e}))<VAR>x : α<VAR>hxB : x ∈ B \ insert f (B \ {e})<VAR>hind : M.Indep (insert x (insert f (B \ {e})))<GOAL>False
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>e : α<VAR>he : e ∈ B \ B'<VAR>hnotmax : B \ {e} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>f : α<VAR>hfB : M.Indep (insert f (B \ {e}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = e)<VAR>hfB' : f ∉ B<VAR>hnot : ¬(fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert f (B \ {e}))<VAR>x : α<VAR>hind : M.Indep (insert x (insert f (B \ {e})))<VAR>hxB : x ∈ B ∧ ¬x = f ∧ (x ∈ B → x = e)<GOAL>False
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>f : α<VAR>hfB' : f ∉ B<VAR>x : α<VAR>he : x ∈ B \ B'<VAR>hnotmax : B \ {x} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>hfB : M.Indep (insert f (B \ {x}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = x)<VAR>hnot : ¬(fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert f (B \ {x}))<VAR>hind : M.Indep (insert x (insert f (B \ {x})))<VAR>hxB : x ∈ B ∧ ¬x = f ∧ (x ∈ B → x = x)<GOAL>False
<VAR>α : Type u_1<VAR>I B✝ X : Set α<VAR>M : IndepMatroid α<VAR>B B' : Set α<VAR>hB : B ∈ {I | M.Indep I}<VAR>hBmax : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B b → (fun x x_1 => x ⊆ x_1) b B<VAR>hB' : B' ∈ {I | M.Indep I}<VAR>hB'max : ∀ ⦃b : Set α⦄, b ∈ {I | M.Indep I} → (fun x x_1 => x ⊆ x_1) B' b → (fun x x_1 => x ⊆ x_1) b B'<VAR>f : α<VAR>hfB' : f ∉ B<VAR>x : α<VAR>he : x ∈ B \ B'<VAR>hnotmax : B \ {x} ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>hfB : M.Indep (insert f (B \ {x}))<VAR>hf : f ∈ B' ∧ (f ∈ B → f = x)<VAR>hnot : ¬(fun x => x ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}) (insert f (B \ {x}))<VAR>hind : M.Indep (insert f B)<VAR>hxB : x ∈ B ∧ ¬x = f ∧ (x ∈ B → x = x)<GOAL>False
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>(pullbackP1Iso 𝒰 f g i).hom ≫ pullback.snd (𝒰.map i ≫ f) g = pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g
<VAR>α : Type u_1<VAR>inst✝⁶ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝⁵ : Sub α<VAR>inst✝⁴ : OrderedSub α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a + a - (b + b) = a - b + (a - b)
<VAR>α : Type u_1<VAR>inst✝⁶ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝⁵ : Sub α<VAR>inst✝⁴ : OrderedSub α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a ≤ b<GOAL>a + a - (b + b) = a - b + (a - b)
<VAR>α : Type u_1<VAR>inst✝⁶ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝⁵ : Sub α<VAR>inst✝⁴ : OrderedSub α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : b ≤ a<GOAL>a + a - (b + b) = a - b + (a - b)
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>i : Fin2 n<VAR>x : F α<VAR>x✝ : α i<GOAL>x✝ ∈ supp x i ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>x : α<GOAL>map (fun x_1 => ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>x : α<GOAL>∀ i' ∈ 𝓤 β, ∃ i ∈ 𝓤 β, UniformFun.gen α β i ⊆ (fun x_1 => ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : MulZeroClass α<VAR>s t : Set α<VAR>hs : s.Nonempty<GOAL>0 ⊆ 0 * s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.92128, u_1} C<VAR>inst✝⁶ : Category.{?u.92132, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<GOAL>φ ≫ 𝟙 L = 𝟙 K ≫ φ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.92132, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>φ₃ : K₃ ⟶ L₃<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>comm : φ₁ ≫ b = a ≫ φ₂<VAR>a' : K₂ ⟶ K₃<VAR>b' : L₂ ⟶ L₃<VAR>comm' : φ₂ ≫ b' = a' ≫ φ₃<VAR>n : ℤ<GOAL>(map φ φ (𝟙 K) (𝟙 L) ⋯).f n = (𝟙 (mappingCone φ)).f n
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.19205, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex V c.symm<VAR>i j : ι<VAR>hij : ¬c.Rel i j<GOAL>(X.d j i).op = 0
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.19205, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex V c.symm<VAR>x✝⁴ x✝³ x✝² : ι<VAR>x✝¹ : c.Rel x✝⁴ x✝³<VAR>x✝ : c.Rel x✝³ x✝²<GOAL>(fun i j => (X.d j i).op) x✝⁴ x✝³ ≫ (fun i j => (X.d j i).op) x✝³ x✝² = 0
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<GOAL>mkRat n d = 0 ↔ n = 0
<VAR>x : ℝ<VAR>hx : x ∈ Ioo (-(π / 2)) (π / 2)<GOAL>0 < x + π / 2
<VAR>x : ℝ<VAR>hx : x ∈ Ioo (-(π / 2)) (π / 2)<GOAL>x + π / 2 < π
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>i : σ<GOAL>(X i).IsHomogeneous 1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>i : σ<GOAL>(single i 1).degree = 1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>i : σ<GOAL>(single i 1) i = 1
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<GOAL>1 = 0 ↔ n = 1
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>proj (↑e.symm x) = x.1
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>x : B × F<VAR>hx : x ∈ e.target<VAR>this : proj (↑e.symm x) = (↑e (↑e.symm x)).1<GOAL>proj (↑e.symm x) = x.1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<GOAL>∃ c, 0 < c ∧ map (⇑L) μ = c • ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : CompleteSpace 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : MeasurableSpace E<VAR>inst✝⁸ : BorelSpace E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : MeasurableSpace F<VAR>inst✝⁴ : BorelSpace F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>inst✝¹ : ν.IsAddHaarMeasure<VAR>inst✝ : LocallyCompactSpace E<VAR>h : Function.Surjective ⇑L<VAR>c : ℝ≥0∞<VAR>c_pos : 0 < c<VAR>hc : map (⇑L) μ = (c * addHaar univ) • ν<GOAL>∃ c, 0 < c ∧ map (⇑L) μ = c • ν
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>k : ℕ<VAR>h₀ : k + k ≠ 0<GOAL>0 < a ^ (k + k) ↔ a ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : Odd n<GOAL>1 + n / 2 * 2 = n
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>(B₁ \ B₂).ncard = (B₂ \ B₁).ncard
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>e₁ e₂ : Trivialization F proj<VAR>p : Z<VAR>h : proj p ∈ e₁.baseSet<GOAL>e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a - b ≤ a / 2<GOAL>a / 2 ≤ b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ≤ b * 2<GOAL>a / 2 ≤ b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ≤ b * 2<GOAL>a / 2 ≤ b * 2 / 2
<VAR>a : ℝ<GOAL>closure {z | a < z.im} = {z | a ≤ z.im}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>s.einfsep = ⊤ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x 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>f : Filter Y<VAR>hs : IsCompact s<VAR>hf : Disjoint f (cocompact Y)<GOAL>𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)
<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>f : Filter Y<VAR>hs : IsCompact s<VAR>hf : Disjoint f (cocompact Y)<VAR>K : Set Y<VAR>hKf : K ∈ f<VAR>hK : IsCompact K<GOAL>𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>i✝ : m<VAR>j✝ : o<GOAL>(-M * N) i✝ j✝ = (-(M * N)) i✝ j✝
<VAR>z : ℤ<GOAL>IsSquare ↑z ↔ IsSquare z
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>n✝ : μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι → μ<GOAL>f ∈ Trunc.lift (fun e => map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal s.card n)) ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>n✝ : μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι → μ<VAR>e : { x // x ∈ s } ≃ Fin s.card<GOAL>f ∈ Trunc.lift (fun e => map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal s.card n)) ⋯ (Trunc.mk e) ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>n✝ : μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι → μ<VAR>e : { x // x ∈ s } ≃ Fin s.card<GOAL>(∃ a, ∑ i : Fin s.card, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.43135, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : ∀ (X : C), Projective X<GOAL>IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>c : ℝ≥0<GOAL>edist x y < ↑c ↔ nndist x y < c
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>gp_n : Pair K<VAR>s_nth_eq : (of v).s.get? n = some gp_n<GOAL>∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>gp_n : Pair K<VAR>s_nth_eq : (of v).s.get? n = some gp_n<VAR>ifp : IntFractPair K<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp<VAR>gp_n_eq : { a := 1, b := ↑ifp.b } = gp_n<GOAL>∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp : IntFractPair K<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp<VAR>s_nth_eq : (of v).s.get? n = some { a := 1, b := ↑ifp.b }<GOAL>∃ ifp_1, IntFractPair.stream v (n + 1) = some ifp_1 ∧ ↑ifp_1.b = { a := 1, b := ↑ifp.b }.b
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>ker (inr R M M₂) = ⊥
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<VAR>h : EqOn f g [[a, b]]<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : OuterMeasure α<VAR>ι : Sort u_3<VAR>f : ι → OuterMeasure α<VAR>s : Set α<GOAL>(⨆ i, f i) s = ⨆ i, (f i) s