ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>r : ℝ<GOAL>Adapted ℱ fun i => stoppedValue f (leastGE f r i)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>r : ℝ<GOAL>∀ (i : ℕ), Integrable (stoppedValue f (leastGE f r i)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 2 / (1 - 2 / rexp 1) ≤ x<GOAL>x / rexp 1 < ↑⌊x / 2⌋₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 2 / (1 - 2 / rexp 1) ≤ x<GOAL>x / rexp 1 ≤ x / 2 - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 2 / (1 - 2 / rexp 1) ≤ x<VAR>this : 0 < 1 - 2 / rexp 1<GOAL>x / rexp 1 ≤ x / 2 - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 2 / (1 - 2 / rexp 1) ≤ x<VAR>this : 0 < 1 - 2 / rexp 1<GOAL>0 < 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>x : ℝ<VAR>hx : 2 / (1 - 2 / rexp 1) ≤ x<VAR>this : 0 < 1 - 2 / rexp 1<GOAL>2 ≠ 0
<VAR>P✝ : TopCat → Prop<VAR>α : Type w<VAR>inst✝² : Finite α<VAR>X : α → CompHausLike P✝<VAR>inst✝¹ : HasExplicitFiniteCoproduct X<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitFiniteCoproducts P<VAR>a : α<GOAL>OpenEmbedding ⇑(Sigma.ι X a)
<VAR>P✝ : TopCat → Prop<VAR>α : Type w<VAR>inst✝² : Finite α<VAR>X : α → CompHausLike P✝<VAR>inst✝¹ : HasExplicitFiniteCoproduct X<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitFiniteCoproducts P<VAR>a : α<GOAL>OpenEmbedding (⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘ ⇑(Sigma.ι X a))
<VAR>P✝ : TopCat → Prop<VAR>α : Type w<VAR>inst✝² : Finite α<VAR>X : α → CompHausLike P✝<VAR>inst✝¹ : HasExplicitFiniteCoproduct X<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitFiniteCoproducts P<VAR>a : α<VAR>e_2✝ : ↑(finiteCoproduct.cofan X).pt.toTop = (forget (CompHausLike P✝)).obj (finiteCoproduct X)<GOAL>⇑(homeoOfIso ((colimit.isColimit (Discrete.functor X)).coconePointUniqueUpToIso (finiteCoproduct.isColimit X))) ∘ ⇑(Sigma.ι X a) = ⇑(finiteCoproduct.ι X a)
<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>m : ℕ<GOAL>∀ {n : ℕ}, IsPrimitiveRoot μ n → m.Coprime n → minpoly ℤ μ = minpoly ℤ (μ ^ m)
<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>m n✝ : ℕ<GOAL>IsPrimitiveRoot μ n✝ → Nat.Coprime 0 n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ 0)
<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>m n✝ : ℕ<GOAL>∀ (x : ℕ), IsUnit x → IsPrimitiveRoot μ n✝ → x.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ x)
<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>m n✝ : ℕ<GOAL>∀ (a p : ℕ), a ≠ 0 → Prime p → (IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) → IsPrimitiveRoot μ n✝ → (p * a).Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : factorization a = factorization b<GOAL>a ~ᵤ b
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : normalizedFactors a = normalizedFactors b<GOAL>a ~ᵤ b
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<VAR>hx : z ∣ x<VAR>hy : z ∣ y<GOAL>z ∣ gcd x y
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<VAR>hx : Ideal.span {x} ≤ Ideal.span {z}<VAR>hy : Ideal.span {y} ≤ Ideal.span {z}<GOAL>Ideal.span {gcd x y} ≤ Ideal.span {z}
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<VAR>hx : Ideal.span {x} ≤ Ideal.span {z}<VAR>hy : Ideal.span {y} ≤ Ideal.span {z}<GOAL>Ideal.span {x} ≤ Ideal.span {z} ∧ Ideal.span {y} ≤ Ideal.span {z}
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>this : ¬Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)<GOAL>∃ a b, eval a f + eval b g = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>this : ¬∀ ⦃a : R⦄, (∃ a_1 ∈ univ, eval a_1 f = a) → ¬∃ a_2 ∈ univ, eval a_2 (-g) = a<GOAL>∃ a b, eval a f + eval b g = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this : DecidableEq R := Classical.decEq R<VAR>x a : R<VAR>left✝¹ : a ∈ univ<VAR>ha : eval a f = x<VAR>b : R<VAR>left✝ : b ∈ univ<VAR>hb : eval b (-g) = x<GOAL>∃ a b, eval a f + eval b g = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this : DecidableEq R := Classical.decEq R<VAR>hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)<GOAL>¬Fintype.card R % 2 = f.natDegree * (image (fun x => eval x f) univ).card % 2
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this : DecidableEq R := Classical.decEq R<VAR>hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)<GOAL>0 < (-g).degree
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this : DecidableEq R := Classical.decEq R<VAR>hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)<GOAL>0 < 2
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Fintype R<VAR>f g : R[X]<VAR>hf2 : f.degree = 2<VAR>hg2 : g.degree = 2<VAR>hR : Fintype.card R % 2 = 1<VAR>this : DecidableEq R := Classical.decEq R<VAR>hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)<GOAL>f.natDegree * (image (fun x => eval x f) univ).card + (-g).natDegree * (image (fun x => eval x (-g)) univ).card = 2 * ((image (fun x => eval x f) univ).card + (image (fun x => eval x (-g)) univ).card)
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>a₁ a₂ z : ℂ<VAR>hz : z ≠ 0<GOAL>z ^ a₁ * cexp (↑b₁ * z) = z ^ a₂ * cexp (↑b₁ * z) * z ^ (a₁ - a₂)
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>a₁ a₂ : ℂ<GOAL>(fun z => z ^ a₂ * cexp (↑b₁ * z) * cexp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z => z ^ a₂ * cexp (↑b₂ * z)
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>a₁ a₂ : ℂ<GOAL>(fun z => z ^ a₂ * cexp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * cexp (↑b₂ * z)
<VAR>z : ZFSet<GOAL>congToClass ∅ z ↔ ∅ z
<VAR>z : ZFSet<GOAL>¬{y | ↑y ∈ ∅} z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>y : β<GOAL>y ∈ r.image Set.univ ↔ y ∈ r.codom
<VAR>α : Type u_1<VAR>inst✝ : BEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+ l₂<GOAL>l₁.erase a <+ l₂.erase a
<VAR>α : Type u_1<VAR>inst✝ : BEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+ l₂<GOAL>eraseP (fun x => x == a) l₁ <+ eraseP (fun x => x == a) l₂
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : 2 ≤ n<VAR>hx : 0 < x<GOAL>f ↑n + x * log (↑n - 1) ≤ f (↑n + x)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : 2 ≤ n<VAR>hx : 0 < x<VAR>npos : 0 < ↑n - 1<GOAL>f ↑n + x * log (↑n - 1) ≤ f (↑n + x)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : 2 ≤ n<VAR>hx : 0 < x<VAR>npos : 0 < ↑n - 1<VAR>c : (f ↑n - f (↑n - 1)) / (↑n - (↑n - 1)) ≤ (f (↑n + x) - f ↑n) / (↑n + x - ↑n)<GOAL>f ↑n + x * log (↑n - 1) ≤ f (↑n + x)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : 2 ≤ n<VAR>hx : 0 < x<VAR>npos : 0 < ↑n - 1<VAR>c : f ↑n - f (↑n - 1) ≤ (f (↑n + x) - f ↑n) / x<GOAL>f ↑n + x * log (↑n - 1) ≤ f (↑n + x)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : 2 ≤ n<VAR>hx : 0 < x<VAR>npos : 0 < ↑n - 1<VAR>c : f ↑n - f (↑n - 1) ≤ (f (↑n + x) - f ↑n) / x<VAR>this : f (↑n - 1) = f ↑n - log (↑n - 1)<GOAL>f ↑n + x * log (↑n - 1) ≤ f (↑n + x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module 𝕜 V<VAR>inst✝¹⁵ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹⁴ : AddCommGroup W<VAR>inst✝¹³ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℂ F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℂ G<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : TopologicalRing 𝕜<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : Integrable f μ<GOAL>Continuous (fourierIntegral e μ L f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module 𝕜 V<VAR>inst✝¹⁵ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹⁴ : AddCommGroup W<VAR>inst✝¹³ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℂ F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℂ G<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : TopologicalRing 𝕜<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : Integrable f μ<GOAL>∀ (x : W), AEStronglyMeasurable (fun a => e (-(L a) x) • f a) μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module 𝕜 V<VAR>inst✝¹⁵ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹⁴ : AddCommGroup W<VAR>inst✝¹³ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℂ F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℂ G<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : TopologicalRing 𝕜<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : Integrable f μ<GOAL>∀ (x : W), ∀ᵐ (a : V) ∂μ, ‖e (-(L a) x) • f a‖ ≤ ?bound a
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module 𝕜 V<VAR>inst✝¹⁵ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹⁴ : AddCommGroup W<VAR>inst✝¹³ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℂ F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℂ G<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : TopologicalRing 𝕜<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : Integrable f μ<GOAL>Integrable ?bound μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module 𝕜 V<VAR>inst✝¹⁵ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹⁴ : AddCommGroup W<VAR>inst✝¹³ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℂ F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℂ G<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : TopologicalRing 𝕜<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : Integrable f μ<GOAL>∀ᵐ (a : V) ∂μ, Continuous fun x => e (-(L a) x) • f a
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : CommRing 𝕜<VAR>V : Type u_2<VAR>inst✝¹⁷ : AddCommGroup V<VAR>inst✝¹⁶ : Module 𝕜 V<VAR>inst✝¹⁵ : MeasurableSpace V<VAR>W : Type u_3<VAR>inst✝¹⁴ : AddCommGroup W<VAR>inst✝¹³ : Module 𝕜 W<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℂ F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℂ G<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : TopologicalRing 𝕜<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : TopologicalSpace W<VAR>e : AddChar 𝕜 ↥𝕊<VAR>μ : Measure V<VAR>L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : FirstCountableTopology W<VAR>he : Continuous ⇑e<VAR>hL : Continuous fun p => (L p.1) p.2<VAR>f : V → E<VAR>hf : Integrable f μ<GOAL>V → ℝ
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>(map W f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f (W.negAddY x₁ x₂ y₁ L)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>f L * (f (W.addX x₁ x₂ L) - f x₁) + f y₁ = f (L * (W.addX x₁ x₂ L - x₁) + y₁)
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i j1 j2 : ℕ<VAR>hj : j1 ≤ j2<VAR>cell : (i, j2) ∈ μ<GOAL>T i j1 ≤ T i j2
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i j1 j2 : ℕ<VAR>hj : j1 ≤ j2<VAR>cell : (i, j2) ∈ μ<VAR>h : j1 = j2<GOAL>T i j1 ≤ T i j2
<VAR>μ : YoungDiagram<VAR>T : SemistandardYoungTableau μ<VAR>i j1 j2 : ℕ<VAR>hj : j1 ≤ j2<VAR>cell : (i, j2) ∈ μ<VAR>h : j1 < j2<GOAL>T i j1 ≤ T i j2
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>(nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<VAR>eq : ((G.mapHomologicalComplex c).map (nullHomotopicMap' (hσ' q))).f n = (nullHomotopicMap' fun i j hij => G.map (hσ' q i j hij)).f n<GOAL>(nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<VAR>eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n<GOAL>(nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<VAR>eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n<GOAL>(nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>G : C ⥤ D<VAR>inst✝ : G.Additive<VAR>X : SimplicialObject C<VAR>q n : ℕ<VAR>eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n<VAR>h : ((whiskering C D).obj G ⋙ alternatingFaceMapComplex D).obj X = (alternatingFaceMapComplex C ⋙ G.mapHomologicalComplex (ComplexShape.down ℕ)).obj X := Eq.symm (Functor.congr_obj (map_alternatingFaceMapComplex G) X)<GOAL>(nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>y : α<GOAL>y ∈ EMetric.ball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>y : α<GOAL>ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<GOAL>update i f b = f - single i (f i) + single i b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Ring R₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ ker f<VAR>h' : ker f ≤ p<GOAL>ker (p.liftQ f h) = ⊥
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Z<VAR>x : X<VAR>f : X → Z<VAR>hf : ContinuousWithinAt f s x<VAR>hxe : x ∈ e.source<VAR>ht : t ∈ 𝓝 (f x)<GOAL>↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Z<VAR>x : X<VAR>f : X → Z<VAR>hf : ContinuousWithinAt f s x<VAR>hxe : x ∈ e.source<VAR>ht : t ∈ 𝓝 (f x)<GOAL>∀ᶠ (x : X) in 𝓝 x, ↑e x ∈ ↑e.symm ⁻¹' s ↔ ↑e x ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Z<VAR>x : X<VAR>f : X → Z<VAR>hf : ContinuousWithinAt f s x<VAR>hxe : x ∈ e.source<VAR>ht : t ∈ 𝓝 (f x)<GOAL>∀ a ∈ e.source, (a ∈ s → a ∈ f ⁻¹' t) → (↑e a ∈ ↑e.symm ⁻¹' s ↔ ↑e a ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t))
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Z<VAR>x : X<VAR>f : X → Z<VAR>hf : ContinuousWithinAt f s x<VAR>hxe : x ∈ e.source<VAR>ht : t ∈ 𝓝 (f x)<VAR>y : X<VAR>hy : y ∈ e.source<VAR>hyu : y ∈ s → y ∈ f ⁻¹' t<GOAL>↑e y ∈ ↑e.symm ⁻¹' s ↔ ↑e y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hG : Nat.card G = p ^ 2<GOAL>IsCyclic (G ⧸ center G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hG : Nat.card G = p ^ 2<GOAL>Nat.card (G ⧸ center G) ∣ p
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hG : Nat.card G = p ^ 2<GOAL>p * Nat.card (G ⧸ center G) ∣ Nat.card ↥(center G) * (center G).index
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hG : Nat.card G = p ^ 2<GOAL>p ∣ Nat.card ↥(center G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hG : Nat.card G = p ^ 2<VAR>k : ℕ<VAR>hk0 : k > 0<VAR>hk : Nat.card ↥(center G) = p ^ k<GOAL>p ∣ Nat.card ↥(center G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hG : Nat.card G = p ^ 2<VAR>k : ℕ<VAR>hk0 : k > 0<VAR>hk : Nat.card ↥(center G) = p ^ k<GOAL>p ∣ p ^ k
<VAR>x p : ℝ<VAR>hx_pos : 0 < x<GOAL>↑x.toNNReal ^ p = ↑(x ^ p).toNNReal
<VAR>x p : ℝ<VAR>hx_pos : 0 < x<GOAL>x.toNNReal ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>γ : Type w<VAR>inst✝ : EMetricSpace γ<VAR>s : Set γ<GOAL>0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝ : NormedRing R<VAR>f : ι → ℝ<VAR>g : ι' → ℝ<VAR>hf : Summable f<VAR>hg : Summable g<VAR>hf' : 0 ≤ f<VAR>hg' : 0 ≤ g<GOAL>Summable fun x => ∑' (y : ι'), f (x, y).1 * g (x, y).2
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup A<VAR>s : Set G<VAR>inst✝¹ : Group α<VAR>inst✝ : MulDistribMulAction α G<VAR>a : α<VAR>S T : Subgroup G<GOAL>a • (S ⊓ T) = a • S ⊓ a • T
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>al : ∀ (a : α), count a s ≤ count a t<GOAL>s ≤ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>al : ∀ (a : α), count a s ≤ count a t<GOAL>s ≤ s ∪ t
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>P' : C<VAR>fst' : P' ⟶ X<VAR>snd' : P' ⟶ Y<VAR>h : IsPullback fst snd f g<VAR>h' : IsPullback fst' snd' f g<GOAL>(isoIsPullback X Y h h').inv ≫ fst = fst'