ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s i)).toReal) =ᶠ[li] m) _auto✝<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<VAR>this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε<GOAL>∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - (μ x).toReal • b‖ ≤ ε * ‖(μ x).toReal‖
<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>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s i)).toReal) =ᶠ[li] m) _auto✝<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<VAR>this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε<GOAL>∀ (a : Set X), μ a < ⊤ → IntegrableOn f a μ → AEStronglyMeasurable f (μ.restrict a) → (∀ᵐ (x : X) ∂μ, x ∈ a → f x ∈ closedBall b ε) → ‖∫ (x : X) in a, f x ∂μ - (μ a).toReal • b‖ ≤ ε * ‖(μ a).toReal‖
<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>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s i)).toReal) =ᶠ[li] m) _auto✝<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<VAR>this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε<GOAL>∀ (a : Set X), μ a < ⊤ → IntegrableOn f a μ → AEStronglyMeasurable f (μ.restrict a) → (∀ᵐ (x : X) ∂μ, x ∈ a → ‖f x - b‖ ≤ ε) → ‖∫ (x : X) in a, f x ∂μ - (μ a).toReal • b‖ ≤ ε * ‖(μ a).toReal‖
<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>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm✝ : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s✝ : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s✝ li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s✝ i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s✝ i)).toReal) =ᶠ[li] m) _auto✝<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<VAR>this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε<VAR>s : Set X<VAR>hμs : μ s < ⊤<VAR>h_integrable : IntegrableOn f s μ<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε<GOAL>‖∫ (x : X) in s, f x ∂μ - (μ s).toReal • b‖ ≤ ε * ‖(μ s).toReal‖
<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>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm✝ : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s✝ : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s✝ li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s✝ i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s✝ i)).toReal) =ᶠ[li] m) _auto✝<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<VAR>this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε<VAR>s : Set X<VAR>hμs : μ s < ⊤<VAR>h_integrable : IntegrableOn f s μ<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε<GOAL>‖∫ (a : X) in s, f a - b ∂μ‖ ≤ ε * (μ s).toReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.reverse.sublists' = map reverse l.sublists
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : ∀ (p : ℕ), ↑p = 0 → p = 0<VAR>x : ℕ<GOAL>↑x = 0 ↔ 0 ∣ x
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : ∀ (p : ℕ), ↑p = 0 → p = 0<VAR>x : ℕ<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : ¬∀ (p : ℕ), ↑p = 0 → p = 0<VAR>x : ℕ<VAR>H1 : ↑x = 0<VAR>H2 : ¬x % Nat.find ⋯ = 0<GOAL>↑(x % Nat.find ⋯) = 0
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : ¬∀ (p : ℕ), ↑p = 0 → p = 0<VAR>x : ℕ<VAR>H1 : Nat.find ⋯ ∣ x<GOAL>↑x = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r✝ : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>r : β → β → Prop<VAR>inst✝ : IsTrans β r<VAR>f : ℕ → β<VAR>a : ℕ<VAR>h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))<VAR>b c : ℕ<VAR>hab : a ≤ b<GOAL>r (f b) (f b.succ)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r✝ : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>r : β → β → Prop<VAR>inst✝ : IsTrans β r<VAR>f : ℕ → β<VAR>a : ℕ<VAR>h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))<VAR>b c : ℕ<VAR>hab : a ≤ b<VAR>k : ℕ<VAR>b_lt_k : b.succ.le k<VAR>r_b_k : r (f b) (f k)<GOAL>r (f b) (f k.succ)
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderClosedTopology α<VAR>inst✝ : PreconnectedSpace X<VAR>a b : X<VAR>f g : X → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>ha : f a ≤ g a<VAR>hb : g b ≤ f b<GOAL>∃ x, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderClosedTopology α<VAR>inst✝ : PreconnectedSpace X<VAR>a b : X<VAR>f g : X → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>ha : f a ≤ g a<VAR>hb : g b ≤ f b<VAR>x : X<VAR>left✝ : x ∈ univ<VAR>hfg : f x ≤ g x<VAR>hgf : g x ≤ f x<GOAL>∃ x, f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝¹ : Zero α<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsDiag<VAR>i j : n<GOAL>diagonal A.diag i j = A i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝¹ : Zero α<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsDiag<VAR>i : n<GOAL>diagonal A.diag i i = A i i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝¹ : Zero α<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<VAR>h : A.IsDiag<VAR>i j : n<VAR>hij : i ≠ j<GOAL>diagonal A.diag i j = A i j
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>E : Set α<VAR>δ δ' : ℝ<VAR>hδ₀ : 0 < δ'<VAR>hδδ' : δ < δ'<GOAL>cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>E : Set α<VAR>δ δ' : ℝ<VAR>hδ₀ : 0 < δ'<VAR>hδδ' : δ < δ'<VAR>x : α<VAR>hx : x ∈ thickening δ' E<GOAL>x ∈ ⋃ x ∈ E, closedBall x δ'
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>E : Set α<VAR>δ δ' : ℝ<VAR>hδ₀ : 0 < δ'<VAR>hδδ' : δ < δ'<VAR>x : α<VAR>hx : x ∈ thickening δ' E<VAR>y : α<VAR>hy₁ : y ∈ E<VAR>hy₂ : dist x y < δ'<GOAL>x ∈ ⋃ x ∈ E, closedBall x δ'
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<GOAL>StrictConvexOn ℝ (Ioi 0) fun x => x ^ m
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<GOAL>ContinuousOn (fun x => x ^ m) (Ioi 0)
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<GOAL>∀ x ∈ Ioi 0, 0 < deriv^[2] (fun x => x ^ m) x
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>0 < deriv^[2] (fun x => x ^ m) x
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < deriv^[2] (fun x => x ^ m) x
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < (∏ i ∈ Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < ∏ i ∈ Finset.range 2, (↑m - ↑i)
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < ∏ i ∈ Finset.range 2, (m - ↑i)
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hm : m ∈ Ico 0 ↑2<GOAL>False
<VAR>m : ℤ<VAR>hm₀ : m ≠ 0<VAR>hm₁ : m ≠ 1<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hm : m ∈ ↑(Finset.Ico 0 ↑2)<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>x✝² y z : α<VAR>ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ : Set α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : α → β<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>ε : ℝ≥0∞<VAR>x✝¹ : 0 < ε<VAR>δ : ℝ≥0∞<VAR>x✝ : 0 < δ<VAR>x : α<GOAL>edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>l : List α<GOAL>𝓝 (a :: l) = Seq.seq (List.cons <$> 𝓝 a) fun x => 𝓝 l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<GOAL>∃ x₀, ∀ (x : α), f x₀ ≤ f x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>val✝ : Fintype α<GOAL>∃ x₀, ∀ (x : α), f x₀ ≤ f x
<VAR>P : MorphismProperty Scheme<VAR>inst✝² : IsLocalAtSource P<VAR>X✝ Y✝ U V : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g : U ⟶ Y✝<VAR>inst✝¹ : IsOpenImmersion g<VAR>𝒰✝ : X✝.OpenCover<VAR>inst✝ : P.IsMultiplicative<VAR>hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<GOAL>P f ↔ ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)
<VAR>P : MorphismProperty Scheme<VAR>inst✝² : IsLocalAtSource P<VAR>X✝ Y✝ U V : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g : U ⟶ Y✝<VAR>inst✝¹ : IsOpenImmersion g<VAR>𝒰✝ : X✝.OpenCover<VAR>inst✝ : P.IsMultiplicative<VAR>hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.pullbackCover f).J<GOAL>P ((𝒰.pullbackCover f).map i ≫ f) ↔ P (𝒰.pullbackHom f i)
<VAR>P : MorphismProperty Scheme<VAR>inst✝² : IsLocalAtSource P<VAR>X✝ Y✝ U V : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g : U ⟶ Y✝<VAR>inst✝¹ : IsOpenImmersion g<VAR>𝒰✝ : X✝.OpenCover<VAR>inst✝ : P.IsMultiplicative<VAR>hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : IsOpenImmersion g], P (f ≫ g) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.pullbackCover f).J<GOAL>P (𝒰.pullbackHom f i ≫ 𝒰.map i) ↔ P (𝒰.pullbackHom f i)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>motive : (m : ℕ) → m ≤ k → Sort u_1<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<VAR>of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯<VAR>self : motive k ⋯<GOAL>decreasingInduction of_succ self ⋯ = decreasingInduction (fun n_1 ih => of_succ n_1 ⋯) (decreasingInduction of_succ self hnk) hmn
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : ¬a = 0<VAR>x : α<VAR>hx : x ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)<GOAL>Prime x
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : ¬a = 0<VAR>y : α<VAR>hy : y ∈ Classical.choose ⋯<VAR>hx : normalize y ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)<GOAL>Prime (normalize y)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : ¬a = 0<VAR>y : α<VAR>hy : y ∈ Classical.choose ⋯<VAR>hx : normalize y ∈ Multiset.map (fun x => normalize x) (Classical.choose ⋯)<GOAL>Prime y
<VAR>q : ℚ<VAR>a b : ℤ<VAR>b0 : b ≠ 0<GOAL>a /. b = 0 ↔ a = 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>A B : PointedGaloisObject F<VAR>f : A ⟶ B<VAR>φ : Aut B.obj<GOAL>∃ a, ((autGaloisSystem F).map f) a = φ
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>A B : PointedGaloisObject F<VAR>f : A ⟶ B<VAR>φ : Aut B.obj<VAR>ψ : Aut A.obj<VAR>hψ : autMap f.val ψ = φ<GOAL>∃ a, ((autGaloisSystem F).map f) a = φ
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>A B : PointedGaloisObject F<VAR>f : A ⟶ B<VAR>φ : Aut B.obj<VAR>ψ : Aut A.obj<VAR>hψ : autMap f.val ψ = φ<GOAL>((autGaloisSystem F).map f) ψ = φ
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>A B : PointedGaloisObject F<VAR>f : A ⟶ B<VAR>φ : Aut B.obj<VAR>ψ : Aut A.obj<VAR>hψ : autMap f.val ψ = φ<GOAL>(autMapHom f.val) ψ = φ
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<GOAL>(π.map f).map p ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧ ⟦H.evalAt x₀⟧ ≫ (π.map g).map p = H.diagonalPath' p
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<GOAL>(hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫ ⟦H.evalAt x₁⟧ = H.diagonalPath' p ∧ (hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫ hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ = H.diagonalPath' p
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<GOAL>(hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫ hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast ⋯ = H.diagonalPath' p ∧ (hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫ hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ = H.diagonalPath' p
<VAR>α : Type u<VAR>i s1 e2 e1 s2 : Nat<VAR>a : Array α<VAR>h : s1 + e2 ≤ e1<GOAL>(a.extract s1 e1).extract s2 e2 = a.extract (s1 + s2) (s1 + e2)
<VAR>α : Type u<VAR>i s1 e2 e1 s2 : Nat<VAR>a : Array α<VAR>h : s1 + e2 ≤ e1<GOAL>((a.extract s1 e1).extract s2 e2).size = (a.extract (s1 + s2) (s1 + e2)).size
<VAR>α : Type u<VAR>i s1 e2 e1 s2 : Nat<VAR>a : Array α<VAR>h : s1 + e2 ≤ e1<GOAL>∀ (i : Nat) (hi₁ : i < ((a.extract s1 e1).extract s2 e2).size) (hi₂ : i < (a.extract (s1 + s2) (s1 + e2)).size), ((a.extract s1 e1).extract s2 e2)[i] = (a.extract (s1 + s2) (s1 + e2))[i]
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p : ℕ<VAR>hp0 : 0 < f ↑p<VAR>hp1 : f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>∃! p, ∃ (hp : Fact (Nat.Prime p)), f.equiv (mulRingNorm_padic p)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p✝ : ℕ<VAR>hp0 : 0 < f ↑p✝<VAR>hp1 : f ↑p✝ < 1<VAR>hmin✝ : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p✝ ≤ m<VAR>p : ℕ<VAR>hfp : 0 < f ↑p ∧ f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<GOAL>∃! p, ∃ (hp : Fact (Nat.Prime p)), f.equiv (mulRingNorm_padic p)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p✝ : ℕ<VAR>hp0 : 0 < f ↑p✝<VAR>hp1 : f ↑p✝ < 1<VAR>hmin✝ : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p✝ ≤ m<VAR>p : ℕ<VAR>hfp : 0 < f ↑p ∧ f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>hprime : Nat.Prime p<GOAL>∃! p, ∃ (hp : Fact (Nat.Prime p)), f.equiv (mulRingNorm_padic p)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p✝ : ℕ<VAR>hp0 : 0 < f ↑p✝<VAR>hp1 : f ↑p✝ < 1<VAR>hmin✝ : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p✝ ≤ m<VAR>p : ℕ<VAR>hfp : 0 < f ↑p ∧ f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>hprime : Nat.Prime p<VAR>hprime_fact : Fact (Nat.Prime p)<GOAL>∃! p, ∃ (hp : Fact (Nat.Prime p)), f.equiv (mulRingNorm_padic p)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p✝ : ℕ<VAR>hp0 : 0 < f ↑p✝<VAR>hp1 : f ↑p✝ < 1<VAR>hmin✝ : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p✝ ≤ m<VAR>p : ℕ<VAR>hfp : 0 < f ↑p ∧ f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>hprime : Nat.Prime p<VAR>hprime_fact : Fact (Nat.Prime p)<VAR>t : ℝ<VAR>h : 0 < t ∧ f ↑p = ↑p ^ (-t)<GOAL>∃! p, ∃ (hp : Fact (Nat.Prime p)), f.equiv (mulRingNorm_padic p)
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p✝ : ℕ<VAR>hp0 : 0 < f ↑p✝<VAR>hp1 : f ↑p✝ < 1<VAR>hmin✝ : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p✝ ≤ m<VAR>p : ℕ<VAR>hfp : 0 < f ↑p ∧ f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>hprime : Nat.Prime p<VAR>hprime_fact : Fact (Nat.Prime p)<VAR>t : ℝ<VAR>h : 0 < t ∧ f ↑p = ↑p ^ (-t)<GOAL>∃! p, ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (mulRingNorm_padic p) ↑n
<VAR>f g : MulRingNorm ℚ<VAR>hf_nontriv : f ≠ 1<VAR>bdd : ∀ (n : ℕ), f ↑n ≤ 1<VAR>p✝ : ℕ<VAR>hp0 : 0 < f ↑p✝<VAR>hp1 : f ↑p✝ < 1<VAR>hmin✝ : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p✝ ≤ m<VAR>p : ℕ<VAR>hfp : 0 < f ↑p ∧ f ↑p < 1<VAR>hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m<VAR>hprime : Nat.Prime p<VAR>hprime_fact : Fact (Nat.Prime p)<VAR>t : ℝ<VAR>h : 0 < t ∧ f ↑p = ↑p ^ (-t)<GOAL>(fun p => ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (mulRingNorm_padic p) ↑n) p ∧ ∀ (y : ℕ), (fun p => ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (mulRingNorm_padic p) ↑n) y → y = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x : α<VAR>hx : ↑(f.restrict s) x ≠ 0<VAR>hxs : x ∈ s<VAR>x✝ : μ (↑(f.restrict s) ⁻¹' {↑(f.restrict s) x}) ≠ 0<GOAL>↑(f.restrict s) x ∈ f.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>b : α<VAR>hb : ↑f b = 0<GOAL>↑f b * μ (↑(f.restrict s) ⁻¹' {↑f b}) = ↑f b * μ (↑f ⁻¹' {↑f b} ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>b : α<VAR>hb : ¬↑f b = 0<GOAL>↑f b * μ (↑(f.restrict s) ⁻¹' {↑f b}) = ↑f b * μ (↑f ⁻¹' {↑f b} ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>h : a ≠ 0<GOAL>a / a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<GOAL>f =ᶠ[ae μ] s.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>f' : α → ℝ := AEStronglyMeasurable.mk f ⋯<GOAL>f =ᶠ[ae μ] s.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>f' : α → ℝ := AEStronglyMeasurable.mk f ⋯<VAR>hadd' : s = t + μ.withDensityᵥ f'<GOAL>f =ᶠ[ae μ] s.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>f' : α → ℝ := AEStronglyMeasurable.mk f ⋯<VAR>hadd' : s = t + μ.withDensityᵥ f'<VAR>this : s.HaveLebesgueDecomposition μ<GOAL>f =ᶠ[ae μ] s.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t✝ t : SignedMeasure α<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<VAR>hadd : s = t + μ.withDensityᵥ f<VAR>f' : α → ℝ := AEStronglyMeasurable.mk f ⋯<VAR>hadd' : s = t + μ.withDensityᵥ f'<VAR>this : s.HaveLebesgueDecomposition μ<GOAL>μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Rack R✝<VAR>R : Type u_2<VAR>inst✝ : Rack R<VAR>x y z : R<GOAL>x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Rack R✝<VAR>R : Type u_2<VAR>inst✝ : Rack R<VAR>x y z : R<GOAL>(x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<GOAL>M.charpolyRev.coeff 1 = -M.trace
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h✝ : IsEmpty n<GOAL>M.charpolyRev.coeff 1 = -M.trace
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>h✝ : Nonempty n<GOAL>M.charpolyRev.coeff 1 = -M.trace
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DecidableEq β<VAR>f g : α →. β<VAR>inst✝² : (x : α) → Decidable (f x).Dom<VAR>inst✝¹ : (x : α) → Decidable (g x).Dom<VAR>s t : Finset α<VAR>b : β<VAR>inst✝ : DecidableEq α<GOAL>pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f (insert a s) t = (fun b => f a b) '' t ∪ image2 f s t
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>W (fun x => x ∈ Set.range F.obj) f ↔ IsIso (G.map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>W (fun x => x ∈ Set.range F.obj) (f ≫ adj.unit.app Y) ↔ IsIso (G.map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>W (fun x => x ∈ Set.range F.obj) (adj.unit.app X ≫ (G ⋙ F).map f) ↔ IsIso (G.map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>IsIso ((G ⋙ F).map f) ↔ IsIso (G.map f)