ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : PseudoMetrizableSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>s : Set β<VAR>h1s : IsClosed s<VAR>h2s : s.Nonempty<VAR>h3s : s ≠ Set.univ<VAR>this : Measurable fun x => infNndist (g x) s<VAR>h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0}<GOAL>MeasurableSet ((fun x => infNndist (g x) s) ⁻¹' {0})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a✝ b : α<VAR>s : Finset α<VAR>a : α<GOAL>↑s = {a} ↔ s = {a}
<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>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<GOAL>Continuous (e₁.coordChange e₂ b)
<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>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<GOAL>Continuous (Prod.mk b)
<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>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<GOAL>∀ (x : F), (b, x) ∈ e₁.target
<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>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<GOAL>∀ (x : F), ↑e₁.symm (b, x) ∈ e₂.source
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>p : X → Prop<VAR>x : X<VAR>hx : p x<VAR>h : ∀ᶠ (x : X) in 𝓝 x, p x<GOAL>range Subtype.val ∈ 𝓝 ↑⟨x, hx⟩
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>p : X → Prop<VAR>x : X<VAR>hx : p x<VAR>h : ∀ᶠ (x : X) in 𝓝 x, p x<GOAL>p ∈ 𝓝 ↑⟨x, hx⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), (f i).NeBot<VAR>I : Set ι<GOAL>(pi f ⊓ 𝓟 (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ 𝓟 (s i)).NeBot
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z✝ : TopCat<VAR>Z : C<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>U : Opens ↑X<VAR>φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z<VAR>h : ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V), ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ = ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ<GOAL>φ = ψ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z✝ : TopCat<VAR>Z : C<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>U : Opens ↑X<VAR>φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z<VAR>h : ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V), ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ = ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ<GOAL>∀ (j : CostructuredArrow (Opens.map f).op (op U)), ((Functor.LeftExtension.mk ((Opens.map f).op.lan.obj F) ((Opens.map f).op.lanUnit.app F)).coconeAt (op U)).ι.app j ≫ φ = ((Functor.LeftExtension.mk ((Opens.map f).op.lan.obj F) ((Opens.map f).op.lanUnit.app F)).coconeAt (op U)).ι.app j ≫ ψ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z✝ : TopCat<VAR>Z : C<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>U : Opens ↑X<VAR>φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z<VAR>h : ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V), ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ = ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ<VAR>V : Opens ↑Y<VAR>as✝ : PUnit.{1}<VAR>b : unop ((Functor.fromPUnit (op U)).obj { as := as✝ }) ⟶ unop ((Opens.map f).op.obj (op V))<GOAL>((Functor.LeftExtension.mk ((Opens.map f).op.lan.obj F) ((Opens.map f).op.lanUnit.app F)).coconeAt (op U)).ι.app { left := op V, right := { as := as✝ }, hom := op b } ≫ φ = ((Functor.LeftExtension.mk ((Opens.map f).op.lan.obj F) ((Opens.map f).op.lanUnit.app F)).coconeAt (op U)).ι.app { left := op V, right := { as := as✝ }, hom := op b } ≫ ψ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>γ : Type u_7<VAR>s : Finset (α × β × γ)<VAR>f : α × β × γ → M<GOAL>∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝¹ : Functor t<VAR>inst✝ : LawfulFunctor t<VAR>α β γ : Type u<VAR>g : α → β<VAR>h : β → γ<VAR>x : t' α<GOAL>Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝¹ : HasRightDual X<VAR>inst✝ : HasRightDual Y<VAR>f : X ⟶ Y<VAR>g : Xᘁ ⟶ Z<GOAL>((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g = 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝¹ : HasRightDual X<VAR>inst✝ : HasRightDual Y<VAR>f : X ⟶ Y<VAR>g : Xᘁ ⟶ Z<GOAL>𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z = (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ⊗ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>X Y Z : C<VAR>inst✝¹ : HasRightDual X<VAR>inst✝ : HasRightDual Y<VAR>f : X ⟶ Y<VAR>g : Xᘁ ⟶ Z<GOAL>𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ ((Yᘁ ⊗ Y) ◁ g ≫ ε_ Y Yᘁ ▷ Z) ⊗≫ 𝟙 Z = (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ▷ Xᘁ ≫ Y ◁ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom
<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 Q' : QuadraticForm R M<VAR>h : Q' = -Q<VAR>h' : Q = -Q'<VAR>m₁ m₂ : M<GOAL>(((even.ι Q).compr₂ ((evenToNeg Q' Q h').comp (evenToNeg Q Q' h))).bilin m₁) m₂ = (((even.ι Q).compr₂ (AlgHom.id R ↥(even Q))).bilin m₁) m₂
<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 Q' : QuadraticForm R M<VAR>h : Q' = -Q<VAR>h' : Q = -Q'<VAR>m₁ m₂ : M<GOAL>(evenToNeg Q' Q h') ((evenToNeg Q Q' h) (((even.ι Q).bilin m₁) m₂)) = ((even.ι Q).bilin m₁) m₂
<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 Q' : QuadraticForm R M<VAR>h : Q' = -Q<VAR>h' : Q = -Q'<VAR>m₁ m₂ : M<GOAL>(evenToNeg Q' Q h') (-((even.ι Q').bilin m₁) m₂) = ((even.ι Q).bilin m₁) m₂
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(ρ_ X₁).hom ⊗ (ρ_ X₂).hom = ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<VAR>this : (ρ_ X₁).hom ⊗ (ρ_ X₂).hom = (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom<GOAL>(ρ_ X₁).hom ⊗ (ρ_ X₂).hom = ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom = ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ ((β_ (𝟙_ C) X₂).hom ≫ (ρ_ X₂).hom) = ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : Group α<VAR>h₁ : UniformContinuous fun p => p.1 * p.2<VAR>h₂ : UniformContinuous fun p => p⁻¹<GOAL>UniformContinuous fun p => p.1 / p.2
<VAR>d x y : ℕ<VAR>a : ℤ√↑d<VAR>ha : a.Nonneg<GOAL>({ re := ↑x, im := ↑y } * a).Nonneg
<VAR>d x y : ℕ<VAR>a : ℤ√↑d<VAR>ha : a.Nonneg<VAR>this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)<GOAL>({ re := ↑x, im := ↑y } * a).Nonneg
<VAR>d x y : ℕ<VAR>a : ℤ√↑d<VAR>ha : a.Nonneg<VAR>this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)<GOAL>(↑x * a + sqrtd * (↑y * a)).Nonneg
<VAR>m n : ℕ<VAR>h : m ∣ n<GOAL>fib m ∣ fib n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : Monoid γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>p : β → Prop<VAR>hom : ∀ (a b : β), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ s, p (f x)<GOAL>p (s.noncommProd f comm)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : Monoid γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>p : β → Prop<VAR>hom : ∀ (a b : β), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ s, p (f x)<VAR>b : β<VAR>hb : b ∈ Multiset.map f s.val<GOAL>p b
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : PreservesLimit (cospan f f) F<VAR>inst✝ : Mono f<VAR>this : let_fun this := ⋯; IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)<GOAL>Mono (F.map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : PreservesLimit (cospan f f) F<VAR>inst✝ : Mono f<VAR>this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)<GOAL>Mono (F.map f)
<VAR>n k : ℕ<VAR>hk : k ≠ 0<GOAL>Λ (n ^ k) = Λ n
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P Q : Cᵒᵖ ⥤ D<VAR>R : Sheaf J D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ (sheafToPresheaf J D).obj R<GOAL>J.sheafifyMap η ≫ J.sheafifyLift γ ⋯ = J.sheafifyLift (η ≫ γ) ⋯
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>X✝ : Cᵒᵖ ⥤ D<VAR>Y✝ Y'✝ : Sheaf J D<VAR>η : (plusPlusSheaf J D).obj X✝ ⟶ Y✝<VAR>γ : Y✝ ⟶ Y'✝<GOAL>J.toSheafify X✝ ≫ η.val ≫ γ.val = (J.toSheafify X✝ ≫ η.val) ≫ γ.val
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<VAR>hy : a.y = 0<GOAL>False
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<VAR>hy : a.y = 0<VAR>prop : a.x ^ 2 - d * a.y ^ 2 = 1<GOAL>False
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<VAR>hy : a.y = 0<VAR>prop : a.x ^ 2 = 1<GOAL>False
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>s : Multiset α<GOAL>s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>s : Multiset α<GOAL>s = Multiset.map id s
<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>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Sieve (F.obj X)<VAR>Y✝ Z✝ : C<VAR>f : Y✝ ⟶ X<VAR>hf : Presieve.functorPullback F R.arrows f<VAR>g : Z✝ ⟶ Y✝<GOAL>R.arrows (F.map (g ≫ f))
<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>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Sieve (F.obj X)<VAR>Y✝ Z✝ : C<VAR>f : Y✝ ⟶ X<VAR>hf : Presieve.functorPullback F R.arrows f<VAR>g : Z✝ ⟶ Y✝<GOAL>R.arrows (F.map g ≫ F.map f)
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>x : ℤ[i]<GOAL>↑(norm x).natAbs = ↑(norm x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<GOAL>⊥.preimage s = ∅
<VAR>m n : ℤ<GOAL>Even (m - n) ↔ (Odd m ↔ Odd n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Dual R M<GOAL>(p x) (p.toDualRight.symm f) = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Dual R M<VAR>h : p.toDualRight (p.toDualRight.symm f) = f<GOAL>(p x) (p.toDualRight.symm f) = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Dual R M<VAR>h : p.flip (p.toDualRight.symm f) = f<GOAL>(p x) (p.toDualRight.symm f) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → Option γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<VAR>g₁ : AssocList α β → List (α × γ) := fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList<GOAL>(Imp.filterMap f m).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → Option γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<VAR>g₁ : AssocList α β → List (α × γ) := fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList<VAR>H1 : ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ), filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })<GOAL>(Imp.filterMap f m).WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → Option γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<VAR>g₁ : AssocList α β → List (α × γ) := fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList<VAR>H1 : ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ), filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })<VAR>g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList<VAR>M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id<VAR>H2 : ∀ (l : List (AssocList α β)) (n : ULift Nat), List.mapM (filterMap.go f AssocList.nil) l n = (List.map g l, { down := n.down + Nat.sum (List.map (fun x => x.toList.length) (List.map g l)) })<VAR>H3 : ∀ (l : List (α × β)), (List.map (fun a => a.fst) (List.filterMap (fun x => match x with | (a, b) => Option.map (fun x => (a, x)) (f a b)) l)).Sublist (List.map (fun x => x.fst) l)<GOAL>∀ (bk : List (AssocList α γ)) (sz : Nat) (h : 0 < bk.length), Array.mapM (filterMap.go f AssocList.nil) m.buckets.val { down := 0 } = ({ data := bk }, { down := sz }) → { size := sz, buckets := ⟨{ data := bk }, h⟩ }.WF
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → Option γ<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>H : m.WF<VAR>g₁ : AssocList α β → List (α × γ) := fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList<VAR>H1 : ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ), filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })<VAR>g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList<VAR>M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id<VAR>H2 : ∀ (l : List (AssocList α β)) (n : ULift Nat), List.mapM (filterMap.go f AssocList.nil) l n = (List.map g l, { down := n.down + Nat.sum (List.map (fun x => x.toList.length) (List.map g l)) })<VAR>H3 : ∀ (l : List (α × β)), (List.map (fun a => a.fst) (List.filterMap (fun x => match x with | (a, b) => Option.map (fun x => (a, x)) (f a b)) l)).Sublist (List.map (fun x => x.fst) l)<GOAL>∀ (bk : List (AssocList α γ)) (sz : Nat) (h : 0 < bk.length), pure { data := List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.data } { down := Nat.sum (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList) m.buckets.val.data) } = ({ data := bk }, { down := sz }) → { size := sz, buckets := ⟨{ data := bk }, h⟩ }.WF
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedField 𝕜₁<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra 𝕜₁ A<VAR>inst✝² : NormedAlgebra 𝕜₂ A<VAR>inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂<VAR>inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<GOAL>⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊ = ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedField 𝕜₁<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra 𝕜₁ A<VAR>inst✝² : NormedAlgebra 𝕜₂ A<VAR>inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂<VAR>inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<VAR>this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊<GOAL>⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊ = ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedField 𝕜₁<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra 𝕜₁ A<VAR>inst✝² : NormedAlgebra 𝕜₂ A<VAR>inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂<VAR>inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<VAR>this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊<GOAL>⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedField 𝕜₁<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra 𝕜₁ A<VAR>inst✝² : NormedAlgebra 𝕜₂ A<VAR>inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂<VAR>inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<VAR>this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊<GOAL>⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedField 𝕜₁<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra 𝕜₁ A<VAR>inst✝² : NormedAlgebra 𝕜₂ A<VAR>inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂<VAR>inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<VAR>this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊<VAR>x : 𝕜₁<VAR>hx : x ∈ spectrum 𝕜₁ a<GOAL>↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>𝕜₁ : Type u_3<VAR>𝕜₂ : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedField 𝕜₁<VAR>inst✝⁵ : NormedField 𝕜₂<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra 𝕜₁ A<VAR>inst✝² : NormedAlgebra 𝕜₂ A<VAR>inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂<VAR>inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A<VAR>f : 𝕜₂ → 𝕜₁<VAR>a : A<VAR>h : SpectrumRestricts a f<VAR>this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊<VAR>x : 𝕜₂<VAR>hx : x ∈ spectrum 𝕜₂ a<GOAL>↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊
<VAR>α✝ : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α✝<VAR>α : Type u<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : CompleteSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>x✝ : f ≤ 𝓟 univ<GOAL>∃ x ∈ univ, f ≤ 𝓝 x
<VAR>α✝ : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α✝<VAR>α : Type u<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : CompleteSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>x✝ : f ≤ 𝓟 univ<VAR>x : α<VAR>hx : f ≤ 𝓝 x<GOAL>∃ x ∈ univ, f ≤ 𝓝 x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).b₂ = ↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) = ↑C.u⁻¹ ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂ + 12 * C.r)