ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℂ<GOAL>HasStrictDerivAt sin ((cexp (x * I) + cexp (-x * I)) * 2⁻¹) x
<VAR>x : ℂ<GOAL>(cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹
<VAR>x : ℂ<GOAL>(cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>D H : Subgroup G<VAR>inst✝ : D.FiniteIndex<VAR>hD_le_H : D ≤ H<GOAL>∃ t, ↑t ∈ leftTransversals ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>D H : Subgroup G<VAR>inst✝ : D.FiniteIndex<VAR>hD_le_H : D ≤ H<VAR>t : Set ↥H<VAR>ht : t ∈ leftTransversals ↑(D.subgroupOf H) ∧ 1 ∈ t<GOAL>∃ t, ↑t ∈ leftTransversals ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>D H : Subgroup G<VAR>inst✝ : D.FiniteIndex<VAR>hD_le_H : D ≤ H<VAR>t : Set ↥H<VAR>ht : t ∈ leftTransversals ↑(D.subgroupOf H) ∧ 1 ∈ t<VAR>hf : t.Finite<GOAL>∃ t, ↑t ∈ leftTransversals ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>D H : Subgroup G<VAR>inst✝ : D.FiniteIndex<VAR>hD_le_H : D ≤ H<VAR>t : Set ↥H<VAR>ht : t ∈ leftTransversals ↑(D.subgroupOf H) ∧ 1 ∈ t<VAR>hf : t.Finite<GOAL>⋃ g ∈ hf.toFinset, ↑g • ↑D = ↑H
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Sigma σ)<GOAL>IsClosed s ↔ ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>v v' : V<VAR>p p' : P<GOAL>edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>v v' : V<VAR>p p' : P<GOAL>↑(nndist (v +ᵥ p) (v' +ᵥ p')) ≤ ↑(nndist v v') + ↑(nndist p p')
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>v v' : V<VAR>p p' : P<GOAL>nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x y : R<VAR>I : Ideal R<GOAL>Subsingleton (R ⧸ I) ↔ I = ⊤
<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>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>stdSimplex 𝕜 (Fin 2) = [Pi.single 0 1-[𝕜]Pi.single 1 1]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>stdSimplex 𝕜 (Fin 2) ⊆ [Pi.single 0 1-[𝕜]Pi.single 1 1]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : Fin 2 → 𝕜<VAR>hf₀ : ∀ (x : Fin 2), 0 ≤ f x<VAR>hf₁ : ∑ x : Fin 2, f x = 1<GOAL>f ∈ [Pi.single 0 1-[𝕜]Pi.single 1 1]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : Fin 2 → 𝕜<VAR>hf₀ : ∀ (x : Fin 2), 0 ≤ f x<VAR>hf₁ : f 0 + f 1 = 1<GOAL>f ∈ [Pi.single 0 1-[𝕜]Pi.single 1 1]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : Fin 2 → 𝕜<VAR>hf₀ : ∀ (x : Fin 2), 0 ≤ f x<VAR>hf₁ : f 0 + f 1 = 1<GOAL>(f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 0 = f 0 ∧ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 1 = f 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>(∃ x_1 ∈ Set.Icc 0 1, (lineMap 0 1) x_1 = x) ↔ x ∈ Set.Icc 0 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>(∃ x_1 ∈ Set.Icc 0 1, (1 - x_1) * 0 + x_1 * 1 = x) ↔ x ∈ Set.Icc 0 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Ring α<VAR>inst✝ : StarRing α<VAR>d : ℤ<GOAL>(↑d)ᴴ = ↑d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a✝ : α<VAR>e : α ↪o β<VAR>he : IsUpperSet (range ⇑e)<VAR>a : α<GOAL>⇑e '' Ioi a = Ioi (e a)
<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>inst✝ : SMulZeroClass S R<VAR>r : S<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(r • { toFinsupp := toFinsupp✝ }).coeff n = r • { toFinsupp := toFinsupp✝ }.coeff n
<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>inst✝ : SMulZeroClass S R<VAR>r : S<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(r • toFinsupp✝) n = r • toFinsupp✝ n
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : NoTopOrder α<VAR>a : α<GOAL>∃ b, a < b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖)) / 4
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>range (map f g) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>Submodule.span R (⇑(map f g) '' {t | ∃ m n, m ⊗ₜ[R] n = t}) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
<VAR>m n : ℕ<GOAL>m.Coprime (m + n) ↔ m.Coprime n
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s / closedBall 1 δ = cthickening δ s
<VAR>ι : Type uι<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Module.Free R M₁<VAR>inst✝³ : Module.Finite R M₁<VAR>inst✝² : Module.Free R M₂<VAR>inst✝¹ : Module.Finite R M₂<VAR>inst✝ : Nontrivial R<VAR>B₁ : BilinForm R M₁<VAR>B₂ : BilinForm R M₂<VAR>x✝³ : M₁<VAR>x✝² : M₂<VAR>x✝¹ : M₁<VAR>x✝ : M₂<GOAL>((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂)) x✝³) x✝²)) x✝¹) x✝ = ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂)) x✝³) x✝²)) x✝¹) x✝
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<VAR>hv : v ≠ 0<VAR>r : R<VAR>hr : r ≠ 0<GOAL>SameRay R v (r • v) ↔ 0 < r
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>E' : IntermediateField F E := adjoin F (Set.range v)<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>E' : IntermediateField F E := adjoin F (Set.range v)<VAR>this : Algebra.IsSeparable F ↥E'<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>E' : IntermediateField F E := adjoin F (Set.range v)<VAR>this : Algebra.IsSeparable F ↥E'<VAR>v' : ι → ↥E' := fun i => ⟨v i, ⋯⟩<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>E' : IntermediateField F E := adjoin F (Set.range v)<VAR>this : Algebra.IsSeparable F ↥E'<VAR>v' : ι → ↥E' := fun i => ⟨v i, ⋯⟩<VAR>h' : LinearIndependent F v'<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra A B<VAR>x : B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>hx : IsIntegral A x<GOAL>Irreducible (minpoly A x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra A B<VAR>x : B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>hx : IsIntegral A x<VAR>f g : A[X]<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>he : f * g = minpoly A x<GOAL>f = 1 ∨ g = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra A B<VAR>x : B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>hx : IsIntegral A x<VAR>f g : A[X]<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>he : f * g = minpoly A x<GOAL>IsUnit f ∨ IsUnit g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra A B<VAR>x : B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>hx : IsIntegral A x<VAR>f g : A[X]<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>he : f * g = minpoly A x<VAR>h : ¬IsUnit f ∧ ¬IsUnit g<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra A B<VAR>x : B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>hx : IsIntegral A x<VAR>f g : A[X]<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>he : f * g = minpoly A x<VAR>h : ¬IsUnit f ∧ ¬IsUnit g<VAR>heval : (Polynomial.aeval x) (f * g) = (Polynomial.aeval x) (minpoly A x)<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra A B<VAR>x : B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>hx : IsIntegral A x<VAR>f g : A[X]<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>he : f * g = minpoly A x<VAR>h : ¬IsUnit f ∧ ¬IsUnit g<VAR>heval : (Polynomial.aeval x) f = 0 ∨ (Polynomial.aeval x) g = 0<GOAL>False
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), f z) = ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>ShortComplex.cyclesMap ((natIsoSc' C c i j k hi hk).hom.app K) ≫ (K.sc' i j k).iCycles = K.iCycles j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.sc j).iCycles = K.iCycles j
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>y : I → Bool<VAR>hy : y ∈ C<VAR>i : I<GOAL>↑(ProjRestricts C ⋯ ⟨Proj J y, ⋯⟩) i = ↑(id ⟨Proj J y, ⋯⟩) i
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝ : Monoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => x * a)^[n] 1 = a ^ n
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>x : α<VAR>r : ι → ℝ<VAR>hr : Tendsto r l atTop<GOAL>∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.ball x (r i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>x : α<VAR>r : ι → ℝ<VAR>hr : Tendsto r l atTop<VAR>y : α<GOAL>∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁷ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>F : C ⥤ D<VAR>inst✝⁶ : FinitaryExtensive D<VAR>inst✝⁵ : HasFiniteCoproducts C<VAR>inst✝⁴ : HasPullbacksOfInclusions C<VAR>inst✝³ : PreservesPullbacksOfInclusions F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁷ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>F : C ⥤ D<VAR>inst✝⁶ : FinitaryExtensive D<VAR>inst✝⁵ : HasFiniteCoproducts C<VAR>inst✝⁴ : HasPullbacksOfInclusions C<VAR>inst✝³ : PreservesPullbacksOfInclusions F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<GOAL>IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝⁷ : Category.{v'', u''} D<VAR>X✝ Y✝ : C<VAR>F : C ⥤ D<VAR>inst✝⁶ : FinitaryExtensive D<VAR>inst✝⁵ : HasFiniteCoproducts C<VAR>inst✝⁴ : HasPullbacksOfInclusions C<VAR>inst✝³ : PreservesPullbacksOfInclusions F<VAR>inst✝² : ReflectsLimitsOfShape WalkingCospan F<VAR>inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F<VAR>inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>hc : IsColimit c<VAR>this : (i : Discrete WalkingPair) → (Z : C) → (f : Z ⟶ X ⨿ Y) → PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app i)) F<GOAL>IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), f a =ᶠ[ae (κ a)] g a<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ.withDensity f) a) s✝ = ((κ.withDensity g) a) s✝
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hIY : I ⊂ Y<VAR>hYX : Y ⊆ X<GOAL>M.Dep Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hIY : I ⊂ Y<VAR>hYX : Y ⊆ X<VAR>this : X ⊆ M.E<GOAL>M.Dep Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hIY : I ⊂ Y<VAR>hYX : Y ⊆ X<VAR>this : X ⊆ M.E<GOAL>¬M.Indep Y
<VAR>a✝ b n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>n.floorRoot (a ^ n) = a
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>x : M₂<GOAL>x ∈ map (↑e) p ↔ e.symm x ∈ p
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>x : M₂<GOAL>(∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>r : HomRel C<VAR>A : Type w<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift C A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : r.IsCompatibleWithShift A<VAR>inst✝ : F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(natTransLift r (((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫ isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫ (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫ isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫ (functor r).associator (lift r F hF) (shiftFunctor D a)).inv).app ((functor r).obj X) = (F.commShiftIso a).inv.app X ≫ (lift r F hF).map (((functor r).commShiftIso a).hom.app X)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>r : HomRel C<VAR>A : Type w<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift C A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : r.IsCompatibleWithShift A<VAR>inst✝ : F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫ isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫ (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫ isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫ (functor r).associator (lift r F hF) (shiftFunctor D a)).inv.app X = (F.commShiftIso a).inv.app X ≫ (lift r F hF).map (((functor r).commShiftIso a).hom.app X)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>r : HomRel C<VAR>A : Type w<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift C A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : r.IsCompatibleWithShift A<VAR>inst✝ : F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(((((𝟙 ((shiftFunctor D a).obj ((lift r F hF).obj ((functor r).obj X))) ≫ (shiftFunctor D a).map (𝟙 (F.obj X))) ≫ (F.commShiftIso a).inv.app X) ≫ 𝟙 (F.obj ((shiftFunctor C a).obj X))) ≫ 𝟙 ((lift r F hF).obj ((functor r).obj ((shiftFunctor C a).obj X)))) ≫ (lift r F hF).map (((functor r).commShiftIso a).hom.app X)) ≫ 𝟙 ((lift r F hF).obj ((shiftFunctor (Quotient r) a).obj ((functor r).obj X))) = (F.commShiftIso a).inv.app X ≫ (lift r F hF).map (((functor r).commShiftIso a).hom.app X)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>a : Pseudoelement P<VAR>x : Over P<GOAL>Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} A<VAR>inst✝² : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>inst✝¹ : J.PreservesSheafification F<VAR>inst✝ : HasWeakSheafify J B<VAR>P₁ P₂ : Cᵒᵖ ⥤ A<VAR>f : P₁ ⟶ P₂<VAR>hf : J.W f<GOAL>IsIso ((presheafToSheaf J B).map (whiskerRight f F))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} A<VAR>inst✝² : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>inst✝¹ : J.PreservesSheafification F<VAR>inst✝ : HasWeakSheafify J B<VAR>P₁ P₂ : Cᵒᵖ ⥤ A<VAR>f : P₁ ⟶ P₂<VAR>hf : J.W f<GOAL>J.W (whiskerRight f F)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<GOAL>HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<GOAL>HasDerivAtFilter f f' x (𝓝 x ⊓ 𝓟 s) ↔ Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')