ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : Algebra ℂ A<VAR>inst✝⁴ : StarModule ℂ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℂ A<VAR>a : A<VAR>f : ℝ → ℝ<VAR>this : CompactSpace ↑(σ ℂ a)<VAR>ha : IsSelfAdjoint a<GOAL>cfc f a = cfc (fun x => ↑(f x.re)) a
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<GOAL>DifferentiableWithinAt 𝕜 (fun f => f i) s' f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<GOAL>HasFDerivWithinAt (fun f => f i) ?f' s' f
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<GOAL>((i : ι) → F' i) →L[𝕜] F' i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>this✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a₂ * b₂ ≤ a₁ * b₁<GOAL>a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>this✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a₂ * b₂ ≤ a₁ * b₁<GOAL>¬a₁ < a₂ ∧ ¬b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha✝ : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>this✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a₂ * b₂ ≤ a₁ * b₁<VAR>ha : a₁ < a₂<GOAL>a₁ * b₁ < a₂ * b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ≤ a₂<VAR>hb✝ : b₁ ≤ b₂<VAR>this✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a₂ * b₂ ≤ a₁ * b₁<VAR>hb : b₁ < b₂<GOAL>a₁ * b₁ < a₂ * b₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center < s.radius<VAR>h : ¬p₁ = p₂<GOAL>0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>r : ℚ<GOAL>↑r.num / ↑r.den = r
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : SummableFamily Γ R α<VAR>g : Γ<GOAL>(x • s).hsum.coeff g = (x * s.hsum).coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : SummableFamily Γ R α<VAR>g : Γ<GOAL>∑ᶠ (i : α), ∑ ij ∈ addAntidiagonal ⋯ ⋯ g, x.coeff ij.1 * (s i).coeff ij.2 = ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ g, x.coeff x_1.1 * ∑ᶠ (i : α), (s i).coeff x_1.2
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : SummableFamily Γ R α<VAR>g : Γ<VAR>a : α<GOAL>∑ ij ∈ addAntidiagonal ⋯ ⋯ g, x.coeff ij.1 * (s a).coeff ij.2 = ∑ b ∈ addAntidiagonal ⋯ ⋯ g, x.coeff b.1 * (s a).coeff b.2
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : SummableFamily Γ R α<VAR>g : Γ<GOAL>∀ b ∈ addAntidiagonal ⋯ ⋯ g, (Function.support fun a => (fun i ij => x.coeff ij.1 * (s i).coeff ij.2) a b).Finite
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : SummableFamily Γ R α<VAR>g : Γ<GOAL>∑ b ∈ addAntidiagonal ⋯ ⋯ g, ∑ᶠ (a : α), x.coeff b.1 * (s a).coeff b.2 = ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ g, x.coeff x_1.1 * ∑ᶠ (i : α), (s i).coeff x_1.2
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : HasRightDual X<VAR>f : Y ⟶ Xᘁ<GOAL>(ρ_ Y).inv ≫ Y ◁ η_ X Xᘁ ≫ (α_ Y X Xᘁ).inv ≫ (f ▷ X ≫ ε_ X Xᘁ) ▷ Xᘁ = 𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : HasRightDual X<VAR>f : Y ⟶ Xᘁ<GOAL>𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : HasRightDual X<VAR>f : Y ⟶ Xᘁ<GOAL>𝟙 Y ⊗≫ (f ▷ 𝟙_ C ≫ Xᘁ ◁ η_ X Xᘁ) ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : HasRightDual X<VAR>f : Y ⟶ Xᘁ<GOAL>f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ≫ (λ_ Xᘁ).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : HasRightDual X<VAR>f : Y ⟶ Xᘁ<GOAL>f ⊗≫ ⊗𝟙 = f ≫ (λ_ Xᘁ).inv
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : σ → τ<VAR>x : τ → R<GOAL>comap (rename f) x = x ∘ f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : σ → τ<VAR>x : τ → R<VAR>x✝ : σ<GOAL>comap (rename f) x x✝ = (x ∘ f) x✝
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>i : ι<VAR>hv : LinearIndependent R v<VAR>h : v i = 0<GOAL>(Finsupp.single i 1) i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>i : ι<VAR>hv : LinearIndependent R v<VAR>h : v i = 0<GOAL>0 i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>i : ι<VAR>hv : LinearIndependent R v<VAR>h : v i = 0<GOAL>(Finsupp.total ι M R v) (Finsupp.single i 1) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCancelCommMonoid E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>c x : E<VAR>hx : x ∈ (fun z => c + z) ⁻¹' s<VAR>y : E<VAR>hy : y ∈ (fun z => c + z) ⁻¹' s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<GOAL>Normal F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>hFEp : IsSplittingField F E 0<GOAL>Normal F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<GOAL>Normal F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<VAR>x : E<GOAL>IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<VAR>x : E<VAR>this : FiniteDimensional F E<GOAL>IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<VAR>x : E<VAR>this : FiniteDimensional F E<VAR>hx : IsIntegral F x<GOAL>IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<VAR>x : E<VAR>this : FiniteDimensional F E<VAR>hx : IsIntegral F x<VAR>L : Type u_1 := (p * minpoly F x).SplittingField<GOAL>IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<VAR>x : E<VAR>this : FiniteDimensional F E<VAR>hx : IsIntegral F x<VAR>L : Type u_1 := (p * minpoly F x).SplittingField<VAR>hL : Splits (algebraMap F (p * minpoly F x).SplittingField) p ∧ Splits (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)<GOAL>IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Algebra F K<VAR>E : Type u_3<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra K E<VAR>inst✝⁵ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Field E'<VAR>inst✝ : Algebra F E'<VAR>p : F[X]<VAR>hFEp : IsSplittingField F E p<VAR>hp : p ≠ 0<VAR>x : E<VAR>this : FiniteDimensional F E<VAR>hx : IsIntegral F x<VAR>L : Type u_1 := (p * minpoly F x).SplittingField<GOAL>Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (p * minpoly F x) ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f f'✝ : M →ₗ[R] M'<VAR>g g'✝ : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>f' : M' →ₗ[R] M''<VAR>g' : M'' →ₗ[R] M'<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B'.IsAdjointPair B'' f' g'<VAR>x : M<VAR>y : M''<GOAL>(B'' ((f' ∘ₗ f) x)) y = (B x) ((g ∘ₗ g') y)
<VAR>a b : EReal<GOAL>(a * b)⁻¹ = a⁻¹ * b⁻¹
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>(ENNReal.ofReal x).log = ↑(Real.log x)
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>¬x ≤ 0
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z m : ℤ<VAR>hm : b - a = m • p<GOAL>z • b - z • a = m • z • p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] (↑n - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] ↑(n - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Ioo a b)<GOAL>Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Ioo a b)<GOAL>Tendsto (Subtype.val ∘ f) l (𝓝[>] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsLowerSet α<VAR>s : Set α<GOAL>IsOpen s ↔ IsLowerSet s
<VAR>α✝ β α : Type u<GOAL>Infinite α ↔ ℵ₀ ≤ #α
<VAR>α : Type u_1<VAR>l₁ l₂ l : List α<GOAL>l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ l : List α<VAR>p : l₁ ++ l ~ l₂ ++ l<GOAL>l₁ ~ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<GOAL>𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : DivisionMonoid α<VAR>inst✝ : HasDistribNeg α<VAR>a : α<VAR>n : ℤ<VAR>h : Even n<GOAL>(-1) ^ n = 1
<VAR>x y : ℝ<VAR>h : x ^ 2 ≤ y<GOAL>|x| ≤ √y
<VAR>x y : ℝ<VAR>h : x ^ 2 ≤ y<GOAL>√(x ^ 2) ≤ √y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>s t : Multiset α<VAR>hs : ∀ ⦃x : α⦄, x ∈ s → x ∈ ∅<VAR>ht : ∀ ⦃x : α⦄, x ∈ t → x ∈ ∅<GOAL>card s = n → card t = n → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f g : ι → α<GOAL>(∑ i ∈ s, f i) * ∑ i ∈ s, f i ≤ ↑s.card * ∑ x ∈ s, f x * f x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>s t : Finset α<VAR>a b : α<GOAL>IsUnit s ↔ ∃ a, s = {a}
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)
<VAR>f : Bool → Bool → Bool<VAR>a b : Bool<VAR>m n : ℕ<GOAL>(bif f false false then -[Nat.bitwise (fun x y => !f x y) (Nat.bit a m) (Nat.bit b n)+1] else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) = bit (f a b) (bif f false false then -[Nat.bitwise (fun x y => !f x y) m n+1] else ↑(Nat.bitwise f m n))
<VAR>f : Bool → Bool → Bool<VAR>a b : Bool<VAR>m n : ℕ<GOAL>(bif f false true then -[Nat.bitwise (fun x y => !f x !y) (Nat.bit a m) (Nat.bit (!b) n)+1] else ↑(Nat.bitwise (fun x y => f x !y) (Nat.bit a m) (Nat.bit (!b) n))) = bit (f a b) (bif f false true then -[Nat.bitwise (fun x y => !f x !y) m n+1] else ↑(Nat.bitwise (fun x y => f x !y) m n))
<VAR>f : Bool → Bool → Bool<VAR>a b : Bool<VAR>m n : ℕ<GOAL>(bif f true false then -[Nat.bitwise (fun x y => !f (!x) y) (Nat.bit (!a) m) (Nat.bit b n)+1] else ↑(Nat.bitwise (fun x y => f (!x) y) (Nat.bit (!a) m) (Nat.bit b n))) = bit (f a b) (bif f true false then -[Nat.bitwise (fun x y => !f (!x) y) m n+1] else ↑(Nat.bitwise (fun x y => f (!x) y) m n))
<VAR>f : Bool → Bool → Bool<VAR>a b : Bool<VAR>m n : ℕ<GOAL>(bif f true true then -[Nat.bitwise (fun x y => !f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n)+1] else ↑(Nat.bitwise (fun x y => f (!x) !y) (Nat.bit (!a) m) (Nat.bit (!b) n))) = bit (f a b) (bif f true true then -[Nat.bitwise (fun x y => !f (!x) !y) m n+1] else ↑(Nat.bitwise (fun x y => f (!x) !y) m n))
<VAR>n m l : ℕ<VAR>hln : l ≤ n<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>decide (l ≤ k) = true
<VAR>n m l : ℕ<VAR>hln : l ≤ n<VAR>k : ℕ<VAR>hk : k ∈ Ico n m<GOAL>l ≤ k
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>s : Set ℝ≥0<VAR>hs : ¬BddAbove s<GOAL>sSup s = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>s : Set ℝ≥0<VAR>hs : ¬BddAbove (toReal '' s)<GOAL>sSup s = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>s : Set ℝ≥0<VAR>hs : ¬BddAbove (toReal '' s)<GOAL>sSup (toReal '' s) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>(1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)<GOAL>(1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)<VAR>H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)<GOAL>(1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)<VAR>H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)<VAR>h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n<GOAL>(1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : Lattice α<VAR>inst✝² : Lattice β<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : BoundedOrder β<VAR>f✝ f : α ≃o β<VAR>a✝ : ComplementedLattice α<GOAL>ComplementedLattice β
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : Lattice α<VAR>inst✝² : Lattice β<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : BoundedOrder β<VAR>f✝ f : α ≃o β<VAR>a✝ : ComplementedLattice β<GOAL>ComplementedLattice α
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op
<VAR>n : ℤ<GOAL>sqrt (n * n) = ↑n.natAbs
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<GOAL>ContinuousMul M
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace M✝<VAR>inst✝³ : Mul M✝<VAR>inst✝² : ContinuousMul M✝<VAR>M : Type u<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>hmul : Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<GOAL>∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)