ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>f : E →SL[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>hC : 0 ≤ C<VAR>hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖<GOAL>‖f‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>f : E →SL[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>hC : 0 ≤ C<VAR>hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>‖f‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝¹ : E<VAR>f : E →SL[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>hC : 0 ≤ C<VAR>hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>x✝ : ε / ‖c‖ ≤ ‖x‖<VAR>hx : ‖x‖ < ε<GOAL>x ∈ ball 0 ε
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>inst✝⁴ : Fintype ↑G.edgeSet<VAR>inst✝³ : Fintype ↑G₁.edgeSet<VAR>inst✝² : Fintype ↑G₂.edgeSet<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<GOAL>⊤.edgeFinset.card = (Fintype.card V).choose 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<GOAL>dropSlice n m xs ~ ys ∩ dropSlice n m xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<GOAL>take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<VAR>this : n ≤ n + m<GOAL>take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<VAR>this : n ≤ n + m<VAR>h₂ : xs.Nodup<GOAL>take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<VAR>this : n ≤ n + m<VAR>h₂ : xs.Nodup<GOAL>take n xs ++ drop (n + m) xs ~ ys ∩ take n xs ++ ys ∩ drop (n + m) xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<VAR>this : n ≤ n + m<VAR>h₂ : xs.Nodup<GOAL>(take n xs).Disjoint (drop (n + m) xs)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<GOAL>eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<GOAL>eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<GOAL>eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>h'p : p < 1<GOAL>eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>h'p : 1 ≤ p<GOAL>eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)<GOAL>(J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus P) F) hP
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)<GOAL>J.toPlus (P ⋙ F) ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus P) F
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>m : Multiset α<VAR>t : (a : α) → Multiset (β a)<GOAL>∀ (a : α) (s : Multiset α), card (s.pi t) = (map (fun a => card (t a)) s).prod → card ((a ::ₘ s).pi t) = (map (fun a => card (t a)) (a ::ₘ s)).prod
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hAC : IsExtreme 𝕜 A C<GOAL>IsExtreme 𝕜 A (B ∩ C)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hAC : IsExtreme 𝕜 A C<GOAL>∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x : E⦄, x ∈ B ∩ C → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hAC : IsExtreme 𝕜 A C<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxB : x ∈ B<VAR>hxC : x ∈ C<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<GOAL>x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hAC : IsExtreme 𝕜 A C<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxB : x ∈ B<VAR>hxC : x ∈ C<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>hx₁B : x₁ ∈ B<VAR>hx₂B : x₂ ∈ B<GOAL>x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>hAB : IsExtreme 𝕜 A B<VAR>hAC : IsExtreme 𝕜 A C<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxB : x ∈ B<VAR>hxC : x ∈ C<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>hx₁B : x₁ ∈ B<VAR>hx₂B : x₂ ∈ B<VAR>hx₁C : x₁ ∈ C<VAR>hx₂C : x₂ ∈ C<GOAL>x₁ ∈ B ∩ C ∧ x₂ ∈ B ∩ C
<VAR>θ ψ : Angle<GOAL>θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑π
<VAR>θ : Angle<VAR>x✝ : ℝ<GOAL>θ.sin = (↑x✝).sin ↔ θ = ↑x✝ ∨ θ + ↑x✝ = ↑π
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>a : G<GOAL>image₂ (fun x x_1 => x * x_1) f.support {a} ⊆ image (fun x => x * a) f.support
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁶ : Countable ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : MeasurableSpace ι<VAR>inst✝³ : BorelSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSingletonClass ι<VAR>inst✝ : SecondCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>MeasurableSet {ω | τ ω = π ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁶ : Countable ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : MeasurableSpace ι<VAR>inst✝³ : BorelSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSingletonClass ι<VAR>inst✝ : SecondCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<GOAL>∀ (i : ι), MeasurableSet ({ω | τ ω = π ω} ∩ {ω | τ ω ≤ i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁶ : Countable ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : MeasurableSpace ι<VAR>inst✝³ : BorelSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSingletonClass ι<VAR>inst✝ : SecondCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>MeasurableSet ({ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁶ : Countable ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : MeasurableSpace ι<VAR>inst✝³ : BorelSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSingletonClass ι<VAR>inst✝ : SecondCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>MeasurableSet {ω | min (τ ω) j = min (π ω) j}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁶ : Countable ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : MeasurableSpace ι<VAR>inst✝³ : BorelSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSingletonClass ι<VAR>inst✝ : SecondCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>Measurable fun x => min (τ x) j
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝⁶ : Countable ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : MeasurableSpace ι<VAR>inst✝³ : BorelSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : MeasurableSingletonClass ι<VAR>inst✝ : SecondCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>j : ι<VAR>this : {ω | τ ω = π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j = min (π ω) j} ∩ {ω | τ ω ≤ j} ∩ {ω | π ω ≤ j}<GOAL>Measurable fun x => min (π x) j
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f g k : MulRingNorm R<VAR>c : ℝ<VAR>hcPos : 0 < c<VAR>hfg : (fun x => f x ^ c) = ⇑g<VAR>d : ℝ<VAR>hdPos : 0 < d<VAR>hgk : (fun x => g x ^ d) = ⇑k<GOAL>f.equiv k
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f g k : MulRingNorm R<VAR>c : ℝ<VAR>hcPos : 0 < c<VAR>hfg : (fun x => f x ^ c) = ⇑g<VAR>d : ℝ<VAR>hdPos : 0 < d<VAR>hgk : (fun x => g x ^ d) = ⇑k<GOAL>(fun x => f x ^ (c * d)) = ⇑k
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x✝ y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f g k : MulRingNorm R<VAR>c : ℝ<VAR>hcPos : 0 < c<VAR>hfg : (fun x => f x ^ c) = ⇑g<VAR>d : ℝ<VAR>hdPos : 0 < d<VAR>hgk : (fun x => g x ^ d) = ⇑k<VAR>x : R<GOAL>f x ^ (c * d) = k x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁹ : Nonempty ι<VAR>inst✝⁸ : Nonempty ι'<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>WithSeminorms fun s => s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁹ : Nonempty ι<VAR>inst✝⁸ : Nonempty ι'<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>Seminorm.IsBounded p (fun s => s.sup p) LinearMap.id
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁹ : Nonempty ι<VAR>inst✝⁸ : Nonempty ι'<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>Seminorm.IsBounded (fun s => s.sup p) p LinearMap.id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s✝ : Finset α<VAR>f : α ↪ β<VAR>g : β ↪ γ<VAR>s : Finset α<GOAL>(map g (map f s)).val = (map (f.trans g) s).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s✝ : Finset α<VAR>f : α ↪ β<VAR>g : β ↪ γ<VAR>s : Finset α<GOAL>Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x✝¹ x✝ : α<GOAL>Setoid.r x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x✝¹ x✝ : α<GOAL>(fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>S : ∀ {x y : α}, R x y → R y x<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>d : Pairwise R l₁<GOAL>Pairwise R l₂
<VAR>n✝ : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>n : ℕ∞<VAR>hf : HasCompactSupport f<VAR>h'f : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<GOAL>∃ C, LipschitzWith C f
<VAR>n✝ : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>n : ℕ∞<VAR>hf : HasCompactSupport f<VAR>h'f : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<VAR>C : ℝ<VAR>hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C<GOAL>∃ C, LipschitzWith C f
<VAR>n✝ : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>n : ℕ∞<VAR>hf : HasCompactSupport f<VAR>h'f : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<VAR>C : ℝ<VAR>hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C<GOAL>LipschitzWith ⟨max C 0, ⋯⟩ f
<VAR>n✝ : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁴ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕂 F'<VAR>f : E' → F'<VAR>n : ℕ∞<VAR>hf : HasCompactSupport f<VAR>h'f : ContDiff 𝕂 n f<VAR>hn : 1 ≤ n<VAR>C : ℝ<VAR>hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C<VAR>x : E'<GOAL>‖fderiv 𝕂 f x‖₊ ≤ ⟨max C 0, ⋯⟩
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ -y ≠ 0<GOAL>‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
<VAR>k n m : ℕ<GOAL>(k + n).dist (k + m) = n.dist m
<VAR>k n m : ℕ<GOAL>(n + k).dist (m + k) = n.dist m
<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 : Fin 3 → F<VAR>hPz : P z = 0<GOAL>toAffine W P = 0
<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>padicValInt p ↑p = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, image2 f (s i j) t
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle x (x - y)).sin = ‖y‖ / ‖x - y‖
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>4 ^ P.parts.card ≤ m
<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✝¹ : AddMonoid M<VAR>inst✝ : SMulZeroClass R M<VAR>b : R<VAR>g : α →₀ M<VAR>a : α<GOAL>a ∈ (b • g).support → a ∈ g.support
<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✝¹ : AddMonoid M<VAR>inst✝ : SMulZeroClass R M<VAR>b : R<VAR>g : α →₀ M<VAR>a : α<GOAL>¬b • g a = 0 → ¬g a = 0
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>A : C<VAR>h : A ∈ i.essImage<GOAL>IsIso ((reflectorAdjunction i).unit.app A)
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>ht : t.Nonempty<VAR>hb : ↑s.card ≤ t.card • b<GOAL>∃ y ∈ t, ↑(filter (fun x => f x = y) s).card ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCommSemiring M<VAR>ht : t.Nonempty<VAR>hb : ∑ a ∈ s, 1 ≤ t.card • b<GOAL>∃ y ∈ t, ∑ a ∈ filter (fun x => f x = y) s, 1 ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a<GOAL>(κ.withDensity fun a x => f a x - g a x) + κ.withDensity g = κ.withDensity f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a<GOAL>κ.withDensity ((fun a x => f a x - g a x) + g) = κ.withDensity f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), g a ≤ᶠ[ae (κ a)] f a<GOAL>Measurable (Function.uncurry fun a x => f a x - g a x)