ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>C : ℝ<VAR>hC : ∀ (i : G), ‖g i‖ ≤ C<VAR>x t : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<GOAL>‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * C) t
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝¹ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>C : ℝ<VAR>hC : ∀ (i : G), ‖g i‖ ≤ C<VAR>x t✝ : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<VAR>t : G<VAR>x✝ : t ∈ u<GOAL>(fun t => ‖(L (f t)) (g (x - t))‖) t ≤ ‖L‖ * ‖f t‖ * C
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>C : ℝ<VAR>hC : ∀ (i : G), ‖g i‖ ≤ C<VAR>x t✝ : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<VAR>t : G<VAR>ht : t ∉ u<GOAL>(fun t => ‖(L (f t)) (g (x - t))‖) t ≤ 0
<VAR>m n : ℤ<VAR>k : ℕ<VAR>k0 : k ≠ 0<GOAL>m ^ k ∣ n ^ k ↔ m ∣ n
<VAR>m n : ℤ<VAR>k : ℕ<VAR>k0 : k ≠ 0<VAR>h : m ^ k ∣ n ^ k<GOAL>m ∣ n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ p₃ p₂ p₁ = ↑π
<VAR>f : ℝ → ℝ<GOAL>∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x
<VAR>f : ℝ → ℝ<VAR>eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x<GOAL>∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>inst✝ : H.FiniteIndex<GOAL>∃ n, H.index = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>inst✝ : H.FiniteIndex<VAR>n : ℕ<VAR>hn : Nat.card (G ⧸ H.normalCore) = p ^ n<GOAL>∃ n, H.index = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>inst✝ : H.FiniteIndex<VAR>n : ℕ<VAR>hn : Nat.card (G ⧸ H.normalCore) = p ^ n<VAR>k : ℕ<VAR>left✝ : k ≤ n<VAR>hk2 : H.index = p ^ k<GOAL>∃ n, H.index = p ^ n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ = pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>(p * X ^ n).natDegree = p.natDegree + n
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ<VAR>b : ℝ≥0<GOAL>ENNReal.ofReal a ≤ ↑b ↔ a ≤ (↑b).toReal
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsBounded s ↔ Bornology.IsBounded s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : Semiring R<VAR>s : Set R<GOAL>closure s ^ 0 = closure (s ^ 0)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : Semiring R<VAR>s : Set R<VAR>n : ℕ<GOAL>closure s ^ (n + 1) = closure (s ^ (n + 1))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<VAR>x : α<VAR>x✝ : x ∈ s<GOAL>∃ u ∈ 𝓝[s] x, μ u = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<VAR>x : α<VAR>x✝ : x ∈ s<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : μ o < ⊤<GOAL>∃ u ∈ 𝓝[s] x, μ u = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<VAR>x : α<VAR>x✝ : x ∈ s<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : μ o < ⊤<GOAL>μ (s ∩ o) = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<VAR>x : α<VAR>x✝ : x ∈ s<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : μ o < ⊤<VAR>s' : Set α := s ∩ o<GOAL>μ (s ∩ o) = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<VAR>x : α<VAR>x✝ : x ∈ s<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : μ o < ⊤<VAR>s' : Set α := s ∩ o<VAR>h : ¬μ (s ∩ o) = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>c d : ℝ≥0<VAR>hcd : c < d<VAR>s : Set α<VAR>hc : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a<VAR>hd : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a<VAR>x : α<VAR>x✝ : x ∈ s<VAR>o : Set α<VAR>xo : x ∈ o<VAR>o_open : IsOpen o<VAR>μo : μ o < ⊤<VAR>s' : Set α := s ∩ o<VAR>h : ¬μ (s ∩ o) = 0<GOAL>ρ s' < ρ s'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₗ[R] M<VAR>n m : ℕ<VAR>w : n ≤ m<VAR>x : M<VAR>h : x ∈ (fun n => ker (f ^ n)) n<GOAL>x ∈ (fun n => ker (f ^ n)) m
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>x : M<VAR>h : x ∈ (fun n => ker (f ^ n)) n<VAR>c : ℕ<VAR>w : n ≤ n + c<GOAL>x ∈ (fun n => ker (f ^ n)) (n + c)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>x : M<VAR>h : (f ^ n) x = 0<VAR>c : ℕ<VAR>w : n ≤ n + c<GOAL>x ∈ (fun n => ker (f ^ n)) (n + c)
<VAR>v : PrimeMultiset<GOAL>v.prod.factorMultiset = v
<VAR>v : PrimeMultiset<GOAL>Coe.coe v.prod.factorMultiset = Coe.coe v
<VAR>v : PrimeMultiset<GOAL>v.prod.factorMultiset.toNatMultiset = v.toNatMultiset
<VAR>v : PrimeMultiset<GOAL>↑v.toNatMultiset.prod.primeFactorsList = v.toNatMultiset
<VAR>v : PrimeMultiset<VAR>l : List Nat.Primes<GOAL>↑(↑(List.map Coe.coe l)).prod.primeFactorsList = ↑(List.map Coe.coe l)
<VAR>v : PrimeMultiset<VAR>l : List Nat.Primes<GOAL>↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)
<VAR>v : PrimeMultiset<VAR>l : List Nat.Primes<VAR>l' : List ℕ := List.map Coe.coe l<GOAL>↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)
<VAR>v : PrimeMultiset<VAR>l : List Nat.Primes<VAR>l' : List ℕ := List.map Coe.coe l<VAR>this : ∀ p ∈ l', Nat.Prime p<GOAL>↑(List.map Coe.coe l).prod.primeFactorsList = ↑(List.map Coe.coe l)
<VAR>n✝ : ℕ<VAR>i✝ : Fin (n✝ + 1).succ<VAR>i : Fin (n✝ + 1)<GOAL>↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)
<VAR>n✝ : ℕ<VAR>i✝ : Fin (n✝ + 1).succ<VAR>i : Fin (n✝ + 1)<GOAL>(if i = Fin.last n✝ then 0 else ↑i.succ + 1) = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)
<VAR>m : Type u_1 → Type u_2<VAR>α ρ : Type u_1<VAR>p : α → Prop<VAR>x : StateT ρ m α<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<GOAL>SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
<VAR>m : Type u_1 → Type u_2<VAR>α ρ : Type u_1<VAR>p : α → Prop<VAR>x : StateT ρ m α<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>x✝ : SatisfiesM p x<VAR>f : StateT ρ m { a // p a }<VAR>eq : Subtype.val <$> f = x<GOAL>∃ f_1, ∀ (x : ρ), Subtype.val <$> f_1 x = (Subtype.val <$> f) x
<VAR>m : Type u_1 → Type u_2<VAR>α ρ : Type u_1<VAR>p : α → Prop<VAR>x : StateT ρ m α<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>x✝ : ∃ f, ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1<VAR>f : ρ → m { a // (fun x => p x.fst) a }<VAR>h : ∀ (x_1 : ρ), Subtype.val <$> f x_1 = x x_1<GOAL>SatisfiesM p x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x : Z<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>p : F<GOAL>↑e.symm (b, p) ∈ proj ⁻¹' {b}
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>φ : L[[α]].Sentence<GOAL>((equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ M ⊨ φ
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>φ : L[[α]].Sentence<GOAL>(BoundedFormula.constantsVarsEquiv φ).Realize (fun x => ↑(L.con ((Equiv.sumEmpty α Empty) x))) default ↔ M ⊨ φ
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>φ : L[[α]].Sentence<GOAL>(BoundedFormula.constantsVarsEquiv φ).Realize (fun x => ↑(L.con ((Equiv.sumEmpty α Empty) x))) default ↔ (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) default) default
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>inst✝¹ : L[[α]].Structure M<VAR>inst✝ : (L.lhomWithConstants α).IsExpansionOn M<VAR>φ : L[[α]].Sentence<GOAL>(BoundedFormula.constantsVarsEquiv φ).Realize (fun x => ↑(L.con ((Equiv.sumEmpty α Empty) x))) default = (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) default) default
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<GOAL>‖q * r‖ = ‖q‖ * ‖r‖
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>f : P →ᵃ[𝕜] P₂<VAR>inhabited_h : Inhabited P<VAR>this : ⇑f.linear = ⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘ ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph<GOAL>IsOpenMap (⇑(AffineIsometryEquiv.vaddConst 𝕜 (f default)).toHomeomorph.symm ∘ ⇑f ∘ ⇑(AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph) ↔ IsOpenMap ⇑f
<VAR>x : EReal<GOAL>x.exp = 0 ↔ x = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>b c : Ordinal.{u_4}<GOAL>b * c % b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Ordinal.{u_4}<GOAL>0 * c % 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>b c : Ordinal.{u_4}<VAR>hb : b ≠ 0<GOAL>b * c % b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>h : s.Subsingleton<GOAL>maximals r s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>t : Set α<VAR>a b x : α<VAR>h : ∅.Subsingleton<GOAL>maximals r ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>t : Set α<VAR>a b x✝ x : α<VAR>h : {x}.Subsingleton<GOAL>maximals r {x} = {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<GOAL>ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) {a | (a, b) ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<GOAL>(∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x => f (x, b)) {a | (a, b) ∈ s} a) ↔ ∀ (b : β), ∀ x ∈ {a | (a, b) ∈ s}, ContinuousWithinAt (fun x => f (x, b)) {a | (a, b) ∈ s} x
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommSemiring R✝<VAR>S✝ : Type v<VAR>inst✝⁴ : Semiring S✝<VAR>inst✝³ : Algebra R✝ S✝<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p : S[X]<GOAL>p ∈ lifts (algebraMap R S) ↔ p ∈ (mapAlg R S).range
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>a x✝ z x : ℂ<GOAL>Real.sin (if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then Real.arcsin ((-x).im / abs x) + π else Real.arcsin ((-x).im / abs x) - π) = x.im / abs x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>hE : CompleteSpace E<VAR>hg : Integrable g (μ.withDensity fun x => ↑(f x))<GOAL>(∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>hE : CompleteSpace E<VAR>hg : Integrable g (μ.withDensity fun x => ↑(f x))<GOAL>∀ (c : E) ⦃s : Set X⦄, MeasurableSet s → (μ.withDensity fun x => ↑(f x)) s < ⊤ → (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) (s.indicator fun x => c)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>hE : CompleteSpace E<VAR>hg : Integrable g (μ.withDensity fun x => ↑(f x))<GOAL>∀ ⦃f_1 g : X → E⦄, Disjoint (support f_1) (support g) → Integrable f_1 (μ.withDensity fun x => ↑(f x)) → Integrable g (μ.withDensity fun x => ↑(f x)) → (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) f_1 → (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) g → (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) (f_1 + g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>hE : CompleteSpace E<VAR>hg : Integrable g (μ.withDensity fun x => ↑(f x))<GOAL>IsClosed {f_1 | (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) ↑↑f_1}