ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>r : R<VAR>ha : (X + C r).natDegree = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>r : R<VAR>ha : 1 = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b : α<GOAL>a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<GOAL>IsAlgebraic R ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<GOAL>IsAlgebraic R (?m.42391 ↑n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<GOAL>R →+* A
<VAR>c : ℝ<VAR>hc : 1 < c<VAR>i : ℕ<GOAL>(1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
<VAR>c : ℝ<VAR>hc : 1 < c<VAR>i : ℕ<VAR>cpos : 0 < c<GOAL>(1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
<VAR>c : ℝ<VAR>hc : 1 < c<VAR>cpos : 0 < c<GOAL>(1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊
<VAR>c : ℝ<VAR>hc : 1 < c<VAR>i : ℕ<VAR>cpos : 0 < c<VAR>hi : i ≠ 0<GOAL>(1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<VAR>Eu : Type (max uE uF uG) := ULift.{max uF uG, uE} E<VAR>Fu : Type (max uE uF uG) := ULift.{max uE uG, uF} F<VAR>Gu : Type (max uE uF uG) := ULift.{max uE uF, uG} G<VAR>isoE : Eu ≃L[𝕜] E<VAR>isoF : Fu ≃L[𝕜] F<VAR>isoG : Gu ≃L[𝕜] G<VAR>fu : Eu → Fu := (⇑isoF.symm ∘ f) ∘ ⇑isoE<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<VAR>Eu : Type (max uE uF uG) := ULift.{max uF uG, uE} E<VAR>Fu : Type (max uE uF uG) := ULift.{max uE uG, uF} F<VAR>Gu : Type (max uE uF uG) := ULift.{max uE uF, uG} G<VAR>isoE : Eu ≃L[𝕜] E<VAR>isoF : Fu ≃L[𝕜] F<VAR>isoG : Gu ≃L[𝕜] G<VAR>fu : Eu → Fu := (⇑isoF.symm ∘ f) ∘ ⇑isoE<VAR>fu_diff : ContDiffOn 𝕜 n fu (⇑isoE ⁻¹' s)<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<VAR>Eu : Type (max uE uF uG) := ULift.{max uF uG, uE} E<VAR>Fu : Type (max uE uF uG) := ULift.{max uE uG, uF} F<VAR>Gu : Type (max uE uF uG) := ULift.{max uE uF, uG} G<VAR>isoE : Eu ≃L[𝕜] E<VAR>isoF : Fu ≃L[𝕜] F<VAR>isoG : Gu ≃L[𝕜] G<VAR>fu : Eu → Fu := (⇑isoF.symm ∘ f) ∘ ⇑isoE<VAR>fu_diff : ContDiffOn 𝕜 n fu (⇑isoE ⁻¹' s)<VAR>gu : Fu → Gu := (⇑isoG.symm ∘ g) ∘ ⇑isoF<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<VAR>Eu : Type (max uE uF uG) := ULift.{max uF uG, uE} E<VAR>Fu : Type (max uE uF uG) := ULift.{max uE uG, uF} F<VAR>Gu : Type (max uE uF uG) := ULift.{max uE uF, uG} G<VAR>isoE : Eu ≃L[𝕜] E<VAR>isoF : Fu ≃L[𝕜] F<VAR>isoG : Gu ≃L[𝕜] G<VAR>fu : Eu → Fu := (⇑isoF.symm ∘ f) ∘ ⇑isoE<VAR>fu_diff : ContDiffOn 𝕜 n fu (⇑isoE ⁻¹' s)<VAR>gu : Fu → Gu := (⇑isoG.symm ∘ g) ∘ ⇑isoF<VAR>gu_diff : ContDiffOn 𝕜 n gu (⇑isoF ⁻¹' t)<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<VAR>Eu : Type (max uE uF uG) := ULift.{max uF uG, uE} E<VAR>Fu : Type (max uE uF uG) := ULift.{max uE uG, uF} F<VAR>Gu : Type (max uE uF uG) := ULift.{max uE uF, uG} G<VAR>isoE : Eu ≃L[𝕜] E<VAR>isoF : Fu ≃L[𝕜] F<VAR>isoG : Gu ≃L[𝕜] G<VAR>fu : Eu → Fu := (⇑isoF.symm ∘ f) ∘ ⇑isoE<VAR>fu_diff : ContDiffOn 𝕜 n fu (⇑isoE ⁻¹' s)<VAR>gu : Fu → Gu := (⇑isoG.symm ∘ g) ∘ ⇑isoF<VAR>gu_diff : ContDiffOn 𝕜 n gu (⇑isoF ⁻¹' t)<VAR>main : ContDiffOn 𝕜 n (gu ∘ fu) (⇑isoE ⁻¹' s)<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<VAR>Eu : Type (max uE uF uG) := ULift.{max uF uG, uE} E<VAR>Fu : Type (max uE uF uG) := ULift.{max uE uG, uF} F<VAR>Gu : Type (max uE uF uG) := ULift.{max uE uF, uG} G<VAR>isoE : Eu ≃L[𝕜] E<VAR>isoF : Fu ≃L[𝕜] F<VAR>isoG : Gu ≃L[𝕜] G<VAR>fu : Eu → Fu := (⇑isoF.symm ∘ f) ∘ ⇑isoE<VAR>fu_diff : ContDiffOn 𝕜 n fu (⇑isoE ⁻¹' s)<VAR>gu : Fu → Gu := (⇑isoG.symm ∘ g) ∘ ⇑isoF<VAR>gu_diff : ContDiffOn 𝕜 n gu (⇑isoF ⁻¹' t)<VAR>main : ContDiffOn 𝕜 n (gu ∘ fu) (⇑isoE ⁻¹' s)<VAR>this : gu ∘ fu = (⇑isoG.symm ∘ g ∘ f) ∘ ⇑isoE<GOAL>ContDiffOn 𝕜 n (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>↑s = Set.univ ↔ s = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p✝ : α → Prop<VAR>f : β → α<VAR>p : ℝ≥0∞<VAR>hμs : p < μ s<VAR>s_mble : MeasurableSet s<GOAL>μ sᶜ < 1 - p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p✝ : α → Prop<VAR>f : β → α<VAR>p : ℝ≥0∞<VAR>hμs : p < μ s<VAR>s_mble : MeasurableSet s<GOAL>1 - μ s < 1 - p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p✝ : α → Prop<VAR>f : β → α<VAR>p : ℝ≥0∞<VAR>hμs : p < μ s<VAR>s_mble : MeasurableSet s<GOAL>1 - (1 - p) < μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p✝ : α → Prop<VAR>f : β → α<VAR>p : ℝ≥0∞<VAR>hμs : p < μ s<VAR>s_mble : MeasurableSet s<GOAL>1 - (1 - p) = p
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>im (r • z) = r * im z
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>x✝¹ x✝ : RatFunc K<VAR>toFractionRing✝¹ toFractionRing✝ : FractionRing K[X]<GOAL>{ toFun := toFractionRing, invFun := ofFractionRing, left_inv := ⋯, right_inv := ⋯ }.toFun ({ toFractionRing := toFractionRing✝¹ } + { toFractionRing := toFractionRing✝ }) = { toFun := toFractionRing, invFun := ofFractionRing, left_inv := ⋯, right_inv := ⋯ }.toFun { toFractionRing := toFractionRing✝¹ } + { toFun := toFractionRing, invFun := ofFractionRing, left_inv := ⋯, right_inv := ⋯ }.toFun { toFractionRing := toFractionRing✝ }
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>x✝¹ x✝ : RatFunc K<VAR>toFractionRing✝¹ toFractionRing✝ : FractionRing K[X]<GOAL>{ toFun := toFractionRing, invFun := ofFractionRing, left_inv := ⋯, right_inv := ⋯ }.toFun ({ toFractionRing := toFractionRing✝¹ } * { toFractionRing := toFractionRing✝ }) = { toFun := toFractionRing, invFun := ofFractionRing, left_inv := ⋯, right_inv := ⋯ }.toFun { toFractionRing := toFractionRing✝¹ } * { toFun := toFractionRing, invFun := ofFractionRing, left_inv := ⋯, right_inv := ⋯ }.toFun { toFractionRing := toFractionRing✝ }
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁸ : DivisionRing K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>W : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Module A V<VAR>inst✝³ : AddCommGroup W<VAR>inst✝² : Module K W<VAR>inst✝¹ : Module A W<VAR>inst✝ : LinearMap.CompatibleSMul V W K A<VAR>h : finrank K W = 1<VAR>f : V →ₗ[A] W<VAR>w : f ≠ 0<GOAL>Surjective ⇑(↑K f)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁸ : DivisionRing K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>W : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Module A V<VAR>inst✝³ : AddCommGroup W<VAR>inst✝² : Module K W<VAR>inst✝¹ : Module A W<VAR>inst✝ : LinearMap.CompatibleSMul V W K A<VAR>h : finrank K W = 1<VAR>f : V →ₗ[A] W<VAR>w : f ≠ 0<VAR>v : V<VAR>n : f v ≠ 0 v<GOAL>Surjective ⇑(↑K f)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁸ : DivisionRing K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>W : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Module A V<VAR>inst✝³ : AddCommGroup W<VAR>inst✝² : Module K W<VAR>inst✝¹ : Module A W<VAR>inst✝ : LinearMap.CompatibleSMul V W K A<VAR>h : finrank K W = 1<VAR>f : V →ₗ[A] W<VAR>w : f ≠ 0<VAR>v : V<VAR>n : f v ≠ 0 v<VAR>z : W<GOAL>∃ a, (↑K f) a = z
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁸ : DivisionRing K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>W : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Module A V<VAR>inst✝³ : AddCommGroup W<VAR>inst✝² : Module K W<VAR>inst✝¹ : Module A W<VAR>inst✝ : LinearMap.CompatibleSMul V W K A<VAR>h : finrank K W = 1<VAR>f : V →ₗ[A] W<VAR>w : f ≠ 0<VAR>v : V<VAR>n : f v ≠ 0 v<VAR>c : K<GOAL>∃ a, (↑K f) a = c • f v
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' x : ℂ<VAR>h : HasDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt f (f' • 1) s x
<VAR>G : Type u_1<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b a : G<VAR>n : ℕ<GOAL>a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
<VAR>G : Type u_1<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b a : G<VAR>n : ℕ<GOAL>a ^ Int.negSucc n = (a ^ ↑(n + 1))⁻¹
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : α → α<VAR>a : α<GOAL>map (fun x => f^[x] a) (range n) = iterate f a n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R S)<VAR>s : S<GOAL>(trace R S) s = 0 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : ℕ → α<VAR>n✝ : ℕ<GOAL>disjointed f (n✝ + 1) = f (n✝ + 1) ⊓ ⨅ i, ⨅ (_ : i < n✝ + 1), (f i)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : ℕ → α<VAR>n✝ : ℕ<GOAL>f (n✝ + 1) ⊓ ⨅ i, ⨅ (_ : i ≤ n✝), (f i)ᶜ = f (n✝ + 1) ⊓ ⨅ i, ⨅ (_ : i < n✝ + 1), (f i)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>f : ℕ → α<VAR>n✝ i : ℕ<GOAL>⨅ (_ : i ≤ n✝), (f i)ᶜ = ⨅ (_ : i < n✝ + 1), (f i)ᶜ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Injective (pseudoApply f)<VAR>a : Pseudoelement P<VAR>ha : pseudoApply f a = 0<GOAL>a = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>h : Function.Injective (pseudoApply f)<VAR>a : Pseudoelement P<VAR>ha : pseudoApply f a = pseudoApply f 0<GOAL>a = 0
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : Set G<VAR>V_open : IsOpen V<VAR>V_mem : 1 ∈ V<VAR>hV : V * V ⊆ U<GOAL>∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : Set G<VAR>V_open : IsOpen V<VAR>V_mem : 1 ∈ V<VAR>hV : V * V ⊆ U<VAR>W : Set G<VAR>W_mem : W ∈ 𝓝 1<VAR>W_closed : IsClosed W<VAR>hW : W ⊆ V<GOAL>∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : Set G<VAR>V_open : IsOpen V<VAR>V_mem : 1 ∈ V<VAR>hV : V * V ⊆ U<VAR>W : Set G<VAR>W_mem : W ∈ 𝓝 1<VAR>W_closed : IsClosed W<VAR>hW : W ⊆ V<GOAL>W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ U
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<GOAL>Mᵀ.det = M.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<GOAL>∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<GOAL>∀ (x : Perm n), ↑↑(sign x) * ∏ i : n, Mᵀ (x i) i = ↑↑(sign x⁻¹) * ∏ i : n, M (x⁻¹ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>σ : Perm n<GOAL>↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ↑↑(sign σ⁻¹) * ∏ i : n, M (σ⁻¹ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>σ : Perm n<GOAL>↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ↑↑(sign σ) * ∏ i : n, M (σ⁻¹ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>σ : Perm n<GOAL>∏ i : n, Mᵀ (σ i) i = ∏ i : n, M (σ⁻¹ i) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>σ : Perm n<GOAL>∀ (x : n), Mᵀ (σ x) x = M (σ⁻¹ (σ x)) (σ x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : T1Space X<VAR>inst✝¹ : DecidableEq X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>x x' : X<VAR>y : Y<VAR>hne : x' ≠ x<GOAL>ContinuousAt (update f x y) x' ↔ ContinuousAt f x'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<VAR>h : xs.Nodup<GOAL>xs.sym2.Nodup
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>A.X.map f ≫ A.counit.app Y✝ = A.counit.app X✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>A.counit.app X✝ ≫ 𝟙 (𝟙_ D) = A.counit.app X✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>A.X.map f ≫ A.comul.app Y✝ = A.comul.app X✝ ≫ (A.X.map f ⊗ A.X.map f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X : C<GOAL>A.X.map (𝟙 X) = 𝟙 (A.X.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>A.X.map (f ≫ g) = A.X.map f ≫ A.X.map g
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ f : Perm α<GOAL>f⁻¹.IsThreeCycle → f.IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ f : Perm α<GOAL>f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedRing α<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>inst✝ : Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g (σ i) = ∑ i : ι, f i • g i ↔ Antivary f (g ∘ ⇑σ)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b b' : β a<VAR>s : AList β<GOAL>(insert a b' (insert a b s)).entries = (insert a b' s).entries
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ c : α<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>(Icc a b).erase a = Ioc a b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F : C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>(({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (𝟙 F)).app P).f = ((𝟙 ({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.obj F)).app P).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<GOAL>(({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map (φ ≫ φ')).app P).f = (({ obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ ≫ { obj := FunctorExtension₁.obj, map := fun {X Y} => FunctorExtension₁.map }.map φ').app P).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<GOAL>(F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = (F.map P.p).f ≫ (φ.app P.X).f ≫ (G.map P.p).f ≫ (φ'.app P.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<VAR>h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p<GOAL>(F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = (F.map P.p).f ≫ (φ.app P.X).f ≫ (G.map P.p).f ≫ (φ'.app P.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<VAR>h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p<VAR>h' : F.map (P.p ≫ P.p) = F.map P.p<GOAL>(F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = (F.map P.p).f ≫ (φ.app P.X).f ≫ (G.map P.p).f ≫ (φ'.app P.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<VAR>h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f<VAR>h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f<GOAL>(F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = (F.map P.p).f ≫ (φ.app P.X).f ≫ (G.map P.p).f ≫ (φ'.app P.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.20465, u_1} C<VAR>inst✝¹ : Category.{?u.20469, u_2} D<VAR>inst✝ : Category.{?u.20473, u_3} E<VAR>F G H : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>φ' : G ⟶ H<VAR>P : Karoubi C<VAR>h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f<VAR>h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f<GOAL>(F.map P.p).f ≫ (φ.app P.X).f ≫ (φ'.app P.X).f = (F.map P.p).f ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ (φ'.app P.X).f