ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<GOAL>x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<VAR>this : 0 ≤ C₂<GOAL>x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<VAR>this✝ : 0 ≤ C₂<VAR>this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)<GOAL>x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<VAR>this✝ : 0 ≤ C₂<VAR>this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)<GOAL>x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<VAR>this✝ : 0 ≤ C₂<VAR>this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)<VAR>h'x : x ≤ 1<GOAL>x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup D<VAR>inst✝⁴ : NormedSpace ℝ D<VAR>inst✝³ : MeasurableSpace D<VAR>inst✝² : BorelSpace D<VAR>inst✝¹ : SecondCountableTopology D<VAR>inst✝ : FiniteDimensional ℝ D<VAR>C₁ C₂ : ℝ<VAR>k l : ℕ<VAR>x f : ℝ<VAR>hx : 0 ≤ x<VAR>hf : 0 ≤ f<VAR>h₁ : f ≤ C₁<VAR>h₂ : x ^ (k + l) * f ≤ C₂<VAR>this✝ : 0 ≤ C₂<VAR>this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)<VAR>h'x : 1 ≤ x<GOAL>x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<VAR>h : a ∈ l<GOAL>⟨a, h⟩ ∈ l.attach
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<VAR>h : a ∈ l<VAR>this : ∃ a_1, a_1 ∈ l.attach ∧ ↑a_1 = a<GOAL>⟨a, h⟩ ∈ l.attach
<VAR>p : ℝ<VAR>n : ℕ<VAR>hp_pos : 0 < p<VAR>hp_lt_one : p < 1<GOAL>0 < (1 - p) ^ n * p
<VAR>p : ℝ<VAR>n : ℕ<VAR>hp_pos : 0 < p<VAR>hp_lt_one : p < 1<VAR>this : 0 < 1 - p<GOAL>0 < (1 - p) ^ n * p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<GOAL>⇑(pullback.snd (D.f i j) (D.f i k)).base '' (⇑(pullback.fst (D.f i j) (D.f i k)).base ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<GOAL>⇑(pullback.snd (D.f i j) (D.f i k)).base '' (⇑(pullback.fst (D.f i j) (D.f i k)).base ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>⇑(pullback.snd (D.f i j) (D.f i k)).base '' (⇑(pullback.fst (D.f i j) (D.f i k)).base ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>⇑((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) '' (⇑((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>⇑(pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) ∘ ⇑(PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom '' (⇑((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) ⁻¹' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>⇑(pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) '' (⇑(PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom '' (⇑((PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) ⁻¹' S)) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>⇑(pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) '' (⇑(PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom '' (⇑(pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k))) ∘ ⇑(PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ⁻¹' S)) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>⇑((forget C).map (D.f i k)) ⁻¹' (⇑((forget C).map (D.f i j)) '' S) = ⇑(D.f i k).base ⁻¹' (⇑(D.f i j).base '' S)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>Function.Surjective ⇑(PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>D : GlueData C<VAR>i j k : D.J<VAR>S : Set ↑↑(D.V (i, j))<VAR>eq₁ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.fst (D.f i j) (D.f i k)).base<VAR>eq₂ : (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫ pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) = (pullback.snd (D.f i j) (D.f i k)).base<GOAL>Epi (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom
<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✝¹ : CommSemiring S<VAR>f : R →+* S<VAR>inst✝ : DecidableEq σ<VAR>i : σ<GOAL>i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>W₀ : Π₀ (i : ι), G i<GOAL>hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : FunLike F A R<VAR>inst✝¹ : AlgHomClass F R A R<VAR>inst✝ : Nontrivial R<VAR>φ : F<VAR>a : A<GOAL>φ a ∈ σ a
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R B<VAR>inst✝² : FunLike F A R<VAR>inst✝¹ : AlgHomClass F R A R<VAR>inst✝ : Nontrivial R<VAR>φ : F<VAR>a : A<VAR>h : ↑ₐ (φ a) - a ∈ RingHom.ker ↑φ<GOAL>φ a ∈ σ a
<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✝⁶ : Fintype ι<VAR>inst✝⁵ : Semiring 𝕜<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝² : (i : ι) → Module 𝕜 (α i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>b₁ b₂ : β i<GOAL>nndist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁)) ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) = nndist b₁ b₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x✝ : X<VAR>s : Set X<VAR>B : Set (Set X)<VAR>hB : IsTopologicalBasis B<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∈ s ∧ s ∈ B) closure
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>x✝ : K<GOAL>x✝ ∈ (valuation A K).integer ↔ x✝ ∈ (algebraMap A K).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>IsOpen s ↔ IsUpperSet s ∧ DirSupInacc s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>IsUpperSet s ∧ IsOpen s ↔ IsUpperSet s ∧ DirSupInacc s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>h : IsUpperSet s<VAR>h' : DirSupInacc s<VAR>d : Set α<VAR>d₁ : d.Nonempty<VAR>d₂ : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>x✝ : α<VAR>d₃ : IsLUB d x✝<VAR>ha : x✝ ∈ s<GOAL>∃ b ∈ d, Ici b ∩ d ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>h : IsUpperSet s<VAR>h' : DirSupInacc s<VAR>d : Set α<VAR>d₁ : d.Nonempty<VAR>d₂ : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>x✝ : α<VAR>d₃ : IsLUB d x✝<VAR>ha : x✝ ∈ s<VAR>b : α<VAR>hbd : b ∈ d<VAR>hbu : b ∈ s<GOAL>∃ b ∈ d, Ici b ∩ d ⊆ s
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>v : π i<GOAL>update (s.piecewise f g) i v = s.piecewise f (update g i v)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>v : π i<GOAL>s.piecewise (update f i v) (update g i v) = s.piecewise f (update g i v)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>v : π i<VAR>j : ι<VAR>hj : j ∈ s<GOAL>j ≠ i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A : OrderBot α<VAR>hB : PartialOrder α<VAR>B : OrderBot α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊥ = ⊥
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A B : OrderBot α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊥ = ⊥
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A B : OrderBot α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊥ ≤ ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup R<VAR>inst✝ : StarAddMonoid R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x - y)
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>↑a.val = (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n) + ↑(if a.val ≤ n / 2 then 0 else n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<VAR>hj : j = 0<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) = X.map (SimplexCategory.δ (j.pred ⋯)) ≫ X.map (SimplexCategory.δ i.castSucc)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>h1 : 1 ∈ S<VAR>hg : g ∈ T<GOAL>↑(hST.equiv g).1 = ↑⟨1, h1⟩
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>i : ι<VAR>x : ↥(A i)<GOAL>((LinearEquiv.ofBijective (coeLinearMap A) h).symm ↑x) i = x
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F : ℕᵒᵖ ⥤ Type u<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>hF : ∀ (n : ℕ), Function.Surjective (F.map (homOfLE ⋯).op)<VAR>a : F.obj (Opposite.op 0)<VAR>n m : ℕ<VAR>h : m ≤ n<GOAL>F.map (Opposite.op { down := { down := h } }) ((fun x => match x with | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n) (Opposite.op n)) = (fun x => match x with | Opposite.op n => CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage hF a n) (Opposite.op m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length<GOAL>(suffixLevenshtein C (x :: xs) (y :: ys)).val[0] = match suffixLevenshtein C xs (y :: ys) with | ⟨dx, property⟩ => match suffixLevenshtein C (x :: xs) ys with | ⟨dy, property_1⟩ => match suffixLevenshtein C xs ys with | ⟨dxy, property_2⟩ => min (C.delete x + dx[0]) (min (C.insert y + dy[0]) (C.substitute x y + dxy[0]))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length<GOAL>(impl C (x :: xs) y (suffixLevenshtein C (x :: xs) ys)).val[0] = match suffixLevenshtein C xs (y :: ys) with | ⟨dx, property⟩ => match suffixLevenshtein C (x :: xs) ys with | ⟨dy, property_1⟩ => match suffixLevenshtein C xs ys with | ⟨dxy, property_2⟩ => min (C.delete x + dx[0]) (min (C.insert y + dy[0]) (C.substitute x y + dxy[0]))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length<GOAL>(impl C (x :: xs) y ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩).val[0] = min (C.delete x + (suffixLevenshtein C xs (y :: ys)).val[0]) (min (C.insert y + (levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val)[0]) (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length<GOAL>(match impl C xs y ⟨(suffixLevenshtein C xs ys).val, ?w'⟩ with | ⟨r, w⟩ => min (C.delete x + r[0]) (min (C.insert y + levenshtein C (x :: xs) ys) (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))) = min (C.delete x + (suffixLevenshtein C xs (y :: ys)).val[0]) (min (C.insert y + (levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val)[0]) (C.substitute x y + (suffixLevenshtein C xs ys).val[0]))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length<GOAL>0 < (suffixLevenshtein C xs ys).val.length
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : α<GOAL>Iio a ⊆ Iic a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop Y) := Presheaf.imageSieve α ((R.val.map π) r) ⊓ Presheaf.imageSieve φ ((A.val.map π) m)<GOAL>(A.val.map π) (smul α φ r m) = smul α φ ((R.val.map π) r) ((A.val.map π) m)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop Y) := Presheaf.imageSieve α ((R.val.map π) r) ⊓ Presheaf.imageSieve φ ((A.val.map π) m)<VAR>hS : S ∈ J.sieves (Opposite.unop Y)<GOAL>(A.val.map π) (smul α φ r m) = smul α φ ((R.val.map π) r) ((A.val.map π) m)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop Y) := Presheaf.imageSieve α ((R.val.map π) r) ⊓ Presheaf.imageSieve φ ((A.val.map π) m)<VAR>hS : S ∈ J.sieves (Opposite.unop Y)<GOAL>∀ (Y_1 : C) (f : Y_1 ⟶ Opposite.unop Y), S.arrows f → (A.val.map f.op) ((A.val.map π) (smul α φ r m)) = (A.val.map f.op) (smul α φ ((R.val.map π) r) ((A.val.map π) m))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y✝ : Cᵒᵖ<VAR>π : X ⟶ Y✝<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>S : Sieve (Opposite.unop Y✝) := Presheaf.imageSieve α ((R.val.map π) r) ⊓ Presheaf.imageSieve φ ((A.val.map π) m)<VAR>hS : S ∈ J.sieves (Opposite.unop Y✝)<VAR>Y : C<VAR>f : Y ⟶ Opposite.unop Y✝<VAR>r₀ : (forget RingCat).obj (R₀.obj (Opposite.op Y))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.val.map f.op) ((R.val.map π) r)<VAR>m₀ : (forget AddCommGrp).obj (M₀.presheaf.obj (Opposite.op Y))<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.val.map f.op) ((A.val.map π) m)<GOAL>(A.val.map f.op) ((A.val.map π) (smul α φ r m)) = (A.val.map f.op) (smul α φ ((R.val.map π) r) ((A.val.map π) m))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ θ : L.BoundedFormula α n<VAR>h1 : T.SemanticallyEquivalent φ ψ<VAR>h2 : T.SemanticallyEquivalent ψ θ<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<VAR>h1' : (φ ⇔ ψ).Realize v xs<VAR>h2' : (ψ ⇔ θ).Realize v xs<GOAL>(φ ⇔ θ).Realize v xs