ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁸ : Category.{u_15, u_1} C₁<VAR>inst✝⁷ : Category.{u_16, u_2} C₂<VAR>inst✝⁶ : Category.{u_14, u_3} C₃<VAR>inst✝⁵ : Category.{u_11, u_4} C₄<VAR>inst✝⁴ : Category.{u_13, u_5} C₁₂<VAR>inst✝³ : Category.{?u.204416, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>j : J<VAR>A : C₄<VAR>f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>f = g
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁸ : Category.{u_15, u_1} C₁<VAR>inst✝⁷ : Category.{u_16, u_2} C₂<VAR>inst✝⁶ : Category.{u_14, u_3} C₃<VAR>inst✝⁵ : Category.{u_11, u_4} C₄<VAR>inst✝⁴ : Category.{u_13, u_5} C₁₂<VAR>inst✝³ : Category.{?u.204416, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>j : J<VAR>A : C₄<VAR>f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>∀ (i : ↑(r ⁻¹' {j})), Cofan.inj (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j) i ≫ f = Cofan.inj (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j) i ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a : α<VAR>h : filter p [a] ≠ []<VAR>h' : p ([a].getLast ⋯) = true<GOAL>(filter p [a]).getLast h = [a].getLast ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a : α<VAR>h : filter p [a] ≠ []<VAR>h' : p a = true<GOAL>(filter p [a]).getLast h = [a].getLast ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a b : α<VAR>as : List α<VAR>h : filter p (a :: b :: as) ≠ []<VAR>h' : p ((a :: b :: as).getLast ⋯) = true<GOAL>(filter p (a :: b :: as)).getLast h = (a :: b :: as).getLast ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a b : α<VAR>as : List α<VAR>h : filter p (a :: b :: as) ≠ []<VAR>h' : p ((b :: as).getLast ⋯) = true<GOAL>(filter p (a :: b :: as)).getLast h = (b :: as).getLast ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a b : α<VAR>as : List α<VAR>h✝ : filter p (a :: b :: as) ≠ []<VAR>h' : p ((b :: as).getLast ⋯) = true<VAR>h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []<GOAL>(if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a b : α<VAR>as : List α<VAR>h✝ : filter p (a :: b :: as) ≠ []<VAR>h' : p ((b :: as).getLast ⋯) = true<VAR>h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []<VAR>ha : p a = true<GOAL>(if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>a b : α<VAR>as : List α<VAR>h✝ : filter p (a :: b :: as) ≠ []<VAR>h' : p ((b :: as).getLast ⋯) = true<VAR>h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []<VAR>ha : p a = false<GOAL>(if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
<VAR>x y : ℂ<GOAL>cos x ^ 2 + sin x ^ 2 = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hg : f =ᶠ[𝓝 x] g<VAR>r₁ : ℝ≥0∞<VAR>h₁ : HasFPowerSeriesOnBall f p x r₁<GOAL>HasFPowerSeriesAt g p x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hg : f =ᶠ[𝓝 x] g<VAR>r₁ : ℝ≥0∞<VAR>h₁ : HasFPowerSeriesOnBall f p x r₁<VAR>r₂ : ℝ≥0∞<VAR>h₂pos : r₂ > 0<VAR>h₂ : EMetric.ball x r₂ ⊆ {x | (fun x => f x = g x) x}<GOAL>HasFPowerSeriesAt g p x
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k x : ℕ<GOAL>x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k x : ℕ<GOAL>(∃ x_1, (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k x : ℕ<GOAL>(∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k x : ℕ<GOAL>∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ↥(Lp E p 0)<GOAL>‖f‖ = 0
<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>𝕜 : Type u_5<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>f : α →ₘ[μ] β<VAR>_f : α → β<VAR>hfm : AEStronglyMeasurable _f μ<VAR>hfi : (mk _f hfm).Integrable<GOAL>MeasureTheory.Integrable ((fun x => c • x) ∘ ↑⟨_f, hfm⟩) μ
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>v : Fin2 2 → ℕ<GOAL>v &0 = v &1 ↔ (Poly.proj &0 - Poly.proj &1) v = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>s : Set α<VAR>m : ι → OuterMeasure α<GOAL>(restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>s : Set α<VAR>m : ι → OuterMeasure α<VAR>this : Nonempty ↑I<GOAL>(restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (restrict s) (m i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Nonempty<VAR>s : Set α<VAR>m : ι → OuterMeasure α<VAR>this : Nonempty ↑I<GOAL>(restrict s) (⨅ i, m ↑i) = ⨅ i, (restrict s) (m ↑i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<GOAL>Even (-2)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁.length < l₂.length<VAR>l : List α<VAR>p : l ~ l₁<VAR>s : l <+ l₂<GOAL>∃ a, a :: l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁.length < l₂.length<VAR>l : List α<VAR>p : l ~ l₁<VAR>s : l <+ l₂<GOAL>l.length < l₂.length → ∃ a, a :: l <+~ l₂
<VAR>α : Type u_1<VAR>l₂ l : List α<VAR>s : l <+ l₂<GOAL>l.length < l₂.length → ∃ a, a :: l <+~ l₂
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<GOAL>UniformContinuousOn f univ ↔ UniformContinuous f
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>inst✝¹ : CompleteLinearOrder δ<VAR>inst✝ : ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>inst✝¹ : CompleteLinearOrder δ<VAR>inst✝ : ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') univ x
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>inst✝¹ : CompleteLinearOrder δ<VAR>inst✝ : ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove (range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') univ x
<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>p₂ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
<VAR>a b : ℝ<VAR>n : ℕ<VAR>this : ∫ (x : ℝ) in a..b, sin x ^ 0 * cos x ^ (2 * 1 + 1) = ∫ (u : ℝ) in sin a..sin b, u ^ 0 * (1 - u ^ 2) ^ 1<GOAL>∫ (x : ℝ) in a..b, cos x ^ 3 = sin b - sin a - (sin b ^ 3 - sin a ^ 3) / 3
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<GOAL>IsCompact ↑(basicOpen f)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<GOAL>IsCompact (Set.range ⇑(comap (algebraMap R (Localization (Submonoid.powers f)))))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>x : L<GOAL>x ∈ dual A K I ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>x : L<GOAL>x ∈ ⟨(↑I)ᵛ, ⋯⟩ ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h₁ : SurjOn f s₁ t₁<VAR>h₂ : SurjOn f s₂ t₂<VAR>h : InjOn f (s₁ ∪ s₂)<VAR>y : β<VAR>hy : y ∈ t₁ ∩ t₂<GOAL>y ∈ f '' (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h₁ : SurjOn f s₁ t₁<VAR>h₂ : SurjOn f s₂ t₂<VAR>h : InjOn f (s₁ ∪ s₂)<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ s₁<VAR>hy : f x₁ ∈ t₁ ∩ t₂<GOAL>f x₁ ∈ f '' (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h₁ : SurjOn f s₁ t₁<VAR>h₂ : SurjOn f s₂ t₂<VAR>h : InjOn f (s₁ ∪ s₂)<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ s₁<VAR>hy : f x₁ ∈ t₁ ∩ t₂<VAR>x₂ : α<VAR>hx₂ : x₂ ∈ s₂<VAR>heq : f x₂ = f x₁<GOAL>f x₁ ∈ f '' (s₁ ∩ s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h₁ : SurjOn f s₁ t₁<VAR>h₂ : SurjOn f s₂ t₂<VAR>h : InjOn f (s₁ ∪ s₂)<VAR>x₁ : α<VAR>hx₁ : x₁ ∈ s₁<VAR>hy : f x₁ ∈ t₁ ∩ t₂<VAR>hx₂ : x₁ ∈ s₂<VAR>heq : f x₁ = f x₁<GOAL>f x₁ ∈ f '' (s₁ ∩ s₂)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝² : (i : ι) → Module R (M₁' i)<VAR>α : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s : Set ι<VAR>inst✝ : DecidableEq { x // x ∈ s }<VAR>e : α ≃ ↑s<VAR>m : α → (i : ι) → M₁ i<VAR>a : α<VAR>z : (i : ι) → M₁ i<VAR>i : ↑s<GOAL>update m a z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝² : (i : ι) → Module R (M₁' i)<VAR>α : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s : Set ι<VAR>inst✝ : DecidableEq { x // x ∈ s }<VAR>e : α ≃ ↑s<VAR>m : α → (i : ι) → M₁ i<VAR>z : (i : ι) → M₁ i<VAR>i : ↑s<GOAL>update m (e.symm i) z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e (e.symm i)) (z ↑(e (e.symm i))) i
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝² : (i : ι) → Module R (M₁' i)<VAR>α : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s : Set ι<VAR>inst✝ : DecidableEq { x // x ∈ s }<VAR>e : α ≃ ↑s<VAR>m : α → (i : ι) → M₁ i<VAR>a : α<VAR>z : (i : ι) → M₁ i<VAR>i : ↑s<VAR>hne : a ≠ e.symm i<GOAL>update m a z (e.symm i) ↑i = update (fun j => m (e.symm j) ↑j) (e a) (z ↑(e a)) i
<VAR>m n : ℕ<VAR>x y : ZMod n<GOAL>(x + y).cast = (x.cast + y.cast) % ↑n
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s t : 𝕜 → 𝕜<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>ht : MeromorphicOn t U<VAR>hf : MeromorphicOn f U<VAR>hg : MeromorphicOn g U<VAR>h : MeromorphicOn (-f) U<GOAL>MeromorphicOn f U
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>‖equivRealProd z‖ ≤ abs z
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p : R[X]<VAR>x : R<GOAL>(aeval h.root) (C x) = h.map (C x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p✝ p q : R[X]<VAR>ihp : (aeval h.root) p = h.map p<VAR>ihq : (aeval h.root) q = h.map q<GOAL>(aeval h.root) (p + q) = h.map (p + q)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p : R[X]<VAR>n : ℕ<VAR>x : R<VAR>x✝ : (aeval h.root) (C x * X ^ n) = h.map (C x * X ^ n)<GOAL>(aeval h.root) (C x * X ^ (n + 1)) = h.map (C x * X ^ (n + 1))
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<GOAL>a * ⅟b * b = a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁴ : CommRing R₂<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v✝ : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>v : ι → M<VAR>i✝ j✝ : ι<GOAL>e.toMatrix v i✝ j✝ = (LinearMap.toMatrix e e) ((e.constr ℕ) v) i✝ j✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.11305, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(F.map f ⊗ (F.closedIhom.obj G).map f) ≫ (ihom.ev (F.obj Y)).app (G.obj Y) = (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.11305, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(F.map f ⊗ (ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y)) ≫ (ihom.ev (F.obj Y)).app (G.obj Y) = (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.11305, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(F.map f ▷ (ihom (F.obj X)).obj (G.obj X) ≫ F.obj Y ◁ ((ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y))) ≫ (ihom.ev (F.obj Y)).app (G.obj Y) = (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<GOAL>Module.rank F ↥⊥ = 1
<VAR>a x z✝ z : ℂ<GOAL>z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
<VAR>m k : ℕ+<GOAL>(k.modDivAux (↑m % ↑k) (↑m / ↑k)).2 = if ↑m % ↑k = 0 then ↑m / ↑k - 1 else ↑m / ↑k
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>inst✝¹ : Bifunctor F<VAR>inst✝ : LawfulBifunctor F<VAR>α₀ α₁ α₂ : Type u₀<VAR>β : Type u₁<VAR>f : α₀ → α₁<VAR>f' : α₁ → α₂<VAR>x : F α₀ β<GOAL>fst f' (fst f x) = fst (f' ∘ f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r✝ : α → β → Prop<VAR>f : α → γ<VAR>g : β → δ<VAR>c : γ<VAR>d : δ<VAR>r : α → β → Prop<VAR>f₁ : α → γ<VAR>g₁ : β → δ<VAR>f₂ : γ → ε<VAR>g₂ : δ → ζ<VAR>a : ε<VAR>b : ζ<GOAL>Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ a b ↔ Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r✝ : α → β → Prop<VAR>f : α → γ<VAR>g : β → δ<VAR>c : γ<VAR>d : δ<VAR>r : α → β → Prop<VAR>f₁ : α → γ<VAR>g₁ : β → δ<VAR>f₂ : γ → ε<VAR>g₂ : δ → ζ<VAR>a : ε<VAR>b : ζ<GOAL>(∃ b_1 b_2 b_3 a_1, (r b_1 b_2 ∧ f₁ b_1 = b_3 ∧ g₁ b_2 = a_1) ∧ f₂ b_3 = a ∧ g₂ a_1 = b) ↔ ∃ a_1 b_1, r a_1 b_1 ∧ f₂ (f₁ a_1) = a ∧ g₂ (g₁ b_1) = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r✝ : α → β → Prop<VAR>f : α → γ<VAR>g : β → δ<VAR>c : γ<VAR>d : δ<VAR>r : α → β → Prop<VAR>f₁ : α → γ<VAR>g₁ : β → δ<VAR>f₂ : γ → ε<VAR>g₂ : δ → ζ<VAR>a✝ : ε<VAR>b✝ : ζ<VAR>a : α<VAR>b : β<GOAL>(∃ b_1 a_1, (r a b ∧ f₁ a = b_1 ∧ g₁ b = a_1) ∧ f₂ b_1 = a✝ ∧ g₂ a_1 = b✝) → r a b ∧ f₂ (f₁ a) = a✝ ∧ g₂ (g₁ b) = b✝
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalSemiring R<VAR>u : (PreQuasiregular R)ˣ<GOAL>(↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0
<VAR>α : Type u_1<VAR>t : Set α<VAR>p : Set α → Prop<GOAL>(∀ (s : Set ↑t), p (val '' s)) ↔ ∀ s ⊆ t, p s
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<GOAL>(A.updateColumn j fun k => ∑ i : n, c i • A k i).det = c j • A.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<GOAL>(Aᵀ.updateRow j fun k => ∑ i : n, c i • A k i).det = c j • Aᵀ.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<VAR>x✝ : n<GOAL>∑ i : n, c i • A x✝ i = (∑ k : n, c k • Aᵀ k) x✝
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a * b = 1<GOAL>a = b⁻¹
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a * b = 1<GOAL>b ≠ ⊤
<VAR>a c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a * ⊤ = 1<GOAL>False
<VAR>x x₁✝ x₂✝ x₃ x' y₁ y₂ y₃ y'✝ x₁ x₂ y' : PGame<VAR>h₁ : x₁.IsOption x<VAR>h₂ : x₂.IsOption x<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y') → P124 a<GOAL>ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y')
<VAR>x x₁✝ x₂✝ x₃ x' y y₁ y₂ y₃ y'✝ : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>x₁ x₂ y' : PGame<VAR>h₁ : x₁.IsOption x<VAR>h₂ : x₂.IsOption x<VAR>hy : y'.IsOption y<GOAL>ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y)
<VAR>x x₁✝ x₂✝ x₃ x' y y₁ y₂ y₃ y'✝ : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<VAR>x₁ x₂ y' : PGame<VAR>h₁ : x₁.IsOption x<VAR>h₂ : x₂.IsOption x<VAR>hy : y'.IsOption y<GOAL>TransGen (CutExpand IsOption) (Args.P24 x₁ x₂ y').toMultiset {x, y'}