ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>f g : α → β<VAR>x : α<VAR>s : Finset α<VAR>hnmem : x ∉ s<VAR>ih : ∀ (comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)) (comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)) (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)), s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg<VAR>comm_ff : (↑(cons x s hnmem)).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (f y)<VAR>y : α<VAR>hy : y ∈ s<GOAL>Commute (g x) (f y)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>((μ.withDensity f).withDensity fun x => (f x)⁻¹) ≤ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>μ.withDensity (f * fun x => (f x)⁻¹) ≤ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(f * fun x => (f x)⁻¹) ≤ᶠ[ae μ] 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>x : α<GOAL>(f * fun x => (f x)⁻¹) x ≤ 1 x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>x : α<GOAL>f x * (f x)⁻¹ ≤ 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>x : α<VAR>hx_top : ¬f x = ⊤<VAR>hx_zero : ¬f x = 0<GOAL>f x * (f x)⁻¹ ≤ 1
<VAR>a b : Ordinal.{u}<GOAL>a.toPGame + b.toPGame ≈ (a ♯ b).toPGame
<VAR>a b : Ordinal.{u}<VAR>i : (a.toPGame + b.toPGame).LeftMoves<GOAL>(a.toPGame + b.toPGame).moveLeft i ⧏ (a ♯ b).toPGame
<VAR>a b : Ordinal.{u}<VAR>i : (a ♯ b).toPGame.LeftMoves<GOAL>(a ♯ b).toPGame.moveLeft i ⧏ a.toPGame + b.toPGame
<VAR>N k : ℕ<GOAL>(N.smoothNumbersUpTo k).card + (N.roughNumbersUpTo k).card = N
<VAR>N k : ℕ<GOAL>(Finset.filter (fun x => x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers) (Finset.range N.succ)).card = N
<VAR>N k : ℕ<GOAL>(Finset.filter (fun x => x ≠ 0) (Finset.range N.succ)).card = N
<VAR>N k : ℕ<GOAL>(Finset.range N.succ).card - 1 = N
<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>β✝ : Type u_7<VAR>inst✝¹ : SeminormedAddCommGroup β✝<VAR>T✝ T' : Set α → β✝<VAR>C✝ C' : ℝ<VAR>β : Type u_8<VAR>inst✝ : NormedAddCommGroup β<VAR>T : Set α → β<VAR>C : ℝ<VAR>m : MeasurableSpace α<VAR>hT : DominatedFinMeasAdditive 0 T C<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>0 s = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<GOAL>x' ∈ (chartAt H x).source
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>hA : FiniteType R A<GOAL>FiniteType S A
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>hA : FiniteType R A<VAR>s : Finset A<VAR>hS : adjoin R ↑s = ⊤<GOAL>FiniteType S A
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>hA : FiniteType R A<VAR>s : Finset A<VAR>hS : adjoin R ↑s = ⊤<VAR>b : A<GOAL>b ∈ adjoin S ↑s
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : CommSemiring S<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>hA : FiniteType R A<VAR>s : Finset A<VAR>hS : adjoin R ↑s = ⊤<VAR>b : A<VAR>le : adjoin R ↑s ≤ Subalgebra.restrictScalars R (adjoin S ↑s)<GOAL>b ∈ adjoin S ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>q : ℚ<VAR>x : ℝ<VAR>hx : x ∈ {r | ↑q ≤ r}<VAR>t : Set ℝ<VAR>ht : t ∈ 𝓝 x<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ t<VAR>p : ℚ<VAR>h₁ : x < ↑p<VAR>h₂ : ↑p < x + ε<GOAL>↑p ∈ ball x ε
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>x y l₁ u₁ : ι → ℝ<VAR>h₁ : ∀ (i : ι), l₁ i < u₁ i<VAR>l₂ u₂ : ι → ℝ<VAR>h₂ : ∀ (i : ι), l₂ i < u₂ i<VAR>h : ↑{ lower := l₁, upper := u₁, lower_lt_upper := h₁ } = ↑{ lower := l₂, upper := u₂, lower_lt_upper := h₂ }<GOAL>{ lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>x y l₁ u₁ : ι → ℝ<VAR>h₁ : ∀ (i : ι), l₁ i < u₁ i<VAR>l₂ u₂ : ι → ℝ<VAR>h₂ : ∀ (i : ι), l₂ i < u₂ i<VAR>h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁<GOAL>{ lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>x y l₁ u₁ : ι → ℝ<VAR>h₁ : ∀ (i : ι), l₁ i < u₁ i<VAR>l₂ u₂ : ι → ℝ<VAR>h₂ : ∀ (i : ι), l₂ i < u₂ i<VAR>h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁<GOAL>l₁ = l₂
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>x y l₁ u₁ : ι → ℝ<VAR>h₁ : ∀ (i : ι), l₁ i < u₁ i<VAR>l₂ u₂ : ι → ℝ<VAR>h₂ : ∀ (i : ι), l₂ i < u₂ i<VAR>h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁<GOAL>u₁ = u₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>inst✝¹ : Mono f<VAR>g : A₂ ⟶ B<VAR>inst✝ : Mono g<VAR>X : Subobject B<VAR>h₁ : mk f ≤ mk g<VAR>h₂ : mk g ≤ X<GOAL>ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X ⋯
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>inst✝¹ : Mono f<VAR>g : A₂ ⟶ B<VAR>inst✝ : Mono g<VAR>X : Subobject B<VAR>h₁ : mk f ≤ mk g<VAR>h₂ : mk g ≤ X<GOAL>(underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atTop, p x<GOAL>∀ᶠ (n : ℚ) in atTop, p ↑n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atTop, p x<GOAL>∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>hle : ‖x‖ ≤ ‖y‖<VAR>h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>hle : ‖x‖ ≤ ‖y‖<VAR>h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2<GOAL>re ⟪x - y, x - y⟫_𝕜 ≤ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>hle : ‖x‖ ≤ ‖y‖<VAR>h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2<VAR>H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2<GOAL>re ⟪x - y, x - y⟫_𝕜 ≤ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>hle : ‖x‖ ≤ ‖y‖<VAR>h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2<VAR>H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2<VAR>H₂ : re ⟪y, x⟫_𝕜 = ‖y‖ ^ 2<GOAL>re ⟪x - y, x - y⟫_𝕜 ≤ 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ ↑F).Nonempty
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>τ : Type u_9<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>inst✝¹⁸ : DecidableEq ι<VAR>inst✝¹⁷ : DecidableEq κ<VAR>inst✝¹⁶ : DecidableEq τ<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype κ<VAR>inst✝¹³ : Fintype τ<VAR>inst✝¹² : Finite ι'<VAR>inst✝¹¹ : Finite κ'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bP : Basis τ R P<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>A : Matrix ι' ι R<VAR>B : Matrix κ' κ R<GOAL>(toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (kroneckerMap (fun x x_1 => x * x_1) A B) = TensorProduct.map ((toLin bM bM') A) ((toLin bN bN') B)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a : ℕ → ℝ<VAR>n : ℕ<VAR>hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))<GOAL>∑ k ∈ Finset.range n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a : ℕ → ℝ<VAR>n : ℕ<VAR>hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))<GOAL>∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>↑(normSq x) = ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>re ↑(normSq x) = re ⟪x, x⟫_𝕜 ∧ im ↑(normSq x) = im ⟪x, x⟫_𝕜
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s : Multiset ℕ<VAR>n : ℕ<GOAL>s.prod % n = (map (fun x => x % n) s).prod % n
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I : Ideal α<GOAL>¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I : Ideal α<GOAL>(I = ⊤ ∨ ∃ x x_1, ∃ (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n m : A<VAR>h : n + m = 0<VAR>X : C<GOAL>(shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).inv.app X) = (shiftFunctorCompIsoId C m n ⋯).inv.app ((shiftFunctor C n).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n m : A<VAR>h : n + m = 0<VAR>X : C<GOAL>𝟙 ((shiftFunctor C n).obj ((𝟭 C).obj X)) = 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>H : Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ ↑(i0 ≪≫ₗ i1.symm)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>H : Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ ↑(i0 ≪≫ₗ i1.symm)<VAR>this : i = Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm<VAR>i1 : ↥M ⊗[R] ↥N ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := TensorProduct.congr m.repr n.repr<VAR>i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ ↑(i0 ≪≫ₗ i1.symm)<VAR>this : i = Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2)<VAR>H : Function.Injective ⇑(M.mulMap N)<GOAL>M.LinearDisjoint N
<VAR>x : ZFSet<GOAL>x = ∅ ↔ ∀ (y : ZFSet), y ∉ x
<VAR>x : ZFSet<GOAL>(∀ (z : ZFSet), z ∈ x ↔ z ∈ ∅) ↔ ∀ (y : ZFSet), y ∉ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I : Set β<GOAL>(M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I : Set β<GOAL>(∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I : Set β<GOAL>(∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Indep I ∧ ⇑f '' I ⊆ range ⇑f
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : Even n<GOAL>closure (range fun x => x ^ n) = nonneg ℚ
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : Even n<GOAL>(range fun x => x ^ n) = ⇑NNRat.coeHom '' range fun x => x ^ n
<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : Even n<GOAL>nonneg ℚ = map NNRat.coeHom (closure (range fun x => x ^ n))
<VAR>X✝ X : LocallyRingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toRingedSpace.toPresheafedSpace<GOAL>x ∈ ↑(X.toRingedSpace.basicOpen 0) ↔ x ∈ ↑⊥
<VAR>X✝ X : LocallyRingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toRingedSpace.toPresheafedSpace<GOAL>∀ (x_1 : x ∈ U), ¬IsUnit ((X.toRingedSpace.presheaf.germ ⟨x, ⋯⟩) 0)
<VAR>X✝ X : LocallyRingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toRingedSpace.toPresheafedSpace<VAR>hx : x ∈ U<GOAL>¬IsUnit ((X.toRingedSpace.presheaf.germ ⟨x, ⋯⟩) 0)
<VAR>X✝ X : LocallyRingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toRingedSpace.toPresheafedSpace<VAR>hx : x ∈ U<GOAL>¬0 = 1
<VAR>X✝ X : LocallyRingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toRingedSpace.toPresheafedSpace<VAR>hx : x ∈ U<GOAL>0 ≠ 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W✝ : WeierstrassCurve R<VAR>C✝ C C' : VariableChange R<VAR>W : WeierstrassCurve R<GOAL>{ a₁ := ↑(C.u * C'.u)⁻¹ * (W.a₁ + 2 * (↑C'.u * C.s + C'.s)), a₂ := ↑(C.u * C'.u)⁻¹ ^ 2 * (W.a₂ - (↑C'.u * C.s + C'.s) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) - (↑C'.u * C.s + C'.s) ^ 2), a₃ := ↑(C.u * C'.u)⁻¹ ^ 3 * (W.a₃ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₁ + 2 * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)), a₄ := ↑(C.u * C'.u)⁻¹ ^ 4 * (W.a₄ - (↑C'.u * C.s + C'.s) * W.a₃ + 2 * (C.r * ↑C'.u ^ 2 + C'.r) * W.a₂ - (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t + (C.r * ↑C'.u ^ 2 + C'.r) * (↑C'.u * C.s + C'.s)) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 - 2 * (↑C'.u * C.s + C'.s) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)), a₆ := ↑(C.u * C'.u)⁻¹ ^ 6 * (W.a₆ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₄ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 * W.a₂ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 3 - (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₃ - (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) ^ 2 - (C.r * ↑C'.u ^ 2 + C'.r) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₁) } = { a₁ := ↑C.u⁻¹ * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s) + 2 * C.s), a₂ := ↑C.u⁻¹ ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2) - C.s * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r - C.s ^ 2), a₃ := ↑C.u⁻¹ ^ 3 * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) + C.r * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 2 * C.t), a₄ := ↑C.u⁻¹ ^ 4 * (↑C'.u⁻¹ ^ 4 * (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 - 2 * C'.s * C'.t) - C.s * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) + 2 * C.r * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) - (C.t + C.r * C.s) * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r ^ 2 - 2 * C.s * C.t), a₆ := ↑C.u⁻¹ ^ 6 * (↑C'.u⁻¹ ^ 6 * (W.a₆ + C'.r * W.a₄ + C'.r ^ 2 * W.a₂ + C'.r ^ 3 - C'.t * W.a₃ - C'.t ^ 2 - C'.r * C'.t * W.a₁) + C.r * (↑C'.u⁻¹ ^ 4 * (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 - 2 * C'.s * C'.t)) + C.r ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) + C.r ^ 3 - C.t * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) - C.t ^ 2 - C.r * C.t * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s))) }
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W✝ : WeierstrassCurve R<VAR>C✝ C C' : VariableChange R<VAR>W : WeierstrassCurve R<GOAL>↑C.u⁻¹ * ↑C'.u⁻¹ * (W.a₁ + 2 * (↑C'.u * C.s + C'.s)) = ↑C.u⁻¹ * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s) + 2 * C.s)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W✝ : WeierstrassCurve R<VAR>C✝ C C' : VariableChange R<VAR>W : WeierstrassCurve R<GOAL>(↑C.u⁻¹ * ↑C'.u⁻¹) ^ 2 * (W.a₂ - (↑C'.u * C.s + C'.s) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) - (↑C'.u * C.s + C'.s) ^ 2) = ↑C.u⁻¹ ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2) - C.s * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r - C.s ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W✝ : WeierstrassCurve R<VAR>C✝ C C' : VariableChange R<VAR>W : WeierstrassCurve R<GOAL>(↑C.u⁻¹ * ↑C'.u⁻¹) ^ 3 * (W.a₃ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₁ + 2 * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) = ↑C.u⁻¹ ^ 3 * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t) + C.r * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 2 * C.t)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W✝ : WeierstrassCurve R<VAR>C✝ C C' : VariableChange R<VAR>W : WeierstrassCurve R<GOAL>(↑C.u⁻¹ * ↑C'.u⁻¹) ^ 4 * (W.a₄ - (↑C'.u * C.s + C'.s) * W.a₃ + 2 * (C.r * ↑C'.u ^ 2 + C'.r) * W.a₂ - (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t + (C.r * ↑C'.u ^ 2 + C'.r) * (↑C'.u * C.s + C'.s)) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 - 2 * (↑C'.u * C.s + C'.s) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t)) = ↑C.u⁻¹ ^ 4 * (↑C'.u⁻¹ ^ 4 * (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 - 2 * C'.s * C'.t) - C.s * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) + 2 * C.r * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) - (C.t + C.r * C.s) * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r ^ 2 - 2 * C.s * C.t)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W✝ : WeierstrassCurve R<VAR>C✝ C C' : VariableChange R<VAR>W : WeierstrassCurve R<GOAL>(↑C.u⁻¹ * ↑C'.u⁻¹) ^ 6 * (W.a₆ + (C.r * ↑C'.u ^ 2 + C'.r) * W.a₄ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 2 * W.a₂ + (C.r * ↑C'.u ^ 2 + C'.r) ^ 3 - (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₃ - (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) ^ 2 - (C.r * ↑C'.u ^ 2 + C'.r) * (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) * W.a₁) = ↑C.u⁻¹ ^ 6 * (↑C'.u⁻¹ ^ 6 * (W.a₆ + C'.r * W.a₄ + C'.r ^ 2 * W.a₂ + C'.r ^ 3 - C'.t * W.a₃ - C'.t ^ 2 - C'.r * C'.t * W.a₁) + C.r * (↑C'.u⁻¹ ^ 4 * (W.a₄ - C'.s * W.a₃ + 2 * C'.r * W.a₂ - (C'.t + C'.r * C'.s) * W.a₁ + 3 * C'.r ^ 2 - 2 * C'.s * C'.t)) + C.r ^ 2 * (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2)) + C.r ^ 3 - C.t * (↑C'.u⁻¹ ^ 3 * (W.a₃ + C'.r * W.a₁ + 2 * C'.t)) - C.t ^ 2 - C.r * C.t * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)))
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ convexBodyLT K f<GOAL>-x ∈ convexBodyLT K f
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧ ∀ (a : InfinitePlace K) (b : a.IsComplex), Complex.abs (x.2 ⟨a, b⟩) < ↑(f a)<GOAL>(∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧ ∀ (a : InfinitePlace K) (b : a.IsComplex), Complex.abs (x.2 ⟨a, b⟩) < ↑(f a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝¹⁵ : Category.{u_7, u_1} C<VAR>inst✝¹⁴ : Category.{u_6, u_2} D<VAR>inst✝¹³ : Category.{?u.101305, u_3} E<VAR>inst✝¹² : Category.{?u.101309, u_4} J<VAR>F₁ F₂ F₃ : C ⥤ D<VAR>τ : F₁ ⟶ F₂<VAR>τ' : F₂ ⟶ F₃<VAR>e : F₁ ≅ F₂<VAR>G G' : D ⥤ E<VAR>τ'' : G ⟶ G'<VAR>H : E ⥤ J<VAR>A : Type u_5<VAR>inst✝¹¹ : AddMonoid A<VAR>inst✝¹⁰ : HasShift C A<VAR>inst✝⁹ : HasShift D A<VAR>inst✝⁸ : HasShift E A<VAR>inst✝⁷ : HasShift J A<VAR>inst✝⁶ : F₁.CommShift A<VAR>inst✝⁵ : F₂.CommShift A<VAR>inst✝⁴ : F₃.CommShift A<VAR>inst✝³ : G.CommShift A<VAR>inst✝² : G'.CommShift A<VAR>inst✝¹ : H.CommShift A<VAR>inst✝ : CommShift τ A<VAR>a : A<GOAL>(F₁.commShiftIso a).hom ≫ whiskerRight τ (shiftFunctor D a) = whiskerLeft (shiftFunctor C a) τ ≫ (F₂.commShiftIso a).hom
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<VAR>d : ℝ<VAR>left✝ : d > 0<VAR>hd' : IsBigOWith d (𝓝[>] 0) f fun x => x ^ (-b)<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume