ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<VAR>h_left_eq' : (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = (T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a))<GOAL>(T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<VAR>h_left_eq' : (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = (T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a))<GOAL>(∑ i ∈ filter (fun b => g b = g (↑f a)) f.range, T (↑f ⁻¹' {i})) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<VAR>h_left_eq' : (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = (T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a))<GOAL>∀ (i : G), MeasurableSet (↑f ⁻¹' {i})
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<VAR>h_left_eq' : (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = (T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a))<GOAL>∀ i ∈ filter (fun b => g b = g (↑f a)) f.range, μ (↑f ⁻¹' {i}) ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<VAR>h_left_eq' : (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = (T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a))<GOAL>∀ i ∈ filter (fun b => g b = g (↑f a)) f.range, ∀ j ∈ filter (fun b => g b = g (↑f a)) f.range, i ≠ j → Disjoint (↑f ⁻¹' {i}) (↑f ⁻¹' {j})
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : P<VAR>ps : Set P<GOAL>affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<GOAL>a / b = c / d ↔ a / c = b / d
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<GOAL>a = c / d * b ↔ a / c = b / d
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<GOAL>a = c / d * b ↔ a = b / d * c
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>x : α<VAR>xs : List α<VAR>n✝ : ℕ<VAR>inst✝ : Inhabited α<VAR>n : ℕ<GOAL>l.getI n = (l.get? n).iget
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J : Ideal R<VAR>hi : I.IsPrimary<VAR>hj : J.IsPrimary<VAR>hij : I.radical = J.radical<VAR>x y : R<VAR>x✝ : x * y ∈ I ⊓ J<VAR>hxyi : x * y ∈ ↑I<VAR>hxyj : x * y ∈ ↑J<GOAL>x ∈ I ⊓ J ∨ y ∈ (I ⊓ J).radical
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J : Ideal R<VAR>hi : I.IsPrimary<VAR>hj : J.IsPrimary<VAR>hij : I.radical = J.radical<VAR>x y : R<VAR>x✝ : x * y ∈ I ⊓ J<VAR>hxyi : x * y ∈ ↑I<VAR>hxyj : x * y ∈ ↑J<GOAL>x ∈ I ⊓ J ∨ y ∈ J.radical
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J : Ideal R<VAR>hi : I.IsPrimary<VAR>hj : J.IsPrimary<VAR>hij : I.radical = J.radical<VAR>x y : R<VAR>x✝ : x * y ∈ I ⊓ J<VAR>hxyi : x * y ∈ ↑I<VAR>hxyj : x * y ∈ ↑J<VAR>hxi : x ∈ I<GOAL>x ∈ I ⊓ J ∨ y ∈ J.radical
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J : Ideal R<VAR>hi : I.IsPrimary<VAR>hj : J.IsPrimary<VAR>hij : I.radical = J.radical<VAR>x y : R<VAR>x✝ : x * y ∈ I ⊓ J<VAR>hxyi : x * y ∈ ↑I<VAR>hxyj : x * y ∈ ↑J<VAR>hyi : y ∈ I.radical<GOAL>x ∈ I ⊓ J ∨ y ∈ J.radical
<VAR>N k n : ℕ<GOAL>n ∈ N.smoothNumbersUpTo k ↔ n ≤ N ∧ n ∈ k.smoothNumbers
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy₁ : x₁ ≡ y₁ [SMOD U]<VAR>hxy₂ : x₂ ≡ y₂ [SMOD U]<GOAL>x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁<VAR>hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂<GOAL>Submodule.Quotient.mk (x₁ + x₂) = Submodule.Quotient.mk (y₁ + y₂)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>(C a * X ^ n).roots = n • {0}
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>t : Finset ι<VAR>hs : ∀ i ∈ t, s i ≠ 0<VAR>pp : (↑t).Pairwise (Coprime on s)<GOAL>↑(chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>x y : α<GOAL>inv Eq x y ↔ x = y
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e ϕ : A₁ ≃ₐ[R] A₂<VAR>ψ χ : A₁ ≃ₐ[R] A₁<VAR>a✝ : A₂<GOAL>({ toFun := fun ψ => ϕ.symm.trans (ψ.trans ϕ), invFun := fun ψ => ϕ.trans (ψ.trans ϕ.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (ψ * χ)) a✝ = ({ toFun := fun ψ => ϕ.symm.trans (ψ.trans ϕ), invFun := fun ψ => ϕ.trans (ψ.trans ϕ.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ψ * { toFun := fun ψ => ϕ.symm.trans (ψ.trans ϕ), invFun := fun ψ => ϕ.trans (ψ.trans ϕ.symm), left_inv := ⋯, right_inv := ⋯ }.toFun χ) a✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2<GOAL>StrictConvexSpace ℝ E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2<VAR>x y : E<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<VAR>hne : x ≠ y<GOAL>‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2<VAR>x y : E<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<VAR>hne : x ≠ y<GOAL>¬‖x + y‖ = 2
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<GOAL>WithSeminorms fun x => normSeminorm 𝕜 E
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<GOAL>𝓝 0 = 𝓝 0
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<GOAL>(𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<GOAL>(𝓝 0).HasBasis (fun x => 0 < x) ((normSeminorm 𝕜 E).ball 0)
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<GOAL>∀ i ∈ p.addGroupFilterBasis, ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id i
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id U
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset (Fin 1)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id U
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset (Fin 1)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>(normSeminorm 𝕜 E).ball 0 r ⊆ id U
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset (Fin 1)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>h : ¬s.Nonempty<GOAL>(normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r
<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>𝕜 : Type u_10<VAR>E : Type u_11<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset (Fin 1)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>h : ¬s.Nonempty<GOAL>(normSeminorm 𝕜 E).ball 0 r ⊆ univ
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>hF : Fact (finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x y : F<VAR>this : ⇑φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y]<GOAL>(((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<GOAL>Function.Surjective ⇑((forget₂ C Ab).map S.g)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<GOAL>Epi S.g
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>inst✝¹ : DecidableRel lt<VAR>inst✝ : IsStrictOrder α lt<VAR>a b : α<GOAL>cmpUsing lt a b = Ordering.gt ↔ lt b a
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>inst✝¹ : DecidableRel lt<VAR>inst✝ : IsStrictOrder α lt<VAR>a b : α<GOAL>lt b a → ¬lt a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<GOAL>induced f inst✝¹ = Preorder.topology α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<GOAL>Preorder.topology α ≤ induced f inst✝¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>a : α<GOAL>𝓝 a ≤ 𝓝 a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>a : α<GOAL>(⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ (⨅ i ∈ Iio (f a), 𝓟 (f ⁻¹' Ioi i)) ⊓ ⨅ i ∈ Ioi (f a), 𝓟 (f ⁻¹' Iio i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>a : α<VAR>b : β<VAR>hb : b ∈ Iio (f a)<GOAL>⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, f x < f y ↔ x < y<VAR>H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y<VAR>H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b<VAR>x✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α<VAR>a : α<VAR>b : β<VAR>hb : b ∈ Ioi (f a)<GOAL>⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : NonUnitalSubalgebra R A<GOAL>Submodule.span R ↑s = s.toSubmodule
<VAR>a✝ b c : Ordinal.{u}<VAR>h : b ≤ c<VAR>a : Ordinal.{u}<GOAL>a ♯ b ≤ a ♯ c
<VAR>a✝ b c : Ordinal.{u}<VAR>h✝ : b ≤ c<VAR>a : Ordinal.{u}<VAR>h : b < c<GOAL>a ♯ b ≤ a ♯ c
<VAR>a✝ b a : Ordinal.{u}<VAR>h : b ≤ b<GOAL>a ♯ b ≤ a ♯ b
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>(∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
<VAR>a b : Cardinal.{u_1}<GOAL>a.alephIdx ≤ b.alephIdx ↔ a ≤ b
<VAR>V : Type (u + 1)<VAR>inst✝ : LargeCategory V<VAR>G : Grp<VAR>A : Action V (MonCat.of ↑G)<VAR>g : ↑G<GOAL>A.ρ (g⁻¹ * g) = 𝟙 A.V
<VAR>V : Type (u + 1)<VAR>inst✝ : LargeCategory V<VAR>G : Grp<VAR>A : Action V (MonCat.of ↑G)<VAR>g : ↑G<GOAL>A.ρ (g * g⁻¹) = 𝟙 A.V
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ (fun a => (a, b)) '' s
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>a / 0 = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<VAR>h : xᶜ = y<GOAL>IsCompl x xᶜ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 1 g<VAR>x₀ : G<GOAL>HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[precompR G L, μ] fderiv 𝕜 g) x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>hf : LocallyIntegrable f μ<VAR>x₀ : G<VAR>hcg : HasCompactSupport 0<VAR>hg : ContDiff 𝕜 1 0<GOAL>HasFDerivAt (f ⋆[L, μ] 0) ((f ⋆[precompR G L, μ] fderiv 𝕜 0) x₀) x₀