ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>hd : HasFDerivAt d d' x<GOAL>d x • c' = c'.smulRight (d x)
<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>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>hd : HasFDerivAt d d' x<VAR>z : E<GOAL>(d x • c') z = (c'.smulRight (d x)) z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>b : β<GOAL>LiftRel R ca (pure b) ↔ ∃ a, a ∈ ca ∧ R a b
<VAR>n : Type u_1<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝ : Field R<VAR>A : Matrix n n R<VAR>hAps : Splits (RingHom.id R) A.charpoly<GOAL>A.det = A.charpoly.roots.prod
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b c d : α<VAR>h : IsUnit a<GOAL>a / b / a = b⁻¹
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<GOAL>∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>c : ℝ<VAR>cmem : c ∈ Ioo a b<VAR>hc : (b - a) * f' c = (f b - f a) * 1<GOAL>∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>c : ℝ<VAR>cmem : c ∈ Ioo a b<VAR>hc : (b - a) * f' c = (f b - f a) * 1<GOAL>f' c = (f b - f a) / (b - a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>hf : LocallyIntegrable f μ<VAR>s : Set X<VAR>hs : MeasurableSet s<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : IntegrableOn f U μ<GOAL>IntegrableAtFilter (s.indicator f) (𝓝 x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω✝ : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : CountablyGenerated γ<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>Ω : Type u_5<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : StandardBorelSpace Ω<VAR>η : Kernel α ℝ<VAR>a : α<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>((borelMarkovFromReal Ω η) a) s = if (η a) (range (embeddingReal Ω))ᶜ = 0 then (η a) (embeddingReal Ω '' s) else (embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω✝ : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : CountablyGenerated γ<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>Ω : Type u_5<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : StandardBorelSpace Ω<VAR>η : Kernel α ℝ<VAR>a : α<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>he : MeasurableEmbedding (embeddingReal Ω)<GOAL>((borelMarkovFromReal Ω η) a) s = if (η a) (range (embeddingReal Ω))ᶜ = 0 then (η a) (embeddingReal Ω '' s) else (embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω✝ : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : CountablyGenerated γ<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>Ω : Type u_5<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : StandardBorelSpace Ω<VAR>η : Kernel α ℝ<VAR>a : α<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>he : MeasurableEmbedding (embeddingReal Ω)<GOAL>(if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a) else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))) s = if (η a) (range (embeddingReal Ω))ᶜ = 0 then (η a) (embeddingReal Ω '' s) else (embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.Adj v w<VAR>a✝ : V<GOAL>a✝ ∈ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) ↔ a✝ ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.Adj v w<VAR>a✝ : V<GOAL>¬G.Adj v a✝ → ¬G.Adj w a✝ → ¬(a✝ = w ∨ a✝ = v)
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : Cone F<GOAL>Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℕ<GOAL>(1 / a) ^ n = 1 / a ^ n
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>hX : (Ideal.span {X}).IsMaximal<GOAL>LocalRing.maximalIdeal k⟦X⟧ = Ideal.span {X}
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<GOAL>s ≤ s + t
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(aeval fun i => (map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) = (aeval fun i => (rename (Prod.mk i)) (W_ R n)) Φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(fun i => (map (Int.castRingHom R)) (wittStructureInt p Φ i)) = fun i => (map (Int.castRingHom R)) (wittStructureInt p Φ i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(fun i => (rename (Prod.mk i)) (W_ R n)) = fun i => (map (Int.castRingHom R)) ((rename (Prod.mk i)) (W_ ℤ n))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>(¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b c : α<GOAL>(IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ<VAR>z : α × β<GOAL>z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq β<VAR>i : β<GOAL>i ∈ image Prod.snd (s ×ˢ t) → i ∈ t
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<GOAL>F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<VAR>h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ<GOAL>finrank (↥F⟮α⟯) E = finrank (↥⊤) E
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<VAR>h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ<VAR>this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra<GOAL>finrank (↥F⟮α⟯) E = finrank (↥⊤) E
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<VAR>h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ<VAR>this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra<VAR>this : Algebra.IsSeparable (↥F⟮α⟯) E<GOAL>finrank (↥F⟮α⟯) E = finrank (↥⊤) E
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<VAR>h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ<VAR>this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra<VAR>this : Algebra.IsSeparable (↥F⟮α⟯) E<GOAL>∃ x, ∀ (y : E →ₐ[↥F⟮α⟯] A), y = x
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝¹¹ : Field F✝<VAR>inst✝¹⁰ : Field E✝<VAR>inst✝⁹ : Algebra F✝ E✝<VAR>inst✝⁸ : FiniteDimensional F✝ E✝<VAR>inst✝⁷ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>inst✝³ : FiniteDimensional F E<VAR>inst✝² : Algebra.IsSeparable F E<VAR>A : Type u_5<VAR>inst✝¹ : Field A<VAR>inst✝ : Algebra F A<VAR>hA : ∀ (x : E), Splits (algebraMap F A) (minpoly F x)<VAR>α : E<VAR>φ : E →ₐ[F] A<VAR>h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ<VAR>this✝ : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra<VAR>this : Algebra.IsSeparable (↥F⟮α⟯) E<GOAL>∀ (x : E), Splits (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1✝ : WSeq α<VAR>s2✝ : WSeq β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1✝ s2✝<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<VAR>s1 : WSeq γ<VAR>s2 : WSeq δ<VAR>h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<GOAL>Computation.LiftRel (LiftRelO S fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) (map f1 s).destruct (map f2 t).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1✝ : WSeq α<VAR>s2✝ : WSeq β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1✝ s2✝<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<VAR>s1 : WSeq γ<VAR>s2 : WSeq δ<VAR>h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<GOAL>Computation.LiftRel (LiftRelO S fun s1 s2 => ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x) (Computation.map (Option.map (Prod.map f1 (map f1))) s.destruct) (Computation.map (Option.map (Prod.map f2 (map f2))) t.destruct)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1✝ : WSeq α<VAR>s2✝ : WSeq β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1✝ s2✝<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<VAR>s1 : WSeq γ<VAR>s2 : WSeq δ<VAR>h✝ : (fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO S (fun s1 s2 => ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x) (Option.map (Prod.map f1 (map f1)) a) (Option.map (Prod.map f2 (map f2)) b)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<GOAL>¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<GOAL>((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<GOAL>(∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) → (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<GOAL>((∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1) → ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y a b : α<VAR>hab : a ≤ b<VAR>hfba : f b < f a<VAR>c d : α<VAR>hcd : c ≤ d<VAR>hfcd : f c < f d<GOAL>∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y a b : α<VAR>hab : a ≤ b<VAR>hfba : f b < f a<VAR>c d : α<VAR>hcd : c ≤ d<VAR>hfcd : f c < f d<VAR>hda : d ≤ a<GOAL>∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y a b : α<VAR>hab : a ≤ b<VAR>hfba : f b < f a<VAR>c d : α<VAR>hcd : c ≤ d<VAR>hfcd : f c < f d<VAR>had : a ≤ d<GOAL>∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y a b : α<VAR>hab : a ≤ b<VAR>hfba : f b < f a<VAR>c d : α<VAR>hcd : c ≤ d<VAR>hfcd : f c < f d<VAR>had : a ≤ d<VAR>hac : a ≤ c<GOAL>∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>x y a b : α<VAR>hab : a ≤ b<VAR>hfba : f b < f a<VAR>c d : α<VAR>hcd : c ≤ d<VAR>hfcd : f c < f d<VAR>had : a ≤ d<VAR>hca : c ≤ a<GOAL>∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>fi : (i : ι) → M i →* N<GOAL>∀ (x y : FreeMonoid ((i : ι) × M i)), Rel M x y → (Con.ker (FreeMonoid.lift fun p => (fi p.fst) p.snd)) x y
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>fi : (i : ι) → M i →* N<GOAL>∀ (x y : FreeMonoid ((i : ι) × M i)), Rel M x y → (FreeMonoid.lift fun p => (fi p.fst) p.snd) x = (FreeMonoid.lift fun p => (fi p.fst) p.snd) y
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>fi : (i : ι) → M i →* N<VAR>i : ι<VAR>x : M i<GOAL>((fun f i => f.comp of) ((fun fi => (conGen (Rel M)).lift (FreeMonoid.lift fun p => (fi p.fst) p.snd) ⋯) fi) i) x = (fi i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>is ts : List α<GOAL>(is ++ ts).permutations = map (fun x => x ++ ts) is.permutations ++ ts.permutationsAux is.reverse
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>h : ∀ x ∈ s, ∏ a ∈ filter (fun y => y ≈ x) s, f a = 1<GOAL>∏ x ∈ s, f x = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>h : ∀ x ∈ s, ∏ a ∈ filter (fun y => y ≈ x) s, f a = 1<GOAL>∀ x ∈ image Quotient.mk'' s, ∏ y ∈ filter (fun x_1 => ⟦x_1⟧ = x) s, f y = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>h : ∀ x ∈ s, ∏ a ∈ filter (fun y => y ≈ x) s, f a = 1<VAR>xbar : Quotient R<VAR>xbar_in_s : xbar ∈ image Quotient.mk'' s<GOAL>∏ y ∈ filter (fun x => ⟦x⟧ = xbar) s, f y = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>h : ∀ x ∈ s, ∏ a ∈ filter (fun y => y ≈ x) s, f a = 1<VAR>x : α<VAR>x_in_s : x ∈ s<VAR>xbar_in_s : Quotient.mk'' x ∈ image Quotient.mk'' s<GOAL>∏ y ∈ filter (fun x_1 => ⟦x_1⟧ = Quotient.mk'' x) s, f y = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>x : α<VAR>x_in_s : x ∈ s<VAR>xbar_in_s : Quotient.mk'' x ∈ image Quotient.mk'' s<VAR>h : ∀ x ∈ s, ∏ x ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f x = 1<GOAL>∏ y ∈ filter (fun x_1 => ⟦x_1⟧ = Quotient.mk'' x) s, f y = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u✝ v : Finset α<VAR>a b : α<VAR>s t u : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ s ∪ (t ∪ u) ↔ x✝ ∈ t ∪ (s ∪ u)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>s : List α<GOAL>s.prod = ∏ m ∈ s.toFinset, m ^ count m s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : UniformSpace E<VAR>inst✝ : UniformAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ContinuousAt (⇑p) 0<GOAL>UniformContinuous ⇑p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : UniformSpace E<VAR>inst✝ : UniformAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp✝ : ContinuousAt (⇑p) 0<VAR>hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)<GOAL>UniformContinuous ⇑p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : UniformSpace E<VAR>inst✝ : UniformAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp✝ : ContinuousAt (⇑p) 0<VAR>hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)<GOAL>Tendsto ((fun p => dist p.1 p.2) ∘ fun x => (p x.1, p x.2)) (comap (fun x => x.1 - x.2) (𝓝 0)) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<GOAL>(M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)
<VAR>F✝ : Type u<VAR>K✝ : Type v<VAR>A✝ : Type w<VAR>inst✝¹⁰ : DivisionRing F✝<VAR>inst✝⁹ : DivisionRing K✝<VAR>inst✝⁸ : AddCommGroup A✝<VAR>inst✝⁷ : Module F✝ K✝<VAR>inst✝⁶ : Module K✝ A✝<VAR>inst✝⁵ : Module F✝ A✝<VAR>inst✝⁴ : IsScalarTower F✝ K✝ A✝<VAR>F : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Ring A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : Algebra F A<VAR>hp : Nat.Prime (finrank F A)<VAR>K : Subalgebra F A<GOAL>K = ⊥ ∨ K = ⊤