ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : B ⊆ ⇑f ⁻¹' this.extend ⋯<VAR>hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this<VAR>Vinh : Inhabited V<VAR>b : ↑(Basis.ofVectorSpaceIndex K V)<VAR>fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩<GOAL>((hC.constr ℕ) (C.restrict (invFun ⇑f))) (f (hB b)) = hB b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>f : V →ₗ[K] V'<VAR>hf_inj : ker f = ⊥<VAR>B : Set V := Basis.ofVectorSpaceIndex K V<VAR>hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V<VAR>hB₀ : LinearIndependent (ι := { x // x ∈ Set.range ⇑hB }) K Subtype.val<VAR>this : LinearIndependent K fun (x : ↑(⇑f '' B)) => ↑x<VAR>C : Set V' := this.extend ⋯<VAR>BC : B ⊆ ⇑f ⁻¹' this.extend ⋯<VAR>hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this<VAR>Vinh : Inhabited V<VAR>b : ↑(Basis.ofVectorSpaceIndex K V)<VAR>fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩<GOAL>C.restrict (invFun ⇑f) ⟨f ↑b, ⋯⟩ = ↑b
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<GOAL>f ≫ explicitCokernelπ f = 0
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>e_1✝ : (X ⟶ explicitCokernel f) = ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ ((Functor.const WalkingParallelPair).obj (cokernelCocone f).pt).obj WalkingParallelPair.one)<GOAL>0 = (cokernelCocone f).ι.app WalkingParallelPair.zero
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>X : J<VAR>hX : IsInitial X<VAR>F : J ⥤ C<VAR>inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ 𝟙 (F.obj X)
<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>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableSet (range f)
<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>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableSet (f '' univ)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball x δ / {y} = ball (x / y) δ
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<GOAL>p.support.Nonempty ↔ p ≠ 0
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀✝ : WithTop (Box ι)<VAR>I J✝ : Box ι<VAR>i✝ : ι<VAR>G : Type u<VAR>inst✝ : AddCommGroup G<VAR>I₀ : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : ℝ → Box (Fin n) → G<VAR>fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G<VAR>hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J<VAR>J : Box (Fin (n + 1))<VAR>hJ : ↑J ≤ ↑I₀<VAR>j : Fin (n + 1)<VAR>x : ℝ<GOAL>x ∈ Set.Ioo (J.lower j) (J.upper j) → Option.elim' 0 (fun J => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower j x) + Option.elim' 0 (fun J => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper j x) = (fun J => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>I₀✝ : WithTop (Box ι)<VAR>I J✝ : Box ι<VAR>i✝ : ι<VAR>G : Type u<VAR>inst✝ : AddCommGroup G<VAR>I₀ : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : ℝ → Box (Fin n) → G<VAR>fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → Fin n →ᵇᵃ[↑(I₀.face i)] G<VAR>hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : Box (Fin n)), f x J = (fb ⟨x, hx⟩) J<VAR>J : Box (Fin (n + 1))<VAR>hJ : J ≤ I₀<VAR>j : Fin (n + 1)<VAR>x : ℝ<GOAL>x ∈ Set.Ioo (J.lower j) (J.upper j) → Option.elim' 0 (fun J => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitLower j x) + Option.elim' 0 (fun J => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) (J.splitUpper j x) = (fun J => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) J
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter β<GOAL>map f (F ⊓ comap f G) = map f F ⊓ G
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter β<GOAL>map f (F ⊓ comap f G) ≤ map f F ⊓ G
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter β<GOAL>map f F ⊓ G ≤ map f (F ⊓ comap f G)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Inv G<VAR>inst✝⁶ : ContinuousInv G<VAR>inst✝⁵ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>ι : Type u_1<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>inst✝⁴ : TopologicalSpace G₂<VAR>inst✝³ : T2Space G₂<VAR>inst✝² : Inv G₁<VAR>inst✝¹ : Inv G₂<VAR>inst✝ : ContinuousInv G₂<GOAL>IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Inv G<VAR>inst✝⁶ : ContinuousInv G<VAR>inst✝⁵ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>ι : Type u_1<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>inst✝⁴ : TopologicalSpace G₂<VAR>inst✝³ : T2Space G₂<VAR>inst✝² : Inv G₁<VAR>inst✝¹ : Inv G₂<VAR>inst✝ : ContinuousInv G₂<GOAL>IsClosed (⋂ i, {x | x i⁻¹ = (x i)⁻¹})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<VAR>H : Set.InjOn f ↑s<GOAL>(image f s).card = s.card
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.158486, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.158486, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.158486, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₂ ⟶ S₃<GOAL>(φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R✝<VAR>p q r : R✝[X]<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n k : ℕ<GOAL>((1 + X) ^ n).coeff k = ↑(n.choose k)
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<VAR>u : Rˣ<VAR>v : Ray R M<GOAL>-u • v = -(u • v)
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<VAR>u : Rˣ<VAR>v✝ : M<VAR>hv✝ : v✝ ≠ 0<GOAL>-u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝<VAR>s✝ s' t✝ : Set α✝<VAR>f✝ : α✝ → β<VAR>μa μa' : Measure α✝<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f : α✝ → β<VAR>G : Type u_8<VAR>α : Type u_9<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MeasurableSpace α<VAR>s t : Set α<VAR>μ : Measure α<VAR>g : G<VAR>h_qmp : QuasiMeasurePreserving (fun x => g⁻¹ • x) μ μ<VAR>h_ae_eq : s =ᵐ[μ] t<GOAL>g • s =ᵐ[μ] g • t
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x : L<VAR>i : ℕ<VAR>a✝ : Nontrivial R<GOAL>(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (charpoly (φ x)).coeff i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>p : (b : β) → π b<GOAL>p ∈ closedBall x r ↔ p ∈ Set.univ.pi fun b => closedBall (x b) r
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x✝ : E<VAR>a b : 𝕜<VAR>x : E<GOAL>Absorbs 𝕜 s {x} ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, c • x ∈ s
<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 : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d - c * x) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x
<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 : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + -c * x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
<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 : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>(-c)⁻¹ • -∫ (x : ℝ) in d + -c * b..d + -c * a, f x = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x
<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✝³ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>huv : u ≤ᶠ[lt] v<VAR>x : ι<VAR>hx : u x ≤ v x<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) x = (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ (Ioc (u t) (v t))).toReal • c) x
<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✝³ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>huv : u ≤ᶠ[lt] v<VAR>x : ι<VAR>hx : u x ≤ v x<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ) x = (fun t => (μ (Ioc (u t) (v t))).toReal) x
<VAR>k : ℕ<GOAL>bernoulliFun k 0 = ↑(bernoulli k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝³ : DecidablePred p<VAR>inst✝² : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset β<VAR>b x✝¹ : β<VAR>x✝ : x✝¹ ∈ s<GOAL>x✝¹ = b ↔ b = x✝¹
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p : P<GOAL>{p} -ᵥ {p} = {0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<GOAL>K⁻¹ * nndist x y ≤ nndist (f x) (f y)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>W'.addY P Q = (-(Q x * P z)) ^ 3 * P y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>-((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) - W'.a₁ * ((-(Q x * P z)) ^ 2 * P x) * (-(Q x * P z) * P z) - W'.a₃ * (-(Q x * P z) * P z) ^ 3 = (-(Q x * P z)) ^ 3 * P y
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<GOAL>HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
<VAR>x : ℝ<VAR>h₁✝ : x ≠ -1<VAR>h₂ : x ≠ 1<VAR>h₁ : x < -1<GOAL>HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
<VAR>x : ℝ<VAR>h₁✝ : x ≠ -1<VAR>h₂ : x ≠ 1<VAR>h₁ : -1 < x<GOAL>HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
<VAR>x : ℝ<VAR>h₁✝ : x ≠ -1<VAR>h₂✝ : x ≠ 1<VAR>h₁ : -1 < x<VAR>h₂ : x < 1<GOAL>HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
<VAR>x : ℝ<VAR>h₁✝ : x ≠ -1<VAR>h₂✝ : x ≠ 1<VAR>h₁ : -1 < x<VAR>h₂ : 1 < x<GOAL>HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h₁ : s₁ ∈ 𝓝ˢ t₁<VAR>h₂ : s₂ ∈ 𝓝ˢ t₂<GOAL>s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>h₁ : s₁ ∈ 𝓝ˢ t₁<VAR>h₂ : s₂ ∈ 𝓝ˢ t₂<GOAL>s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NormedDivisionRing α<VAR>a✝ a : α<VAR>ha : a ≠ 0<VAR>x y : α<GOAL>edist ((Equiv.mulLeft₀ a ha).toFun x) ((Equiv.mulLeft₀ a ha).toFun y) = ↑‖a‖₊ * edist x y
<VAR>z w : ℂ<GOAL>(z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w
<VAR>R : Type u_1<VAR>m n : ℕ<VAR>m0 : m ≠ 0<VAR>n0 : n ≠ 0<GOAL>Ω (m * n) = Ω m + Ω n
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<GOAL>closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H<GOAL>closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H<VAR>h : G<VAR>hh : h ∈ H<GOAL>h ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H<VAR>g : G<VAR>hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))<VAR>r : G<VAR>hr : r ∈ R<VAR>hh : (fun x x_1 => x * x_1) g r ∈ H<GOAL>(fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H<VAR>g : G<VAR>hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))<VAR>r : G<VAR>hr : r ∈ R<VAR>hh : (fun x x_1 => x * x_1) g r ∈ H<GOAL>⟨r, hr⟩ = ⟨1, hR1⟩
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H<VAR>g : G<VAR>hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))<VAR>r : G<VAR>hr : r ∈ R<VAR>hh : (fun x x_1 => x * x_1) g r ∈ H<GOAL>r * (↑⟨r, hr⟩)⁻¹ ∈ ↑H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H<VAR>g : G<VAR>hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))<VAR>r : G<VAR>hr : r ∈ R<VAR>hh : (fun x x_1 => x * x_1) g r ∈ H<GOAL>r * (↑⟨1, hR1⟩)⁻¹ ∈ ↑H
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ i : ι<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>x✝ : (i : ι) → α i<GOAL>x✝ ∈ (insert i s).pi t ↔ x✝ ∈ eval i ⁻¹' t i ∩ s.pi t
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = powers x hx - ofFinsupp (Finsupp.single 0 1)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>∀ (a : ℕ), ((x • powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective }) a = (powers x hx - ofFinsupp (Finsupp.single 0 1)) a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝¹⁰ : CommRing R₂<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v✝ : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : DecidableEq ι<VAR>S : Type u_9<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Nontrivial S<VAR>inst✝³ : Algebra R₂ S<VAR>inst✝² : Module S M₂<VAR>inst✝¹ : IsScalarTower R₂ S M₂<VAR>inst✝ : NoZeroSMulDivisors R₂ S<VAR>b : Basis ι S M₂<VAR>v : ι → ↥(span R₂ (Set.range ⇑b))<VAR>i✝ j✝ : ι<GOAL>(algebraMap R₂ S).mapMatrix ((restrictScalars R₂ b).toMatrix v) i✝ j✝ = b.toMatrix (fun i => ↑(v i)) i✝ j✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l✝ l₁ l₂ l l' : List M<VAR>h : l.length = l'.length<GOAL>l.prod * l'.prod = (zipWith (fun x x_1 => x * x_1) l l').prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l✝ l₁ l₂ l l' : List M<VAR>h : l.length = l'.length<GOAL>(zipWith (fun x x_1 => x * x_1) l l').prod * (drop l'.length l).prod * (drop l.length l').prod = (zipWith (fun x x_1 => x * x_1) l l').prod
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : DecidableEq R<GOAL>Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : DecidableEq R<GOAL>Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ⊆ p ^ n • f.roots
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>a b : n<VAR>hbj : b ≠ j<VAR>M : Matrix n n α<GOAL>(M * stdBasisMatrix i j c) a b = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t A B : Set β<VAR>a✝ : α<VAR>x : β<VAR>a : α<VAR>s : Set α<VAR>x✝ : α<GOAL>x✝ ∈ (op a • s)⁻¹ ↔ x✝ ∈ a⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>((interpolate s v) r).degree < ↑s.card
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑∅<GOAL>((interpolate ∅ v) r).degree < ↑∅.card
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>h : s.Nonempty<GOAL>((interpolate s v) r).degree < ↑s.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁴ : Group G<VAR>inst✝³ : CommGroup H<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>f : N →* P<VAR>x✝ : M<GOAL>(f.comp 1) x✝ = 1 x✝
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>inst✝⁸ : CommMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>s : Set M<VAR>x x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x<GOAL>ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>inst✝⁸ : CommMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>s : Set M<VAR>x x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x<GOAL>ContMDiffWithinAt I' I n (fun x => (∏ c ∈ t, f c) x) s x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedSemiring α<VAR>inst✝⁴ : LinearOrderedSemiring β<VAR>inst✝³ : FloorSemiring α<VAR>inst✝² : FloorSemiring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b<GOAL>⌊a⌋₊ = ⌊b⌋₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedSemiring α<VAR>inst✝⁴ : LinearOrderedSemiring β<VAR>inst✝³ : FloorSemiring α<VAR>inst✝² : FloorSemiring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a : α<VAR>b : β<VAR>h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b<VAR>h₀ : 0 ≤ a ↔ 0 ≤ b<GOAL>⌊a⌋₊ = ⌊b⌋₊