ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s✝ t u : Finset α<VAR>a b : α<VAR>inst✝ : Fintype α<VAR>s : Finset α<GOAL>IsInitSeg (initSeg s) s.card ∧ (initSeg s).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set (X × Y)<VAR>hs : IsClosed s<GOAL>IsClosed (Prod.swap '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set (X × Y)<VAR>hs : IsClosed s<GOAL>IsClosed (Prod.swap ⁻¹' s)
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>s : Ordinal.{u}<VAR>hs : s ∈ S<GOAL>enumOrd S (sSup {a | enumOrd S a ≤ s}) = s
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>s : Ordinal.{u}<VAR>hs : s ∈ S<GOAL>enumOrd S (sSup {a | enumOrd S a ≤ s}) ≤ s
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>s : Ordinal.{u}<VAR>hs : s ∈ S<GOAL>s ≤ enumOrd S (sSup {a | enumOrd S a ≤ s})
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α ≃ᵐ δ<VAR>g : δ → β<GOAL>Integrable g (Measure.map (⇑f) μ) ↔ Integrable (g ∘ ⇑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α ≃ᵐ δ<VAR>g : δ → β<GOAL>Memℒp g 1 (Measure.map (⇑f) μ) ↔ Memℒp (g ∘ ⇑f) 1 μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → F<VAR>inst✝ : NormedAddCommGroup F<VAR>hm : m ≤ mΩ<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → F<VAR>inst✝ : NormedAddCommGroup F<VAR>hm : m ≤ mΩ<VAR>hf : Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, ω)) μ)<GOAL>Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a : α<VAR>h : _root_.Disjoint s {a}<GOAL>s.disjUnion {a} h = cons a s ⋯
<VAR>m n : ℤ<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ m * n<GOAL>↑p ∣ m ∨ ↑p ∣ n
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>v : ℤ<GOAL>↑(filter (fun x => x ≡ v [ZMOD r]) (Ico a b)).card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x✝ : G<GOAL>x✝ ∈ upperCentralSeriesStep H ↔ x✝ ∈ comap (mk' H) (center (G ⧸ H))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x✝ : G<GOAL>x✝ ∈ upperCentralSeriesStep H ↔ ∀ (x : G), ↑x * (mk' H) x✝ = (mk' H) x✝ * ↑x
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x✝ : G<GOAL>∀ (a : G), x✝ * a * x✝⁻¹ * a⁻¹ ∈ H ↔ ↑a * (mk' H) x✝ = (mk' H) x✝ * ↑a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x✝ y : G<GOAL>x✝ * y * x✝⁻¹ * y⁻¹ ∈ H ↔ ↑y * (mk' H) x✝ = (mk' H) x✝ * ↑y
<VAR>f : Char → Bool<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>x✝.all f = x✝.toString.data.all f
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ range n.succ, ↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) / (↑(k, n - k).2 + 1) * bernoulli' (k, n - k).1 = ∑ k ∈ range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n x : ℕ<VAR>hx : x ∈ range n.succ<GOAL>↑(((x, n - x).1 + (x, n - x).2).choose (x, n - x).2) / (↑(x, n - x).2 + 1) * bernoulli' (x, n - x).1 = ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x
<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<GOAL>∫ (x : E), ↑f x ∂μ ≤ (μ (closedBall c f.rOut)).toReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<GOAL>s.bind pure = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<GOAL>IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<GOAL>s.bind pure = s ∨ ∃ s_1, s.bind pure = s_1.bind pure ∧ s = s_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>t : Finset α<VAR>ht : t ∈ 𝒜<VAR>ha : a ∉ t<VAR>hu : insert a t ∈ 𝒜<GOAL>collapse 𝒜 a f t = f t + f (insert a t)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S✝ R✝ : Sieve X<VAR>S : Presieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y<VAR>f : Y ⟶ X<VAR>h : S f<GOAL>R h ≤ pullback f (bind S R)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S✝ R✝ : Sieve X<VAR>S : Presieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y<VAR>f : Y ⟶ X<VAR>h : S f<GOAL>pushforward f (R h) ≤ bind S R
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s✝ : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>s : Set M<VAR>a : M<VAR>h : a ∈ Closure s<GOAL>∃ l, (∀ x ∈ l, x ∈ s) ∧ l.prod = a
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<GOAL>‖f z‖ ≤ c / r * ‖z‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<VAR>norm_f_z₁ : ‖f z₁‖ ≤ c<GOAL>‖f z‖ ≤ c / r * ‖z‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<VAR>norm_f_z₁ : ‖f z₁‖ ≤ c<VAR>r_ne_zero : ↑r ≠ 0<GOAL>‖f z‖ ≤ c / r * ‖z‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<VAR>norm_f_z₁ : ‖f z₁‖ ≤ c<VAR>r_ne_zero : ↑r ≠ 0<VAR>eq : f z = ↑‖z‖ / ↑r * f z₁<GOAL>‖f z‖ ≤ c / r * ‖z‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<VAR>norm_f_z₁ : ‖f z₁‖ ≤ c<VAR>r_ne_zero : ↑r ≠ 0<VAR>eq : f z = ↑‖z‖ / ↑r * f z₁<GOAL>‖f z₁‖ * ‖z‖ / r ≤ c * ‖z‖ / r
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<VAR>norm_f_z₁ : ‖f z₁‖ ≤ c<VAR>r_ne_zero : ↑r ≠ 0<VAR>eq : f z = ↑‖z‖ / ↑r * f z₁<GOAL>0 ≤ c * ‖z‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<VAR>z_zero : ¬z = 0<VAR>z₁ : E := (↑r * (↑‖z‖)⁻¹) • z<VAR>hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z<VAR>norm_f_z₁ : ‖f z₁‖ ≤ c<VAR>r_ne_zero : ↑r ≠ 0<VAR>eq : f z = ↑‖z‖ / ↑r * f z₁<GOAL>‖f z₁‖ * ‖z‖ ≤ c * ‖z‖
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))<VAR>heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))<VAR>heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a<GOAL>∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>g✝ g : Ω → ℝ<VAR>ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))<VAR>heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a<VAR>x : Ω<VAR>hxeq : ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) x = (μ[g|↑ℱ i]) x<VAR>hxt : Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))<GOAL>Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
<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>s : Set α<VAR>t : Set β<GOAL>(Prod.mk '' s).seq t = ((fun b a => (a, b)) '' t).seq s
<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>s : Set α<VAR>t : Set β<GOAL>((fun x => Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a => (a, b)) '' t).seq s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h₁ : 0 < a<VAR>h₂ : 0 < b<GOAL>0 < a * b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>γ : Type<VAR>γtop : TopologicalSpace γ<VAR>γpolish : PolishSpace γ<VAR>g : γ → α<VAR>g_cont : Continuous g<VAR>gs : range g = s<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>γ : Type<VAR>γtop : TopologicalSpace γ<VAR>γpolish : PolishSpace γ<VAR>g : γ → α<VAR>g_cont : Continuous g<VAR>gs : range g = s<VAR>this : f '' s = range (f ∘ g)<GOAL>AnalyticSet (f '' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>γ : Type<VAR>γtop : TopologicalSpace γ<VAR>γpolish : PolishSpace γ<VAR>g : γ → α<VAR>g_cont : Continuous g<VAR>gs : range g = s<VAR>this : f '' s = range (f ∘ g)<GOAL>AnalyticSet (range (f ∘ g))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>γ : Type<VAR>γtop : TopologicalSpace γ<VAR>γpolish : PolishSpace γ<VAR>g : γ → α<VAR>g_cont : Continuous g<VAR>gs : range g = s<VAR>this : f '' s = range (f ∘ g)<GOAL>Continuous (f ∘ g)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>γ : Type<VAR>γtop : TopologicalSpace γ<VAR>γpolish : PolishSpace γ<VAR>g : γ → α<VAR>g_cont : Continuous g<VAR>gs : range g = s<VAR>this : f '' s = range (f ∘ g)<GOAL>∀ (x : γ), g x ∈ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_3<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>hs : AnalyticSet s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>γ : Type<VAR>γtop : TopologicalSpace γ<VAR>γpolish : PolishSpace γ<VAR>g : γ → α<VAR>g_cont : Continuous g<VAR>gs : range g = s<VAR>this : f '' s = range (f ∘ g)<GOAL>∀ (x : γ), g x ∈ range g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ f₃ : L.obj X ⟶ L.obj Y<GOAL>add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ f₃ : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₃ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>h₃ : f₃ = α.thd.map L ⋯<GOAL>add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ f₃ : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₃ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>h₃ : f₃ = α.thd.map L ⋯<GOAL>(LeftFraction₂.mk (α.f + α.f') α.f'' α.s ⋯).add.map L ⋯ = (LeftFraction₂.mk α.f (α.f' + α.f'') α.s ⋯).add.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ f₃ : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction₃ X Y<VAR>h₁ : f₁ = α.fst.map L ⋯<VAR>h₂ : f₂ = α.snd.map L ⋯<VAR>h₃ : f₃ = α.thd.map L ⋯<GOAL>(LeftFraction.mk (α.f + α.f' + α.f'') α.s ⋯).map L ⋯ = (LeftFraction.mk (α.f + (α.f' + α.f'')) α.s ⋯).map L ⋯
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<GOAL>IsSheafFor P ⊤.arrows
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<GOAL>IsSheafFor P (generate (singleton (𝟙 X))).arrows
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<GOAL>IsSheafFor P (singleton (𝟙 X))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : RBSet α cmp<VAR>H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x<GOAL>t.ModifyWF cut f
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : RBSet α cmp<VAR>H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x<GOAL>OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : RBSet α cmp<GOAL>(∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x) → OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>cut : α → Ordering<VAR>f : α → α<VAR>t : RBSet α cmp<GOAL>(∀ {x : α}, (zoom cut t.val).fst.root? = some x → cmpEq cmp (f x) x) → OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val).fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a : α<VAR>z : Sym2 α<VAR>hd : ¬z.IsDiag<VAR>h : a ∈ z<GOAL>Mem.other h ≠ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<VAR>hd : Mem.other h = a<GOAL>z.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<VAR>hd : Mem.other h = a<VAR>h' : s(a, Mem.other h) = z<GOAL>z.IsDiag
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<VAR>this : CompleteSpace E<GOAL>⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<VAR>this✝ : CompleteSpace E<VAR>this : CompleteSpace F<GOAL>⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<VAR>this✝ : CompleteSpace E<VAR>this : CompleteSpace F<GOAL>⟪↑(ContinuousLinearMap.adjoint (toContinuousLinearMap ↑(toContinuousLinearMap A))) y, x⟫_𝕜 = ⟪y, ↑(toContinuousLinearMap A) x⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.toENNRealVectorMeasure.ennrealToMeasure s = μ s
<VAR>θ : Angle<GOAL>(θ + ↑π).tan = θ.tan
<VAR>x✝ : ℝ<GOAL>(↑x✝ + ↑π).tan = (↑x✝).tan
<VAR>x✝ : ℝ<GOAL>Real.tan (x✝ + π) = Real.tan x✝
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : InjectiveResolution X<VAR>Q : InjectiveResolution Y<VAR>φ : P.cocomplex ⟶ Q.cocomplex<VAR>comm : P.ι.f 0 ≫ φ.f 0 = f ≫ Q.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.map f ≫ Q.toRightDerivedZero' F = P.toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hab : a ≤ b<VAR>hb : b ≠ 0<VAR>hcd : c < d<VAR>hd : d ≠ 0<VAR>ha : a = 0<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hab : a ≤ b<VAR>hb : b ≠ 0<VAR>hcd : c < d<VAR>hd : d ≠ 0<VAR>ha : a = 0<GOAL>b * d ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hab : a ≤ b<VAR>hb : b ≠ 0<VAR>hcd : c < d<VAR>hd : d ≠ 0<VAR>ha : ¬a = 0<VAR>hc : c = 0<GOAL>a * c < b * d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hab : a ≤ b<VAR>hb : b ≠ 0<VAR>hcd : c < d<VAR>hd : d ≠ 0<VAR>ha : ¬a = 0<VAR>hc : c = 0<GOAL>b * d ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : GCDMonoid R[X]<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t
<VAR>t : ℝ<GOAL>t ∈ I ↔ 1 - t ∈ I
<VAR>t : ℝ<GOAL>0 ≤ t ∧ t ≤ 1 ↔ 0 ≤ 1 - t ∧ 1 - t ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : R[X][Y]<GOAL>(map W f) ((mk W) x) = (mk (WeierstrassCurve.map W f)) (Polynomial.map (mapRingHom f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : R[X][Y]<GOAL>eval₂ (AdjoinRoot.of (WeierstrassCurve.map W f).toAffine.polynomial) (AdjoinRoot.root (WeierstrassCurve.map W f).toAffine.polynomial) (Polynomial.map (mapRingHom f) x) = (mk (WeierstrassCurve.map W f)) (Polynomial.map (mapRingHom f) x)
<VAR>x✝ y x : ℝ<GOAL>tan (arccos x) = √(1 - x ^ 2) / x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : DivisionSemiring α<VAR>h : Periodic f c<VAR>a : α<GOAL>Periodic (fun x => f (x * a)) (c / a)
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>s t : Set α<VAR>a✝ b✝ c : α<VAR>h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : Disjoint a b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>s t : Set α<VAR>a✝ b✝ c : α<VAR>h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : Disjoint a b<VAR>this : a = b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>s t : Set α<VAR>a✝ b✝ c : α<VAR>h : (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : b = ⊥<VAR>this : a = b<GOAL>False