ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>this : A_compare = B_compare<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a✝ : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<VAR>a : α<GOAL>a ∈ (filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts).biUnion id ↔ a ∈ t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a✝ : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<VAR>a : α<VAR>ha : a ∈ t<GOAL>∃ a_1 ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts, a ∈ id a_1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u✝ : Finset α<VAR>P : Finpartition s<VAR>a✝ : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<VAR>a : α<VAR>ha : a ∈ t<VAR>u : Finset α<VAR>hu : u ∈ (atomise s F).parts<VAR>hau : a ∈ u<GOAL>∃ a_1 ∈ filter (fun u => u ⊆ t ∧ u.Nonempty) (atomise s F).parts, a ∈ id a_1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u✝ : Finset α<VAR>P : Finpartition s<VAR>a✝ : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<VAR>a : α<VAR>ha : a ∈ t<VAR>u : Finset α<VAR>hu : u ∈ (atomise s F).parts<VAR>hau : a ∈ u<VAR>b : α<VAR>hb : b ∈ u<GOAL>b ∈ t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a✝ : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<VAR>a : α<VAR>ha : a ∈ t<VAR>b : α<VAR>Q : Finset (Finset α)<VAR>_hQ : Q ⊆ F<VAR>hu : filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s ∈ (atomise s F).parts<VAR>hau : a ∈ filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s<VAR>hb : b ∈ filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s<GOAL>b ∈ t
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a✝ : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<VAR>a : α<VAR>ha : a ∈ t<VAR>b : α<VAR>Q : Finset (Finset α)<VAR>_hQ : Q ⊆ F<VAR>hu : filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s ∈ (atomise s F).parts<VAR>hau : a ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ a ∈ u<VAR>hb : b ∈ s ∧ ∀ u ∈ F, u ∈ Q ↔ b ∈ u<GOAL>b ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ : Set α<VAR>h : s₂ ⊆ s₁<VAR>x : α<GOAL>x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>hμ₁ : μ s = ⊤<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>hμ₁ : μ s ≠ ⊤<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}<GOAL>0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}<GOAL>0 < (μ.restrict s) {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})<GOAL>0 < (μ.restrict s) {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})<GOAL>{a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤} ⊆ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})<VAR>x : α<VAR>hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal<VAR>hx : x ∉ {x | g x = ⊤}<GOAL>x ∈ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})<VAR>x : α<VAR>hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x<VAR>hx : x ∉ {x | g x = ⊤}<GOAL>x ∈ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
<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 N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hs : NullMeasurableSet s μ<VAR>hμ₁ : μ s ≠ ⊤<VAR>g : α → ℝ≥0∞<VAR>hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ⊤<VAR>hg : Measurable g<VAR>hgf : g ≤ f<VAR>hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ<VAR>hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ<VAR>this : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})<VAR>x : α<VAR>hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal<VAR>hx : x ∉ {x | g x = ⊤}<GOAL>∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>h : f x = 2<VAR>m : M<GOAL>(preReflection ((preReflection x f) y) ((preReflection f ((Dual.eval R M) x)) g)) m = (preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>h : f x = 2<VAR>m : M<GOAL>m - (g m • y - (f m * g x) • y - ((g m * f y) • x - (f m * (g x * f y)) • x)) = m - f m • x - (g m • y - (g m * f y) • x) - (f m • x - (f m • x + f m • x) - ((f m * g x) • y - (f m * (g x * f y)) • x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>g : CauSeq β abv<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>abv (f j - f i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>g : CauSeq β abv<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>h₁ : abv (f i - ↑g i) < ε / 2 / 2<VAR>h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2<GOAL>abv (f j - f i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>g : CauSeq β abv<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>h₁ : abv (↑g i - f i) < ε / 2 / 2<VAR>h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2<GOAL>abv (f j - f i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>g : CauSeq β abv<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>h₁ : abv (↑g i - f i) < ε / 2 / 2<VAR>h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2<VAR>this : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2<GOAL>abv (f j - f i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>g : CauSeq β abv<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>h₁ : abv (↑g i - f i) < ε / 2 / 2<VAR>h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2<VAR>this✝ : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2<VAR>this : abv (f j - ↑g j + (↑g i - f i) + (↑g j - ↑g i)) < ε / 2 / 2 + ε / 2 / 2 + ε / 2<GOAL>abv (f j - f i) < ε
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k d : ℕ+<VAR>ζ : Mˣ<VAR>h : ζ ∈ rootsOfUnity k M<GOAL>ζ ∈ rootsOfUnity (k * d) M
<VAR>self : Aesop.Script.LazyStep<GOAL>0 < self.tacticBuilders.size
<VAR>P : Prop<VAR>h : P → False<GOAL>¬P
<VAR>α : Sort u_1<VAR>x y : α<GOAL>HEq x y ↔ x = y
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Monad m<VAR>a : α<VAR>f : α → m (ForInStep α)<GOAL>(ForInStep.done a).bind f = pure (ForInStep.done a)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Monad m<VAR>a : α<VAR>f : α → m (ForInStep α)<GOAL>(ForInStep.yield a).bind f = f a
<GOAL>∀ {α : Type u_1} {a : α}, (ForInStep.done a).run = a
<GOAL>∀ {α : Type u_1} {a : α}, (ForInStep.yield a).run = a
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m (ForInStep β)<VAR>s : ForInStep β<GOAL>ForInStep.bindList f [] s = pure s
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m (ForInStep β)<VAR>s : ForInStep β<VAR>a : α<VAR>l : List α<GOAL>ForInStep.bindList f (a :: l) s = s.bind fun b => do let x ← f a b ForInStep.bindList f l x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m (ForInStep β)<VAR>a : β<VAR>l : List α<GOAL>ForInStep.bindList f l (ForInStep.done a) = pure (ForInStep.done a)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>f : α → β → m (ForInStep β)<VAR>s : ForInStep β<VAR>l : List α<GOAL>(s.bind fun a => ForInStep.bindList f l (ForInStep.yield a)) = ForInStep.bindList f l s
<VAR>m : Type u_1 → Type u_2<VAR>β : Type u_1<VAR>α : Type u_3<VAR>Monad m<VAR>LawfulMonad m<VAR>f : β → m (ForInStep β)<VAR>g : α → β → m (ForInStep β)<VAR>s : ForInStep β<VAR>l : List α<GOAL>(do let x ← s.bind f ForInStep.bindList g l x) = s.bind fun b => do let x ← f b ForInStep.bindList g l x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m (ForInStep β)<VAR>s : ForInStep β<VAR>a : α<VAR>l : List α<GOAL>ForInStep.bindList f (a :: l) s = do let x ← s.bind (f a) ForInStep.bindList f l x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m (ForInStep β)<VAR>s : ForInStep β<VAR>l₁ l₂ : List α<GOAL>ForInStep.bindList f (l₁ ++ l₂) s = do let x ← ForInStep.bindList f l₁ s ForInStep.bindList f l₂ x
<GOAL>∀ {α : Sort u_1} {a b : α}, HEq a b ↔ a = b
<VAR>α : Sort u_1<VAR>a a' : α<VAR>β : Sort u_2<VAR>y : β<VAR>h : a = a'<GOAL>h ▸ y = y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β → γ<VAR>x x' : α<VAR>y y' : β<VAR>hx : x = x'<VAR>hy : y = y'<GOAL>f x y = f x' y'
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>f g : (a : α) → (b : β a) → γ a b<VAR>h : f = g<VAR>a : α<VAR>b : β a<GOAL>f a b = g a b
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>δ : (a : α) → (b : β a) → γ a b → Sort u_4<VAR>f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c<VAR>h : f = g<VAR>a : α<VAR>b : β a<VAR>c : γ a b<GOAL>f a b c = g a b c
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>f g : (a : α) → (b : β a) → γ a b<VAR>h : ∀ (a : α) (b : β a), f a b = g a b<GOAL>f = g
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>γ : (a : α) → β a → Sort u_3<VAR>δ : (a : α) → (b : β a) → γ a b → Sort u_4<VAR>f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c<VAR>h : ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c<GOAL>f = g
<VAR>α : Sort u_1<VAR>β : α → Sort u<VAR>f₁ f₂ : (x : α) → β x<GOAL>f₁ = f₂ ↔ ∀ (a : α), f₁ a = f₂ a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>x y : α<GOAL>f x ≠ f y → x ≠ y
<GOAL>∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)
<VAR>α β : Sort u_1<VAR>a : α<VAR>a' : β<VAR>e : α = β<GOAL>cast e a = a' → HEq a a'
<GOAL>∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' ↔ HEq a_2 a'
<VAR>α : Sort u_1<VAR>a : α<VAR>motive : (a' : α) → a = a' → Sort u_2<VAR>x : motive a ⋯<VAR>a' : α<VAR>e : a = a'<GOAL>e ▸ x = cast ⋯ x
<VAR>α : Sort u_1<VAR>a : α<VAR>motive : (a' : α) → a = a' → Sort u_2<VAR>x : motive a ⋯<VAR>a' : α<VAR>e : a = a'<GOAL>HEq (e ▸ x) x
<VAR>α : Sort u_1<VAR>a : α<VAR>motive : (a' : α) → a = a' → Sort u_2<VAR>x : motive a ⋯<VAR>a' : α<VAR>e : a = a'<VAR>β : Sort u_2<VAR>y : β<GOAL>HEq (e ▸ x) y ↔ HEq x y
<VAR>α : Sort u_1<VAR>a : α<VAR>motive : (a' : α) → a = a' → Sort u_2<VAR>x : motive a ⋯<VAR>a' : α<VAR>e : a = a'<VAR>β : Sort u_2<VAR>y : β<GOAL>HEq y (e ▸ x) ↔ HEq y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Membership α β<VAR>s : β<VAR>a b : α<VAR>h : a ∈ s<GOAL>¬b ∈ s → a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Membership α β<VAR>s t : β<VAR>a : α<VAR>h : a ∈ s<GOAL>¬a ∈ t → s ≠ t
<VAR>α : Sort u_1<VAR>Subsingleton α<VAR>x y : α<GOAL>x = y ↔ True
<VAR>α : Sort u_1<VAR>x : α<VAR>h : ∀ (y : α), y = x<GOAL>Subsingleton α
<VAR>α : Sort u_1<VAR>x : α<GOAL>Subsingleton α ↔ ∀ (y : α), y = x
<VAR>α : Sort u_1<VAR>γ : Sort u_2<VAR>x x' : α<VAR>β : α → Sort u_3<VAR>f : (x : α) → β x → γ<VAR>h : x = x'<VAR>y : β x<GOAL>f x' (h ▸ y) = f x y
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>motive : (a : α) → Acc r a → Sort v<VAR>intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (hr : r y x) → motive y ⋯) → motive x ⋯<VAR>a : α<VAR>h : ∀ (y : α), r y a → Acc r y<GOAL>Acc.recC intro ⋯ = intro a h fun y hr => Acc.recC intro ⋯
<GOAL>@WellFounded.fixF = @WellFounded.fixFC
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Nat<VAR>f : α → α<GOAL>(a.modify i f).size = a.size
<VAR>α : Type u_1<VAR>BEq α<VAR>self : PartialEquivBEq α<VAR>a b : α<GOAL>(a == b) = true → (b == a) = true
<VAR>α : Type u_1<VAR>BEq α<VAR>self : PartialEquivBEq α<VAR>a b c : α<GOAL>(a == b) = true → (b == c) = true → (a == c) = true
<VAR>self : Aesop.LocalRuleSet<GOAL>0 < self.simprocsArray.size
<VAR>self : Aesop.LocalRuleSet<GOAL>0 < self.simpTheoremsArray.size
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p : α → Prop<VAR>Applicative m<VAR>LawfulApplicative m<VAR>x : m α<VAR>h : ∀ (a : α), p a<GOAL>SatisfiesM p x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Applicative m<VAR>LawfulApplicative m<VAR>x : m α<GOAL>SatisfiesM (fun x => True) x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>Functor m<VAR>LawfulFunctor m<VAR>x : m α<VAR>h : SatisfiesM p x<VAR>H : ∀ {a : α}, p a → q a<GOAL>SatisfiesM q x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>∀ {α_1 : Type u_1} {q : α_1 → Prop} {f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <$> x)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>∀ {α_1 : Type u_1} {f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p x → SatisfiesM (fun b => ∃ a, p a ∧ b = f a) (f <$> x)