ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>α : Type u_9<VAR>inst✝ : DecidableEq α<VAR>x : Multiset α<GOAL>((Finset.range (card x + 1)).sup fun k => powersetCard k x) = x.powerset
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>α : Type u_9<VAR>inst✝ : DecidableEq α<VAR>x : Multiset α<GOAL>((Finset.range (card x + 1)).sup fun k => powersetCard k x) = (range (card x + 1)).bind fun k => powersetCard k x
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>α : Type u_9<VAR>inst✝ : DecidableEq α<VAR>x : Multiset α<GOAL>((Finset.range (card x + 1)).sup fun k => powersetCard k x) = ∑ x_1 ∈ Finset.range (card x + 1), powersetCard x_1 x
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => rexp (-b * x ^ 2)) =o[atTop] fun x => rexp (-x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>succ a ≤ b * succ a
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>this : cmpLE x y = cmpLE y x<GOAL>(Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>this : cmpLE x y = cmpLE y x<GOAL>(match cmpLE x y with | Ordering.lt => (Ordnode.insert x l).balanceL y r | Ordering.eq => node size✝ l x r | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual = match (cmpLE x y).swap with | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual | Ordering.eq => node size✝ r.dual x l.dual | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>a b : G<GOAL>a * (b * a⁻¹) = b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.223578, 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<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (inr φ))
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>s : Submonoid α<VAR>a : α<VAR>ha : a • ↑s = ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>s : Submonoid α<VAR>a : α<VAR>ha : a • ↑s = ↑s<GOAL>a ∈ a • ↑s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>g : Y → Z<VAR>s : Set Z<GOAL>IsOpen (g ∘ f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>g : Y → Z<VAR>s : Set Z<GOAL>IsOpen (f ⁻¹' (g ⁻¹' s))
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>τ₂₁ : R₂ →+* R<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[τ₂₁] M<VAR>hf : ∀ (c : M₂), f c ∈ p<GOAL>ker (codRestrict p f hf) = ker f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>τ₂₁ : R₂ →+* R<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[τ₂₁] M<VAR>hf : ∀ (c : M₂), f c ∈ p<GOAL>comap f ⊥ = ker f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U V : (Opens ↑↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U V : (Opens ↑↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>(X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop V)))) = (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫ Y.presheaf.map ((opensFunctor f).op.map i)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U V : (Opens ↑↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) = ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫ Y.presheaf.map ((opensFunctor f).op.map i)) ≫ f.c.app (op ((opensFunctor f).obj (unop V)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U V : (Opens ↑↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map (i ≫ eqToHom ⋯) = X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map f.base).map ((opensFunctor f).map i.unop)).op)
<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>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>y : Y<VAR>s : Set X<VAR>t : Set Y<GOAL>𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y
<VAR>S : LightProfinite<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>Function.Surjective ⇑(S.transitionMapLE h)
<VAR>S : LightProfinite<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>Function.Surjective (⇑(S.transitionMapLE h) ∘ ⇑(S.proj m))
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z a : K<VAR>h : ‖a‖ ≤ re a<GOAL>im a = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>x : L<GOAL>∃ k, ↑(weightSpace M 0) ≤ LinearMap.ker ((toEnd R L M) x ^ k)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : CommSemiring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R S A<VAR>t : Set A<VAR>z : A<GOAL>z ∈ Subsemiring.closure (Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) ∪ t) ↔ z ∈ Subsemiring.closure (Set.range ⇑(algebraMap S A) ∪ t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : CommSemiring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R S A<VAR>t : Set A<VAR>z : A<GOAL>Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) = Set.range ⇑(algebraMap S A)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Fintype ι<VAR>f : MultilinearMap R (fun x => R) M₂<VAR>m : ι → R<VAR>this : m = fun i => m i • 1<GOAL>(MultilinearMap.mkPiRing R ι (f fun x => 1)) m = f m
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Fintype ι<VAR>f : MultilinearMap R (fun x => R) M₂<VAR>m : ι → R<VAR>this : m = fun i => m i • 1<GOAL>(MultilinearMap.mkPiRing R ι (f fun x => 1)) m = (∏ i : ι, m i) • f fun i => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hx : (x, y).1 ∈ s<VAR>hy : (x, y).2 ∈ t<GOAL>MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hx : (x, y).1 ∈ s<VAR>hy : (x, y).2 ∈ t<VAR>hst : MeasurableSet (s ×ˢ t)<GOAL>MeasurableSet s ∧ MeasurableSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hx : (x, y).1 ∈ s<VAR>hy : (x, y).2 ∈ t<VAR>hst : MeasurableSet (s ×ˢ t)<VAR>this : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)<GOAL>MeasurableSet s ∧ MeasurableSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hx : (x, y).1 ∈ s<VAR>hy : (x, y).2 ∈ t<VAR>hst : MeasurableSet (s ×ˢ t)<VAR>this✝ : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)<VAR>this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)<GOAL>MeasurableSet s ∧ MeasurableSet t
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type u<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : TopologicalSemiring A<VAR>s : Subalgebra R A<GOAL>IsClosed ↑s.topologicalClosure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>h : Antiperiodic f c<VAR>n : ℕ<GOAL>f (x - ↑n * c) = (-1) ^ n * f x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPullback 0 0 b.inl b.inr
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPullback (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>n : ℕ<GOAL>spectrum ℂ (a ^ n) = (fun x => x ^ n) '' spectrum ℂ a
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>m : M<VAR>p : Submodule R M<GOAL>span R {m} ≤ p ↔ m ∈ p
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<VAR>lv : All (fun x => cmpLT cmp x v) l<VAR>vr : All (fun x => cmpLT cmp v x) r<VAR>hl : Ordered cmp l<VAR>hr : Ordered cmp r<GOAL>Ordered cmp (l.balRight v r)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<VAR>lv : All (fun x => cmpLT cmp x v) l<VAR>vr : All (fun x => cmpLT cmp v x) r<VAR>hl : Ordered cmp l<VAR>hr : Ordered cmp r<GOAL>Ordered cmp (r.reverse.balLeft v l.reverse).reverse
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedDivisionRing R<VAR>inst✝¹ : Algebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>f : C(X, R)<VAR>x : 𝕜<GOAL>x ∈ spectrum 𝕜 f ↔ x ∈ ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f
<VAR>x✝ y x : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hx₂ : x ≤ π<GOAL>arccos (cos x) = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>Kᗮ = ⊤ ↔ K = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>Kᗮ = ⊤ → K = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>h : Kᗮ = ⊤<GOAL>K = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>h : Kᗮ = ⊤<VAR>this : K ⊓ Kᗮ = ⊥<GOAL>K = ⊥
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>b₁ b₂ : β<VAR>l : List α<VAR>h : b₁ ∈ map (const α b₂) ↑l<GOAL>b₁ ∈ replicate (card ↑l) b₂
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<GOAL>Primrec Nat.Partrec.Code.G
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.length).1<GOAL>Primrec Nat.Partrec.Code.G
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.length).1<GOAL>Primrec fun p => (fun a n => Nat.casesOn (ofNat (ℕ × Code) a.length).1 Option.none fun k' => Code.recOn (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) n let y ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) n Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) x) (fun cf cg x x => let z := (unpair n).1; Nat.casesOn (unpair n).2 (Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y) Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair n).1; let m := (unpair n).2; do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<GOAL>Primrec fun p => (fun a n => Nat.casesOn (ofNat (ℕ × Code) a.length).1 Option.none fun k' => Code.recOn (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) n let y ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) n Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) x) (fun cf cg x x => let z := (unpair n).1; Nat.casesOn (unpair n).2 (Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y) Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair n).1; let m := (unpair n).2; do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n : Primrec Prod.snd<GOAL>Primrec fun p => (fun a n => Nat.casesOn (ofNat (ℕ × Code) a.length).1 Option.none fun k' => Code.recOn (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) n let y ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) n Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) x) (fun cf cg x x => let z := (unpair n).1; Nat.casesOn (unpair n).2 (Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y) Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair n).1; let m := (unpair n).2; do let x ← Nat.Partrec.Code.lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n : Primrec Prod.snd<GOAL>Primrec fun p => (fun p k' => Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2 let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x) (fun cf cg x x => let z := (unpair p.2).1; Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y) Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair p.2).1; let m := (unpair p.2).2; do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<GOAL>Primrec fun p => (fun p k' => Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2 let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x) (fun cf cg x x => let z := (unpair p.2).1; Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y) Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair p.2).1; let m := (unpair p.2).2; do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<GOAL>Primrec fun p => (fun p k' => Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2 let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x) (fun cf cg x x => let z := (unpair p.2).1; Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y) Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair p.2).1; let m := (unpair p.2).2; do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<VAR>k' : Primrec Prod.snd<GOAL>Primrec fun p => (fun p k' => Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2 let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x) (fun cf cg x x => let z := (unpair p.2).1; Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y) Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair p.2).1; let m := (unpair p.2).2; do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1))) p.1 p.2