ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : (i : o) → Fintype (n' i)<VAR>inst✝ : Fintype o<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>N : (i : o) → Matrix (n' i) (p' i) α<VAR>k : o<VAR>i : m' k<VAR>k' : o<VAR>j : p' k'<GOAL>(if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) = ∑ x : o, ∑ x_1 : n' x, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : (i : o) → Fintype (n' i)<VAR>inst✝ : Fintype o<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>N : (i : o) → Matrix (n' i) (p' i) α<VAR>k : o<VAR>i : m' k<VAR>k' : o<VAR>j : p' k'<GOAL>(if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0) = ∑ x : n' k, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : (i : o) → Fintype (n' i)<VAR>inst✝ : Fintype o<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>N : (i : o) → Matrix (n' i) (p' i) α<VAR>k : o<VAR>i : m' k<VAR>k' : o<VAR>j : p' k'<GOAL>∀ (x : o), x ≠ k → (∑ x_1 : n' x, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, NullMeasurableSet (t i) μ<VAR>H : μ univ < ∑ i ∈ s, μ (t i)<GOAL>∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, NullMeasurableSet (t i) μ<VAR>H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅<GOAL>∑ i ∈ s, μ (t i) ≤ μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, NullMeasurableSet (t i) μ<VAR>H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅<GOAL>(↑s).Pairwise (AEDisjoint μ on t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, NullMeasurableSet (t i) μ<VAR>H : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → t i ∩ t j = ∅<VAR>i : ι<VAR>hi : i ∈ ↑s<VAR>j : ι<VAR>hj : j ∈ ↑s<VAR>hij : i ≠ j<GOAL>(AEDisjoint μ on t) i j
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x<GOAL>∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) = (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) - (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x<GOAL>∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) = ∫ (x : ℝ) in 0 ..π / 2, ↑(sin x) * ↑(cos x) ^ (n - 1) * Complex.sin (2 * z * ↑x)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x<GOAL>(↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) - (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) = ↑(sin (π / 2)) * ↑(cos (π / 2)) ^ (n - 1) * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) - ↑(sin 0) * ↑(cos 0) ^ (n - 1) * (-Complex.cos (2 * z * ↑0) / (2 * z)) - ∫ (x : ℝ) in 0 ..π / 2, (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x<GOAL>IntervalIntegrable (fun x => ↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) volume 0 (π / 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x<GOAL>IntervalIntegrable (fun x => Complex.sin (2 * z * ↑x)) volume 0 (π / 2)
<VAR>α : Type u_1<VAR>inst✝ : AddGroup α<VAR>n : ℕ<VAR>hn : (Nat.card α).Coprime n<VAR>a : α<GOAL>n • (↑n)⁻¹.val • a = a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y₁ Y₂ : D<VAR>f : Y₁ ⟶ Y₂<VAR>g₁ g₂ : StructuredArrow Y₂ L<VAR>φ : g₁ ⟶ g₂<GOAL>((const (StructuredArrow Y₂ L)).obj (limit (StructuredArrow.proj Y₁ L ⋙ F))).map φ ≫ (fun g => limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g)) g₂ = (fun g => limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g)) g₁ ≫ (StructuredArrow.proj Y₂ L ⋙ F).map φ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y : D<VAR>j : StructuredArrow Y L<GOAL>limit.lift (StructuredArrow.proj Y L ⋙ F) { pt := limit (StructuredArrow.proj Y L ⋙ F), π := { app := fun g => limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj g), naturality := ⋯ } } ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j = 𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y : D<VAR>j : StructuredArrow Y L<GOAL>limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj j) = limit.π (StructuredArrow.proj Y L ⋙ F) j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y : D<VAR>j : StructuredArrow Y L<GOAL>(StructuredArrow.map (𝟙 Y)).obj j = j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y₁ Y₂ Y₃ : D<VAR>f : Y₁ ⟶ Y₂<VAR>f' : Y₂ ⟶ Y₃<VAR>j : StructuredArrow Y₃ L<GOAL>limit.lift (StructuredArrow.proj Y₃ L ⋙ F) { pt := limit (StructuredArrow.proj Y₁ L ⋙ F), π := { app := fun g => limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map (f ≫ f')).obj g), naturality := ⋯ } } ≫ limit.π (StructuredArrow.proj Y₃ L ⋙ F) j = (limit.lift (StructuredArrow.proj Y₂ L ⋙ F) { pt := limit (StructuredArrow.proj Y₁ L ⋙ F), π := { app := fun g => limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g), naturality := ⋯ } } ≫ limit.lift (StructuredArrow.proj Y₃ L ⋙ F) { pt := limit (StructuredArrow.proj Y₂ L ⋙ F), π := { app := fun g => limit.π (StructuredArrow.proj Y₂ L ⋙ F) ((StructuredArrow.map f').obj g), naturality := ⋯ } }) ≫ limit.π (StructuredArrow.proj Y₃ L ⋙ F) j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y₁ Y₂ Y₃ : D<VAR>f : Y₁ ⟶ Y₂<VAR>f' : Y₂ ⟶ Y₃<VAR>j : StructuredArrow Y₃ L<GOAL>limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map (f ≫ f')).obj j) = limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj ((StructuredArrow.map f').obj j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.123995, u_1} C<VAR>inst✝² : Category.{?u.123999, u_2} D<VAR>inst✝¹ : Category.{?u.124003, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>Y₁ Y₂ Y₃ : D<VAR>f : Y₁ ⟶ Y₂<VAR>f' : Y₂ ⟶ Y₃<VAR>j : StructuredArrow Y₃ L<GOAL>(StructuredArrow.map (f ≫ f')).obj j = (StructuredArrow.map f).obj ((StructuredArrow.map f').obj j)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>e : F ≃L[𝕜] G<GOAL>ContDiff 𝕜 n (⇑e ∘ f) ↔ ContDiff 𝕜 n f
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>x : E<GOAL>f.normed μ x ≤ 1 / (μ (closedBall c f.rIn)).toReal
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>x : E<GOAL>↑f x / ∫ (x : E), ↑f x ∂μ ≤ 1 / (μ (closedBall c f.rIn)).toReal
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>M.E = ∅ ↔ M = emptyOn α
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>M.E = ∅ → ∀ I ⊆ M.E, M.Indep I ↔ I = ∅
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>x✝ y✝ : R✝<VAR>inst✝¹ : CommSemiring R✝<VAR>x y : R✝<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<GOAL>sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}
<VAR>x✝ y x : ℝ<GOAL>x < sin (π / 2) ↔ x < 1
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>(p.succAbove i).rev = p.rev.succAbove i.rev
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>x : E<GOAL>iteratedFDeriv 𝕜 n (fun x => 0) x = 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ✝ ε δ : ℝ<VAR>s : Set E<VAR>x : E<GOAL>infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ✝ ε δ : ℝ<VAR>s : Set E<VAR>x : E<VAR>hδ : δ ≤ 0<GOAL>infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ✝ ε δ : ℝ<VAR>s : Set E<VAR>x : E<VAR>hδ : 0 < δ<GOAL>infEdist x (cthickening δ s) = infEdist x s - ENNReal.ofReal δ
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<GOAL>M.Basis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Indep I<GOAL>e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
<VAR>n : ℕ<GOAL>(2 * n)! ≤ (2 * n) ^ n * n !
<VAR>n : ℕ<GOAL>(n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → Option β<VAR>s' s t : Finset α<VAR>f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'<GOAL>∀ (x : β), x ∈ ↑(filterMap f s f_inj) ↔ x ∈ {b | ∃ a ∈ s, f a = some b}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<GOAL>IsPreconnected (f '' s) ↔ IsPreconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<VAR>h : IsPreconnected (f '' s)<GOAL>IsPreconnected s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<VAR>h : IsPreconnected (f '' s)<VAR>u v : Set α<VAR>hu' : IsOpen u<VAR>hv' : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxu : x ∈ u<VAR>y : α<VAR>hys : y ∈ s<VAR>hyv : y ∈ v<GOAL>(s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<VAR>h : IsPreconnected (f '' s)<VAR>v : Set α<VAR>hv' : IsOpen v<VAR>x : α<VAR>hxs : x ∈ s<VAR>y : α<VAR>hys : y ∈ s<VAR>hyv : y ∈ v<VAR>u : Set β<VAR>hu : IsOpen u<VAR>hu' : IsOpen (f ⁻¹' u)<VAR>huv : s ⊆ f ⁻¹' u ∪ v<VAR>hxu : x ∈ f ⁻¹' u<GOAL>(s ∩ (f ⁻¹' u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<VAR>h : IsPreconnected (f '' s)<VAR>x : α<VAR>hxs : x ∈ s<VAR>y : α<VAR>hys : y ∈ s<VAR>u : Set β<VAR>hu : IsOpen u<VAR>hu' : IsOpen (f ⁻¹' u)<VAR>hxu : x ∈ f ⁻¹' u<VAR>v : Set β<VAR>hv : IsOpen v<VAR>hv' : IsOpen (f ⁻¹' v)<VAR>hyv : y ∈ f ⁻¹' v<VAR>huv : s ⊆ f ⁻¹' u ∪ f ⁻¹' v<GOAL>(s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<VAR>h : IsPreconnected (f '' s)<VAR>x : α<VAR>hxs : x ∈ s<VAR>y : α<VAR>hys : y ∈ s<VAR>u : Set β<VAR>hu : IsOpen u<VAR>hu' : IsOpen (f ⁻¹' u)<VAR>hxu : x ∈ f ⁻¹' u<VAR>v : Set β<VAR>hv : IsOpen v<VAR>hv' : IsOpen (f ⁻¹' v)<VAR>hyv : y ∈ f ⁻¹' v<VAR>huv : f '' s ⊆ u ∪ v<GOAL>(s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Inducing f<VAR>h : IsPreconnected (f '' s)<VAR>x : α<VAR>hxs : x ∈ s<VAR>y : α<VAR>hys : y ∈ s<VAR>u : Set β<VAR>hu : IsOpen u<VAR>hu' : IsOpen (f ⁻¹' u)<VAR>hxu : x ∈ f ⁻¹' u<VAR>v : Set β<VAR>hv : IsOpen v<VAR>hv' : IsOpen (f ⁻¹' v)<VAR>hyv : y ∈ f ⁻¹' v<VAR>huv : f '' s ⊆ u ∪ v<VAR>z : α<VAR>hzs : z ∈ s<VAR>hzuv : f z ∈ u ∩ v<GOAL>(s ∩ (f ⁻¹' u ∩ f ⁻¹' v)).Nonempty
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>h : s ⊆ t<GOAL>μ (toMeasurable (μ.restrict t) s ∩ t) = (μ.restrict t) s
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<GOAL>M ⊨ L.infiniteTheory ↔ Infinite M
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>a₁ : σ₁<GOAL>(∀ ⦃a₂ : σ₂⦄, (fun a b => tr a = b) a₁ a₂ → match f₁ a₁ with | some b₁ => ∃ b₂, (fun a b => tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂ | none => f₂ a₂ = none) ↔ FRespects f₂ tr (tr a₁) (f₁ a₁)
<VAR>s n : Nat<GOAL>range' s n = map (fun x => s + x) (range n)
<VAR>s n : Nat<GOAL>range' s n = range' (s + 0) n
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝³ : MeasurableSpace ι<VAR>t : ι → Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : MetrizableSpace ι<VAR>h : ProgMeasurable f u<VAR>ht : ProgMeasurable f t<VAR>ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i<VAR>i : ι<GOAL>StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝³ : MeasurableSpace ι<VAR>t : ι → Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : MetrizableSpace ι<VAR>h : ProgMeasurable f u<VAR>ht : ProgMeasurable f t<VAR>ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i<VAR>i : ι<VAR>this : (fun p => u (t (↑p.1) p.2) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2)<GOAL>StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝³ : MeasurableSpace ι<VAR>t : ι → Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : BorelSpace ι<VAR>inst✝ : MetrizableSpace ι<VAR>h : ProgMeasurable f u<VAR>ht : ProgMeasurable f t<VAR>ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i<VAR>i : ι<VAR>this : (fun p => u (t (↑p.1) p.2) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2)<GOAL>StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2))
<VAR>x : ℝ<VAR>h : Irrational x<GOAL>x ≠ 1
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>hnb : log p n < b<GOAL>multiplicity p (n.choose k) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>hnb : log p n < b<VAR>this : n - k + k = n<GOAL>multiplicity p (n.choose k) = ↑(filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>hnb : log p n < b<VAR>this : n - k + k = n<GOAL>n = n - k + k
<VAR>p n k b : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>hnb : log p n < b<VAR>this : n - k + k = n<GOAL>log p (n - k + k) < b
<VAR>x✝ y✝ x y : ℝ<GOAL>x ^ 2 < y ↔ -√y < x ∧ x < √y
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>f : α → β<VAR>g : α →𝒄 β<VAR>h : f = ⇑g<GOAL>Continuous (g.copy f h)
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>f : α → β<VAR>g : α →𝒄 β<VAR>h : f = ⇑g<GOAL>Continuous g.toOrderHom
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a)
<VAR>m n : ℕ<VAR>this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r<GOAL>eulerMascheroniSeq m < eulerMascheroniSeq' n
<VAR>m n : ℕ<VAR>this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r<GOAL>eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ : P<GOAL>c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫_ℝ = dist p₁ p₂ ^ 2 / 2
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝² : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>inst✝¹ : L.NeBot<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Tendsto (fun i => μ (As i)) L (𝓝 (μ A))
<VAR>α : Type u_1<VAR>inst✝³ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝² : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>inst✝¹ : L.NeBot<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>MeasurableSet A
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Fintype I<VAR>e : I → R<VAR>he : CompleteOrthogonalIdempotents e<GOAL>∏ i : I, (1 - e i) = 0
<VAR>a b c : ℤ<VAR>hdvd : ¬3 ∣ a * b * c<GOAL>a ^ 3 + b ^ 3 ≠ c ^ 3
<VAR>a b c : ℤ<VAR>hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c<GOAL>a ^ 3 + b ^ 3 ≠ c ^ 3
<VAR>a b c : ℤ<VAR>hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c<GOAL>¬↑(a ^ 3 + b ^ 3) = ↑(c ^ 3)
<VAR>a b c : ℤ<VAR>hdvd : (¬3 ∣ a ∧ ¬3 ∣ b) ∧ ¬3 ∣ c<GOAL>¬↑a ^ 3 + ↑b ^ 3 = ↑c ^ 3
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>IsHomogeneous 𝒜 I ↔ ∃ S, I = span (Subtype.val '' S)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>I = (homogeneousCore 𝒜 I).toIdeal ↔ ∃ S, I = span (Subtype.val '' S)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring R<VAR>a b : R<VAR>h : Commute a b<GOAL>a ^ 2 - b ^ 2 = (a + b) * (a - b)