ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>AEStronglyMeasurable (↑↑(condexpIndSMul hm hs hμs x)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : InnerProductSpace 𝕜 E'<VAR>inst✝¹⁴ : CompleteSpace E'<VAR>inst✝¹³ : NormedSpace ℝ E'<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 ≠ ⊤ → ∫⁻ (x_1 : α) in s_1, ↑‖↑↑(condexpIndSMul hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>I : Type u_6<VAR>l : I → Filter α<VAR>ι : I → Sort u_7<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>S : Set I<VAR>hd : S.PairwiseDisjoint l<VAR>hS : S.Finite<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>I : Type u_6<VAR>l : I → Filter α<VAR>ι : I → Sort u_7<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>S : Set I<VAR>hd✝ : S.PairwiseDisjoint l<VAR>hS : S.Finite<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<VAR>t : I → Set α<VAR>htl : ∀ (i : I), t i ∈ l i<VAR>hd : S.PairwiseDisjoint t<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>I : Type u_6<VAR>l : I → Filter α<VAR>ι : I → Sort u_7<VAR>p : (i : I) → ι i → Prop<VAR>s : (i : I) → ι i → Set α<VAR>S : Set I<VAR>hd✝ : S.PairwiseDisjoint l<VAR>hS : S.Finite<VAR>h : ∀ (i : I), (l i).HasBasis (p i) (s i)<VAR>t : I → Set α<VAR>htl : ∀ (i : I), t i ∈ l i<VAR>hd : S.PairwiseDisjoint t<VAR>ind : (i : I) → ι i<VAR>hp : ∀ (i : I), p i (ind i)<VAR>ht : ∀ (i : I), s i (ind i) ⊆ t i<GOAL>∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j✝ : J<GOAL>(biproduct.ι (fun j => f j ⊗ X) j✝ ≫ biproduct.desc fun j => biproduct.ι f j ▷ X) = biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>a₁ a₂ : A i<GOAL>(ι' R A) ((lof R I A i) a₁) * (ι' R A) ((lof R I A i) a₂) = (ι' R A) ((lof R I A i) (a₁ * a₂))
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>a₁ a₂ : A i<GOAL>(ι' R A) ((lof R I A i) a₁) * (ι' R A) ((lof R I A i) a₂) = (RingQuot.mkAlgHom R (rel R A)) ((tprod R (⨁ (i : I), A i) 2) fun x => match x with | 0 => (lof R I A i) a₁ | 1 => (lof R I A i) a₂)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : ℕ<VAR>E : Fin n → Type u_2<VAR>inst✝¹ : (i : Fin n) → MeasureSpace (E i)<VAR>inst✝ : ∀ (i : Fin n), SigmaFinite volume<VAR>f : (i : Fin n) → E i → 𝕜<VAR>hf : ∀ (i : Fin n), Integrable (f i) volume<GOAL>Integrable (fun x => ∏ i : Fin n, f i (x i)) volume
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ≈ -x ↔ 0 ≈ x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<GOAL>Absorbent 𝕜 (p.closedBall x r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<VAR>y : E<VAR>hy : y ∈ p.closedBall 0 (r - p x)<GOAL>y ∈ p.closedBall x r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<VAR>y : E<VAR>hy : p y ≤ r - p x<GOAL>y ∈ p.closedBall x r
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : MvPolynomial σ R<VAR>n : σ →₀ ℕ<VAR>a : R<VAR>m : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R m) ↑((monomial n) a) = (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a)
<VAR>n : ℕ<VAR>m : ℝ<VAR>m1 : 1 < m<VAR>m0 : 0 < m<VAR>mi : 1 / m < 1<GOAL>∑' (i : ℕ), 1 / m ^ (i + (n + 1)!) = ∑' (i : ℕ), (1 / m) ^ i * (1 / m ^ (n + 1)!)
<VAR>n : ℕ<VAR>m : ℝ<VAR>m1 : 1 < m<VAR>m0 : 0 < m<VAR>mi : 1 / m < 1<GOAL>(∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x<VAR>c : HasDerivAt (fun x => Complex.sin (↑x * (2 * z)) / (2 * z)) (Complex.cos (↑x * (2 * z)) * (2 * z) / (2 * z)) x<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x<VAR>c : HasDerivAt (fun x => Complex.sin (↑x * (2 * z)) / (2 * z)) (Complex.cos (↑x * (2 * z))) x<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>z : ℂ<VAR>n : ℕ<VAR>hz : z ≠ 0<VAR>x : ℝ<VAR>a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x<VAR>b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x<VAR>c : HasDerivAt (fun x => Complex.sin (2 * z * ↑x) / (2 * z)) (Complex.cos (2 * z * ↑x)) x<GOAL>HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<GOAL>IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<GOAL>(∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>S : J.Cover X<GOAL>Nonempty (IsLimit (S.multifork P)) → IsIso (S.toMultiequalizer P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>X : C<VAR>S : J.Cover X<GOAL>IsIso (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))
<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>i : X ⟶ Y<VAR>f : Y ⟶ Z<VAR>inst✝ : IsIso i<VAR>S : Sieve Z<GOAL>S.arrows (i ≫ f) ↔ S.arrows f
<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>i : X ⟶ Y<VAR>f : Y ⟶ Z<VAR>inst✝ : IsIso i<VAR>S : Sieve Z<VAR>H : S.arrows (i ≫ f)<GOAL>S.arrows f
<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>i : X ⟶ Y<VAR>f : Y ⟶ Z<VAR>inst✝ : IsIso i<VAR>S : Sieve Z<VAR>H : S.arrows (i ≫ f)<GOAL>f = inv i ≫ i ≫ f
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>m n : ℤ<GOAL>(a ^ m).y < (a ^ n).y ↔ m < n
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>m n : ℤ<VAR>H : (a ^ m).y < (a ^ n).y<GOAL>m < n
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>m n : ℤ<VAR>H : n ≤ m<GOAL>(a ^ n).y ≤ (a ^ m).y
<VAR>x y : ℝ<GOAL>ContinuousOn log {0}ᶜ
<VAR>x y : ℝ<GOAL>Continuous fun x => log ↑x
<VAR>x y : ℝ<GOAL>Continuous fun x => expOrderIso.symm ⟨|↑x|, ⋯⟩
<VAR>it : Iterator<VAR>n : Nat<GOAL>it.forward n = it.nextn n
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s t : Set α<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>l : ι → Filter α<VAR>hd : Pairwise (Disjoint on l)<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s t : Set α<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>l : ι → Filter α<VAR>hd : Pairwise (Disjoint on l)<VAR>this : Pairwise fun i j => ∃ s t, Disjoint ↑s ↑t<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ : Set α<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>l : ι → Filter α<VAR>hd : Pairwise (Disjoint on l)<VAR>s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }<VAR>t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }<VAR>hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t<VAR>i : ι<GOAL>(fun i => ⋂ j, ↑s ∩ ↑t) i ∈ l i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ : Set α<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>l : ι → Filter α<VAR>hd : Pairwise (Disjoint on l)<VAR>s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }<VAR>t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }<VAR>hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>(Disjoint on fun i => ⋂ j, ↑s ∩ ↑t) i j
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>x : k<GOAL>∃ z, x = z * z
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>z : k<GOAL>∃ z_1, z ^ 2 = z_1 * z_1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<GOAL>F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorComm D a b).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : (F.commShiftIso (a + b)).hom.app X = (CommShift.isoAdd (F.commShiftIso a) (F.commShiftIso b)).hom.app X<GOAL>F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorComm D a b).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorComm D a b).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ ((shiftFunctorAdd' D a b (a + b) ⋯).symm ≪≫ shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorComm C a b).hom.app X) = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ ((shiftFunctorAdd' D a b (a + b) ⋯).inv.app (F.obj X) ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X)) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)<GOAL>F.map (((shiftFunctorAdd C a b).symm ≪≫ shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) = F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorAdd C a b).inv.app X ≫ (shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) = F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.73697, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift B<VAR>X : C<VAR>a b : B<VAR>eq : F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X = (F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)<GOAL>F.map ((shiftFunctorAdd C a b).inv.app X) ≫ F.map ((shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) = F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (F.commShiftIso (a + b)).hom.app X ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫ (shiftFunctor D a).map ((F.commShiftIso b).inv.app X) ≫ (F.commShiftIso a).inv.app ((shiftFunctor C b).obj X)
<VAR>p : Nat.Primes<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>‖↑↑p ^ (-s)‖ ≤ 1 / 2
<VAR>p : Nat.Primes<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>↑↑p ^ (-s).re ≤ 1 / 2
<VAR>p : Nat.Primes<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>2 ^ (-s).re ≤ 1 / 2
<VAR>p : Nat.Primes<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>2 ^ (-s).re ≤ 2 ^ (-1)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a✝ : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>a : AddCircle p<GOAL>∃ b ∈ Ico 0 p, ↑b = a
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a✝ : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>a : AddCircle p<VAR>b : ↑(Ico 0 (0 + p)) := (QuotientAddGroup.equivIcoMod ⋯ 0) a<GOAL>∃ b ∈ Ico 0 p, ↑b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>hs : ∀ (j : Subtype p), (s ↑j).Nonempty<VAR>j0 : Subtype p<VAR>hj0 : BddBelow (range fun i => f ↑i)<VAR>m : Set (Subtype p) := {j | BddBelow (range fun i => f ↑i)}<VAR>this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)<VAR>A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)<VAR>B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)<GOAL>liminf f v = ⨆ j, ⨅ i, f ↑i
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>W'.neg ((fun m => m • Q) u) ≈ W'.neg Q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>A B : Subalgebra R S<VAR>inst✝³ : Module.Free R ↥A<VAR>inst✝² : Module.Free R ↥B<VAR>inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)<VAR>inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)<GOAL>finrank R ↥(A ⊔ B) = finrank R ↥A * finrank ↥A ↥(Algebra.adjoin ↥A ↑B)