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>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : T<VAR>p : T[X]<VAR>ha : a ≠ 0<GOAL>(C a * p).aroots S = p.aroots S
<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>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : T<VAR>p : T[X]<VAR>ha : a ≠ 0<GOAL>(algebraMap T S) a ≠ 0
<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>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : T<VAR>p : T[X]<VAR>ha : a ≠ 0<GOAL>Function.Injective ⇑(algebraMap T S)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f✝ : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>f : α → β → γ<VAR>h : UniformContinuous₂ f<VAR>x : α<GOAL>UniformContinuousOn (↿f) (univ ×ˢ univ)
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>P : SL(2, R) → Prop<VAR>a b c d : R<VAR>hdet : a * d - b * c = 1<GOAL>!![a, b; c, d].det = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>P : SL(2, R) → Prop<VAR>h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩<VAR>m : Matrix (Fin 2) (Fin 2) R<VAR>hm : m.det = 1<GOAL>P ⟨m, hm⟩
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>P : SL(2, R) → Prop<VAR>h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩<VAR>m : Matrix (Fin 2) (Fin 2) R<VAR>hm : m.det = 1<GOAL>m = !![m 0 0, m 0 1; m 1 0, m 1 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✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<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✝ y✝ z x y : P<GOAL>(pointReflection (midpoint R x y)) x = y
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x y : R<GOAL>eval (x + y) f = ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) + f.sum fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x y : R<GOAL>(f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)) = ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) + f.sum fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : DivisionRing γ<VAR>inst✝² : Module γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<GOAL>∑' (i : β), g • f i = g • ∑' (i : β), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : DivisionRing γ<VAR>inst✝² : Module γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<GOAL>∑' (i : β), 0 • f i = 0 • ∑' (i : β), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : DivisionRing γ<VAR>inst✝² : Module γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hg : g ≠ 0<GOAL>∑' (i : β), g • f i = g • ∑' (i : β), f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>normSq x = 0 ↔ ⟪x, x⟫_𝕜 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>init n (x ^ m) = init n (init n x ^ m)
<VAR>V : Type u<VAR>x : { adj // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }<VAR>v w : V<GOAL>(fun v w => ↑x v w = true) v w → (fun v w => ↑x v w = true) w v
<VAR>V : Type u<VAR>x : { adj // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }<VAR>v : V<GOAL>¬(fun v w => ↑x v w = true) v v
<VAR>V : Type u<VAR>adj : V → V → Bool<VAR>property✝¹ : (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true<VAR>adj' : V → V → Bool<VAR>property✝ : (∀ (x y : V), adj' x y = adj' y x) ∧ ∀ (x : V), ¬adj' x x = true<VAR>h : (fun v w => adj v w = true) = fun v w => adj' v w = true<GOAL>adj = adj'
<VAR>V : Type u<VAR>adj : V → V → Bool<VAR>property✝¹ : (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true<VAR>adj' : V → V → Bool<VAR>property✝ : (∀ (x y : V), adj' x y = adj' y x) ∧ ∀ (x : V), ¬adj' x x = true<VAR>h : (fun v w => adj v w = true) = fun v w => adj' v w = true<VAR>v w : V<GOAL>adj v w = adj' v w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s : Set α<VAR>t : TopologicalSpace α<VAR>t_le : t ≤ inst✝<VAR>t_polish : PolishSpace α<VAR>h : IsClosed s<VAR>h' : IsOpen s<GOAL>IsClopenable sᶜ
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : MonoidalCategory C<VAR>A B X X' Y Y' Z : C<VAR>inst✝⁴ : Closed A<VAR>inst✝³ : Closed B<VAR>A₁ A₂ A₃ : C<VAR>inst✝² : Closed A₁<VAR>inst✝¹ : Closed A₂<VAR>inst✝ : Closed A₃<VAR>f : A₁ ⟶ A₂<VAR>g : A₂ ⟶ A₃<GOAL>pre (f ≫ g) = pre g ≫ pre f
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>f : F → IntermediateField F E := fun x => F⟮α + x • β⟯<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>f : F → IntermediateField F E := fun x => F⟮α + x • β⟯<VAR>x y : F<VAR>hneq : x ≠ y<VAR>heq : f x = f y<GOAL>∃ γ, F⟮α, β⟯ = F⟮γ⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>f : F → IntermediateField F E := fun x => F⟮α + x • β⟯<VAR>x y : F<VAR>hneq : x ≠ y<VAR>heq : f x = f y<GOAL>F⟮α, β⟯ = F⟮α + x • β⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>f : F → IntermediateField F E := fun x => F⟮α + x • β⟯<VAR>x y : F<VAR>hneq : x ≠ y<VAR>heq : f x = f y<GOAL>F⟮α, β⟯ ≤ F⟮α + x • β⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Infinite F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>ϕ : F →+* E<VAR>α β : E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>f : F → IntermediateField F E := fun x => F⟮α + x • β⟯<VAR>x y : F<VAR>hneq : x ≠ y<VAR>heq : f x = f y<GOAL>F⟮α + x • β⟯ ≤ F⟮α, β⟯
<VAR>q : ℍ<GOAL>normSq (exp ℝ q) = normSq (exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im))
<VAR>q : ℍ<GOAL>normSq (exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) = exp ℝ q.re ^ 2 * normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)
<VAR>q : ℍ<GOAL>normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
<VAR>q : ℍ<VAR>hv : ‖q.im‖ = 0<GOAL>normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
<VAR>q : ℍ<VAR>hv : ‖q.im‖ ≠ 0<GOAL>normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) = Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2
<VAR>q : ℍ<GOAL>exp ℝ q.re ^ 2 * (Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2) = exp ℝ q.re ^ 2
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)<VAR>n : ℕ<GOAL>f n = g n
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : (fun n => (bind₁ f) (wittPolynomial p ℤ n)) = fun n => (bind₁ g) (wittPolynomial p ℤ n)<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>n : ℕ<VAR>h : ((fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n => (bind₁ f) (wittPolynomial p ℤ n)) = (fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n => (bind₁ g) (wittPolynomial p ℤ n)<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Icc 0 1<GOAL>x + t • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Icc 0 1<VAR>h : x + t • y = (1 - t) • x + t • (x + y)<GOAL>x + t • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Icc 0 1<VAR>h : x + t • y = (1 - t) • x + t • (x + y)<GOAL>(1 - t) • x + t • (x + y) ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp 𝕜 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑↑((condexpL2 𝕜 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp 𝕜 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑↑((condexpL2 𝕜 𝕜 hm) f) x ∂μ = ⟪indicatorConstLp 2 ⋯ hμs 1, f⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp 𝕜 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_eq_inner : ∫ (x : α) in s, ↑↑↑((condexpL2 𝕜 𝕜 hm) f) x ∂μ = ⟪indicatorConstLp 2 ⋯ hμs 1, ↑((condexpL2 𝕜 𝕜 hm) f)⟫_𝕜<GOAL>∫ (x : α) in s, ↑↑↑((condexpL2 𝕜 𝕜 hm) f) x ∂μ = ⟪indicatorConstLp 2 ⋯ hμs 1, f⟫_𝕜
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<VAR>b' : ↑B := b<VAR>r : b' • ↑(MonoidHom.range f) = ↑(MonoidHom.range f)<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<VAR>b' : ↑B := b<VAR>r : b' • ↑(MonoidHom.range f) = 1 • ↑(MonoidHom.range f)<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<VAR>hb : b ∉ MonoidHom.range f<VAR>b' : ↑B := b<VAR>r : b'⁻¹ ∈ MonoidHom.range f<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>f g : ι →₀ α<VAR>a✝ : ι<GOAL>a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>f g : ι →₀ α<VAR>a✝ : ι<GOAL>¬f a✝ ⊓ g a✝ = 0 ↔ ¬f a✝ = 0 ∧ ¬g a✝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : QuadraticMap 𝕜 E F<VAR>a b : E<GOAL>HasLineDerivAt 𝕜 (⇑f) (polar (⇑f) a b) a b
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝 a) (𝓝 0)<VAR>hga : Tendsto g (𝓝 a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝 a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<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>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x<GOAL>HasFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' (l.get i)).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) 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>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x<GOAL>HasFDerivAt (fun x => (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.finRange l.length)).prod) (∑ x_1 : Fin l.length, (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod • (f' (l.get x_1)).smulRight (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod) 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>𝔸' : Type u_8<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>l : List ι<VAR>x : E<VAR>h : ∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x<GOAL>(∑ i : Fin l.length, (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.take (↑i) (List.finRange l.length))).prod • (proj i).smulRight (List.map ((fun x_1 => f x_1 x) ∘ l.get) (List.drop (↑i).succ (List.finRange l.length))).prod).comp (ContinuousLinearMap.pi fun i => f' (l.get i)) = ∑ x_1 : Fin l.length, (List.map (fun x_2 => f x_2 x) (List.take (↑x_1) (List.map l.get (List.finRange l.length)))).prod • (f' (l.get x_1)).smulRight (List.map (fun x_2 => f x_2 x) (List.drop (↑x_1).succ (List.map l.get (List.finRange l.length)))).prod
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<GOAL>a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<VAR>h₁ : a ^ (Fintype.card F - 1) = 1<GOAL>a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Fintype F<VAR>hF : ringChar F ≠ 2<VAR>a : F<VAR>ha : a ≠ 0<VAR>h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1<GOAL>a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
<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 t : Set α<VAR>x : α<GOAL>s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
<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 t : Set α<VAR>x : α<VAR>h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s<GOAL>s.OrdConnected
<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 t : Set α<VAR>x : α<VAR>h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s<GOAL>(↑(upperClosure s) ∩ ↑(lowerClosure s)).OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hla : la.HasBasis pa sa<GOAL>Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>hla : la.HasBasis pa sa<GOAL>(∀ t ∈ lb, ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeInf α<VAR>inst✝⁵ : BoundedOrder α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(s ∪ t).truncatedInf a = s.truncatedInf a ⊓ t.truncatedInf a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' s : Cycle α<VAR>h : s.Nodup<VAR>hn : s.Nontrivial<GOAL>(s.formPerm h).IsCycle
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>a✝ : List α<VAR>h : Nodup (Quot.mk Setoid.r a✝)<VAR>hn : Nontrivial (Quot.mk Setoid.r a✝)<GOAL>(formPerm (Quot.mk Setoid.r a✝) h).IsCycle
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>map valEmbedding (Icc a b) = Icc ↑a ↑b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : NonUnitalNonAssocRing R<VAR>inst✝ : NoZeroDivisors R<VAR>a b : R<VAR>h : Commute a b<GOAL>a * a = b * b ↔ a = b ∨ a = -b
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>W : Type u_2<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>inst✝¹ : Fintype ↑G.edgeSet<VAR>inst✝ : Fintype ↑G'.edgeSet<GOAL>G.edgeFinset.card = G'.edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>W : Type u_2<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>inst✝¹ : Fintype ↑G.edgeSet<VAR>inst✝ : Fintype ↑G'.edgeSet<GOAL>{ x // x ∈ G.edgeFinset } ≃ { x // x ∈ G'.edgeFinset }
<VAR>V : Type u_1<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>W : Type u_2<VAR>G' : SimpleGraph W<VAR>f : G ≃g G'<VAR>inst✝¹ : Fintype ↑G.edgeSet<VAR>inst✝ : Fintype ↑G'.edgeSet<GOAL>{ x // x ∈ G.edgeSet } ≃ { x // x ∈ G'.edgeSet }
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hiw : ⟪i w, w⟫_ℝ = 1 / 2<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v