ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>s t : Set α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : MeasurableSMul G α<VAR>fund_dom_s : IsFundamentalDomain G s μ<VAR>fund_dom_t : IsFundamentalDomain G t μ<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>(Measure.map (Quotient.mk α_mod_G) (μ.restrict s)) U = (Measure.map (Quotient.mk α_mod_G) (μ.restrict t)) U
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>s t : Set α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : MeasurableSMul G α<VAR>fund_dom_s : IsFundamentalDomain G s μ<VAR>fund_dom_t : IsFundamentalDomain G t μ<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>μ (Quotient.mk α_mod_G ⁻¹' U ∩ s) = μ (Quotient.mk α_mod_G ⁻¹' U ∩ t)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>s t : Set α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : MeasurableSMul G α<VAR>fund_dom_s : IsFundamentalDomain G s μ<VAR>fund_dom_t : IsFundamentalDomain G t μ<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>MeasurableSet (Quotient.mk α_mod_G ⁻¹' U)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>s t : Set α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : MeasurableSMul G α<VAR>fund_dom_s : IsFundamentalDomain G s μ<VAR>fund_dom_t : IsFundamentalDomain G t μ<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>∀ (g : G), (fun x => g • x) ⁻¹' (Quotient.mk α_mod_G ⁻¹' U) = Quotient.mk α_mod_G ⁻¹' U
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g✝ : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>lTensor P g ∘ₗ rTensor N f = map f g
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝² : TopologicalSpace N<VAR>inst✝¹ : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>p : M × N<GOAL>p ∈ (I.prod J).interior (M × N) ↔ p ∈ I.interior M ×ˢ J.interior N
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝² : TopologicalSpace N<VAR>inst✝¹ : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>p : M × N<VAR>aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))<GOAL>p ∈ (I.prod J).interior (M × N) ↔ p ∈ I.interior M ×ˢ J.interior 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₄ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hne : p₂ ≠ p₃<GOAL>(∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>s : ι → Set α<VAR>hic : #ι < c<GOAL>⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>s : ι → Set α<VAR>hic : #ι < c<GOAL>⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>s : ι → Set α<VAR>hic : #ι < c<GOAL>(∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<VAR>c : ℕ := Fintype.card α<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<VAR>c : ℕ := Fintype.card α<VAR>hc0 : 0 < c<GOAL>(filter (fun a => orderOf a = d) univ).card = φ d
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<VAR>c : ℕ := Fintype.card α<VAR>hc0 : 0 < c<GOAL>0 < (filter (fun a => orderOf a = d) univ).card
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<VAR>c : ℕ := Fintype.card α<VAR>hc0 : 0 < c<VAR>h0 : ¬0 < (filter (fun a => orderOf a = d) univ).card<GOAL>False
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<VAR>c : ℕ := Fintype.card α<VAR>hc0 : 0 < c<VAR>h0 : filter (fun a => orderOf a = d) univ = ∅<GOAL>False
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>d : ℕ<VAR>hd : d ∣ Fintype.card α<VAR>c : ℕ := Fintype.card α<VAR>hc0 : 0 < c<VAR>h0 : filter (fun a => orderOf a = d) univ = ∅<GOAL>c < c
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>hi : i ∈ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>(s.pi fun j => t j (update f i a j)) = ({i} ∪ s \ {i}).pi fun j => t j (update f i a j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>hi : i ∈ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>(({i} ∪ s \ {i}).pi fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ {i}).pi fun j => t j (f j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>hi : i ∈ s<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>i ∉ s \ {i}
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B'✝ X✝ Y✝ Y' : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i'✝ : B✝ ⟶ B'✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>p' : Y✝ ⟶ Y'<VAR>A B A' B' X Y : C<VAR>i : A ⟶ B<VAR>i' : A' ⟶ B'<VAR>e : Arrow.mk i ≅ Arrow.mk i'<VAR>p : X ⟶ Y<VAR>a✝ : HasLiftingProperty i p<GOAL>HasLiftingProperty i' p
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B'✝ X✝ Y✝ Y' : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i'✝ : B✝ ⟶ B'✝<VAR>p✝ : X✝ ⟶ Y✝<VAR>p' : Y✝ ⟶ Y'<VAR>A B A' B' X Y : C<VAR>i : A ⟶ B<VAR>i' : A' ⟶ B'<VAR>e : Arrow.mk i ≅ Arrow.mk i'<VAR>p : X ⟶ Y<VAR>a✝ : HasLiftingProperty i' p<GOAL>HasLiftingProperty i p
<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>s : Set P<VAR>hs : Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<GOAL>AffineIndependent ℝ p
<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>s : Set P<VAR>hs : Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<GOAL>¬Collinear ℝ (Set.range p)
<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>s : Set P<VAR>hs : Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>hc : Collinear ℝ (Set.range p)<GOAL>False
<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>s : Set P<VAR>hs : Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>hc : ∃ v, ∀ p_1 ∈ Set.range p, ∃ r, p_1 = r • v +ᵥ p 0<GOAL>False
<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>s : Set P<VAR>hs : Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv : ∀ p_1 ∈ Set.range p, ∃ r, p_1 = r • v +ᵥ p 0<GOAL>False
<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>s : Set P<VAR>hs : Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv : ∀ (i : Fin 3), ∃ r, p i = r • v +ᵥ p 0<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv : ∀ (i : Fin 3), ∃ r, p i = r • v +ᵥ p 0<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv : ∀ (i : Fin 3), ∃ r, p i = r • v +ᵥ p 0<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<VAR>hs' : ∀ (i : Fin 3), dist (p i) c = r<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<VAR>hs' : ∀ (i : Fin 3), dist (p i) c = r<VAR>f : Fin 3 → ℝ<VAR>hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0<VAR>hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<VAR>hs' : ∀ (i : Fin 3), dist (p i) c = r<VAR>f : Fin 3 → ℝ<VAR>hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0<VAR>hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r<VAR>hf0 : f 0 = 0<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<VAR>hs' : ∀ (i : Fin 3), dist (p i) c = r<VAR>f : Fin 3 → ℝ<VAR>hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0<VAR>hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r<VAR>hf0 : f 0 = 0<VAR>hfi : Function.Injective f<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<VAR>hs' : ∀ (i : Fin 3), dist (p i) c = r<VAR>f : Fin 3 → ℝ<VAR>hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0<VAR>hf0 : f 0 = 0<VAR>hfi : Function.Injective f<VAR>hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫_ℝ / ⟪v, v⟫_ℝ<GOAL>False
<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>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>v : V<VAR>hv0 : v ≠ 0<VAR>c : P<VAR>r : ℝ<VAR>hs : ∀ p ∈ s, dist p c = r<VAR>hs' : ∀ (i : Fin 3), dist (p i) c = r<VAR>f : Fin 3 → ℝ<VAR>hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0<VAR>hf0 : f 0 = 0<VAR>hfi : Function.Injective f<VAR>hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫_ℝ / ⟪v, v⟫_ℝ<VAR>hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0<GOAL>False
<VAR>α β : HeytAlg<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget HeytAlg).obj α<GOAL>({ toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : HeytAlg<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget HeytAlg).obj β<GOAL>({ toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<GOAL>∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂Measure.map f μ
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<VAR>n✝ m n : ℕ+<GOAL>PNat.find h ≤ n ↔ ∃ m ≤ n, p m
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<GOAL>μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<GOAL>μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<GOAL>μ.normalize.toFiniteMeasure = (μ.mass⁻¹ • μ.mass) • μ.normalize.toFiniteMeasure
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>IsLindelof s ↔ IsLindelof univ
<VAR>a b : ℤ<GOAL>Fintype.card ↑(Set.Ioc a b) = (b - a).toNat
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = ((ρ.IicSnd ↑r) s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>(∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = ((ρ.IicSnd ↑r) s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ⊤
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>W'.negAddY P Q = (-(Q x * P z)) ^ 3 * W'.negY P
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>a b c : R<VAR>inst✝¹ : NeZero 2<VAR>inst✝ : NoZeroDivisors R<VAR>ha : a ≠ 0<VAR>x : R<GOAL>a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>a b c : R<VAR>inst✝¹ : NeZero 2<VAR>inst✝ : NoZeroDivisors R<VAR>ha : a ≠ 0<VAR>x : R<VAR>h : discrim a b c = (2 * a * x + b) ^ 2<GOAL>a * x * x + b * x + c = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>a b c : R<VAR>inst✝¹ : NeZero 2<VAR>inst✝ : NoZeroDivisors R<VAR>ha : a ≠ 0<VAR>x : R<VAR>h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2<GOAL>a * x * x + b * x + c = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>a b c : R<VAR>inst✝¹ : NeZero 2<VAR>inst✝ : NoZeroDivisors R<VAR>ha✝ : a ≠ 0<VAR>x : R<VAR>h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2<VAR>ha : 2 * 2 * a ≠ 0<GOAL>a * x * x + b * x + c = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>a b c : R<VAR>inst✝¹ : NeZero 2<VAR>inst✝ : NoZeroDivisors R<VAR>ha✝ : a ≠ 0<VAR>x : R<VAR>h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2<VAR>ha : 2 * 2 * a ≠ 0<GOAL>2 * 2 * a * (a * x * x + b * x + c) = 2 * 2 * a * 0
<VAR>C : Type w<VAR>inst✝ : Category.{v, w} C<VAR>X Y : Condensed C<VAR>f g : X ⟶ Y<VAR>h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S<GOAL>f = g
<VAR>C : Type w<VAR>inst✝ : Category.{v, w} C<VAR>X Y : Condensed C<VAR>f g : X ⟶ Y<VAR>h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S<GOAL>f.val = g.val
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx✝ : 0 ≤ x<VAR>hx : 0 < x<GOAL>logb b x ≤ 0 ↔ x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>t₁ t₂ : TopologicalSpace α<VAR>inst✝¹ : Topology.IsLowerSet α<VAR>inst✝ : IsLower α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsOpen s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>t₁ t₂ : TopologicalSpace α<VAR>inst✝¹ : Topology.IsLowerSet α<VAR>inst✝ : IsLower α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsLowerSet s
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>h : H<VAR>w : NormalWord d<GOAL>(lift (fun i => MulAction.toEndHom) MulAction.toEndHom ⋯) ((base φ) h) w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>h : H<VAR>w : NormalWord d<GOAL>MulAction.toEndHom h w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝¹ : Functor t<VAR>inst✝ : LawfulFunctor t<VAR>α : Type u<VAR>x : t' α<GOAL>Equiv.map eqv id x = x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : MeasurableSpace M<VAR>inst✝⁵ : MeasurableSpace N<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : SMul M α<VAR>inst✝¹ : SMulInvariantMeasure M α μ<VAR>inst✝ : MeasurableSMul M α<VAR>c : Mᵈᵐᵃ<VAR>f g : ↥(Lp E p μ)<GOAL>dist (c • f) (c • g) = dist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>i : α<GOAL>update 0 a b = single a b
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K : ℕ<VAR>Y : ℕ → Ω → ℝ := fun n => truncation X ↑n<VAR>ρ : Measure ℝ := Measure.map X ℙ<GOAL>∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K : ℕ<VAR>Y : ℕ → Ω → ℝ := fun n => truncation X ↑n<VAR>ρ : Measure ℝ := Measure.map X ℙ<VAR>Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0 ..↑n, x ^ 2 ∂ρ<GOAL>∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>t : Finset β<GOAL>interedges r ∅ t = ∅
<VAR>x : ℝ<GOAL>Real.toEReal '' Iio x = Ioo ⊥ ↑x
<VAR>x : ℝ<GOAL>WithBot.some '' (WithTop.some '' Iio x) = Ioo ⊥ ↑x
<VAR>x : ℝ<GOAL>Ioo ⊥ ↑↑x = Ioo ⊥ ↑x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁴ : Category.{u_4, u_1} C<VAR>inst✝¹³ : HasZeroObject C<VAR>inst✝¹² : HasShift C ℤ<VAR>inst✝¹¹ : Preadditive C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : Category.{?u.5817, u_2} D<VAR>inst✝⁷ : HasZeroObject D<VAR>inst✝⁶ : HasShift D ℤ<VAR>inst✝⁵ : Preadditive D<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : Pretriangulated D<VAR>inst✝² : Category.{u_5, u_3} A<VAR>inst✝¹ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>hF : ∀ (T : Triangle C) (hT : T ∈ distinguishedTriangles), ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>T' : Triangle C<VAR>e : T ≅ T'<VAR>h' : ((shortComplexOfDistTriangle T' ⋯).map F).Exact<GOAL>((shortComplexOfDistTriangle T hT).map F).Exact
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u✝ v : 𝕜 → 𝕜'<VAR>u : 𝕜'<GOAL>deriv (fun y => u * v y) x = u * deriv v x
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<GOAL>closure (range fun x => x ^ n) = ⊤
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>x : ℚ≥0<GOAL>x ∈ closure (range fun x => x ^ n)
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>x : ℚ≥0<GOAL>x = (x.num * x.den ^ (n - 1)) • (↑x.den)⁻¹ ^ n
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>x : ℚ≥0<GOAL>x = ↑(x.num * x.den ^ (n - 1)) * (↑x.den)⁻¹ ^ n
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>x : ℚ≥0<GOAL>x = ↑x.num * ↑x.den ^ (n - 1) * (↑x.den)⁻¹ ^ n
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>x : ℚ≥0<GOAL>↑x.den ≠ 0
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>x : ℚ≥0<GOAL>1 ≤ n