ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a p q : ℤ<VAR>hpq : p + n = q<GOAL>(γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Encodable α<VAR>inst✝ : Encodable β<VAR>n : ℕ<GOAL>decode n = (decode (unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (unpair n).2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Encodable α<VAR>inst✝ : Encodable β<VAR>n : ℕ<GOAL>Option.map (⇑(Equiv.sigmaEquivProd α β)) ((decode (unpair n).1).bind fun a => Option.map (Sigma.mk a) (decode (unpair n).2)) = (decode (unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (unpair n).2)
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f'✝ : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>g : γ → δ<VAR>f' : α' → β' → δ<VAR>g₁ : α → α'<VAR>g₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)<GOAL>g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)
<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>S : Set X<VAR>x : ↑S<GOAL>(𝓝[≠] x).NeBot ↔ (𝓝[≠] ↑x ⊓ 𝓟 S).NeBot
<VAR>l : Filter ℂ<VAR>hre : Tendsto re l atTop<VAR>him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => |z.im|<GOAL>im =O[l] fun z => z.re ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s.toFinset ⊆ t.toFinset ↔ s ⊆ t
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U V : X.Opens<VAR>W : (↑U).Opens<VAR>e : W ≤ U.ι ⁻¹ᵁ V<GOAL>Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U V : X.Opens<VAR>W : (↑U).Opens<VAR>e : W ≤ U.ι ⁻¹ᵁ V<GOAL>X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = X.presheaf.map (homOfLE ⋯).op
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Finite ι<VAR>f : ι → Set X<GOAL>interior (⋂ i, f i) = ⋂ i, interior (f i)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>hpq : p ∣ q<VAR>hq : q ≠ 0<GOAL>Function.Surjective ⇑(restrictDvd hpq)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a \ c ≤ a \ b ⊔ b \ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a \ (a \ b) ≤ c ⊔ b \ c
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : Multiset (MvPolynomial σ R)<GOAL>s.prod.totalDegree ≤ (Multiset.map totalDegree s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : Multiset (MvPolynomial σ R)<VAR>l : List (MvPolynomial σ R)<GOAL>(Multiset.prod ⟦l⟧).totalDegree ≤ (Multiset.map totalDegree ⟦l⟧).sum
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : Multiset (MvPolynomial σ R)<VAR>l : List (MvPolynomial σ R)<GOAL>l.prod.totalDegree ≤ (List.map totalDegree l).sum
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq M<VAR>i : ι<VAR>bi : M<VAR>hbi : bi ∈ Finset.image (⇑b) Finset.univ<GOAL>(b.reindexFinsetRange.repr (b i)) ⟨bi, hbi⟩ = (Finsupp.single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq M<VAR>i : ι<VAR>bi : M<VAR>hbi : bi ∈ Finset.image (⇑b) Finset.univ<GOAL>(Finsupp.single ⟨b i, ⋯⟩ 1) (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨bi, hbi⟩) = (Finsupp.single ⟨b i, ⋯⟩ 1) ⟨bi, hbi⟩
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>⨆ x, ‖f x‖ = ↑(⨆ x, ‖f x‖₊)
<VAR>S : ShortComplex Ab<GOAL>S.Exact ↔ AddMonoidHom.range S.f = AddMonoidHom.ker S.g
<VAR>S : ShortComplex Ab<GOAL>AddMonoidHom.ker S.g ≤ AddMonoidHom.range S.f ↔ AddMonoidHom.range S.f = AddMonoidHom.ker S.g
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>F' : α → E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀<GOAL>Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>F' : α → E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀<VAR>hm : AEStronglyMeasurable (⇑L ∘ F') μ<GOAL>Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>F' : α → E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀<VAR>hm : AEStronglyMeasurable (⇑L ∘ F') μ<VAR>hF'_int : Integrable (⇑L ∘ F') μ<VAR>key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀<GOAL>Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>F' : α → E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀<VAR>hm : AEStronglyMeasurable (⇑L ∘ F') μ<VAR>key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀<VAR>hF'_int : Integrable F' μ<VAR>hE : CompleteSpace E<GOAL>HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>F' : α → E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>hF'_meas : AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<VAR>bound_integrable : Integrable bound μ<VAR>L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (L (F' a)) x₀<VAR>hm : AEStronglyMeasurable (⇑L ∘ F') μ<VAR>key : HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀<VAR>hF'_int : Integrable F' μ<VAR>hE : CompleteSpace E<GOAL>HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (ContinuousLinearMap.smulRight 1 (∫ (a : α), F' a ∂μ)) x₀
<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 : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<GOAL>((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) = (f fun x_1 => x) fun x => y
<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 : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<GOAL>((f fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => s.piecewise (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = (f fun x_1 => x) fun x => y
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : Fin c.length<VAR>j : Fin (c.blocksFun i)<GOAL>↑(c.invEmbedding ((c.embedding i) j)) = ↑j
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a b : R<VAR>hab : a ≤ b<VAR>c : R<GOAL>c * a * star c ≤ c * b * star c
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.542637<VAR>Bₘ : Type ?u.542640<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intNorm A B) x) = (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.542637<VAR>Bₘ : Type ?u.542640<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intNorm A B) x) = (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.542637<VAR>Bₘ : Type ?u.542640<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intNorm A B) x) = (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝ : Lattice α<VAR>s t : Interval α<GOAL>Disjoint ↑s ↑t ↔ Disjoint s t
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<VAR>x : ↥(p ⊔ p')<VAR>hx : ↑x ∈ p<GOAL>Submodule.Quotient.mk x = (quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk ⟨↑x, hx⟩)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<GOAL>X.roots = {0}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddGroup E<VAR>inst✝ : TopologicalSpace α<VAR>f : α → E<VAR>hf : Continuous f<VAR>h : HasCompactSupport f<GOAL>∃ C, ∀ (x : α), ‖f x‖ ≤ C
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>s : ↥S<VAR>m : M<GOAL>LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s
<VAR>x✝ y✝ : ℝ<VAR>x y : ℚ<GOAL>↑x < ↑y ↔ x < y
<VAR>x✝ y✝ : ℝ<VAR>x y : ℚ<GOAL>const abs ↑x < const abs ↑y ↔ x < y
<VAR>θ : Angle<GOAL>2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>r s t : Set (α × α)<VAR>a b : α<GOAL>(a, b) ∈ r ○ s ○ t ↔ (a, b) ∈ r ○ (s ○ t)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>r s t : Set (α × α)<VAR>a b : α<GOAL>(∃ z, (∃ z_1, (a, z_1) ∈ r ∧ (z_1, z) ∈ s) ∧ (z, b) ∈ t) ↔ ∃ z, (a, z) ∈ r ∧ ∃ z_1, (z, z_1) ∈ s ∧ (z_1, b) ∈ t
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.204908, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 2<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<GOAL>2 < 2 + 1
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝⁴ : LinearOrderedField K<VAR>inst✝³ : FloorRing K<VAR>inst✝² : Archimedean K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : OrderTopology K<GOAL>Filter.Tendsto (of v).convs Filter.atTop (𝓝 v)
<VAR>K : Type u<VAR>inst✝ : Field K<GOAL>intDegree 1 = 0
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<GOAL>(mapRingHom f) X = X
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>hx : x ≠ 0<GOAL>addValuation x = ↑x.valuation
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>s : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<GOAL>BddBelow s → s.WellFoundedOn fun x x_1 => x < x_1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>s : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<GOAL>BddBelow s → ∀ (f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1), ¬∀ (n : ℕ), f n ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>s : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>s : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>(range ⇑f).Finite
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<GOAL>↑g 1 0 = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1<GOAL>↑g 1 0 = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>hp : ∀ {g' : SL(2, ℤ)}, g' • z ∈ 𝒟ᵒ → ↑g' 1 0 ≠ 1<VAR>hn : ↑g 1 0 ≠ -1<GOAL>↑g 1 0 = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>hn : ↑g 1 0 ≠ -1<VAR>hp : ↑g 1 0 ≠ 1<GOAL>↑g 1 0 = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>closure (s ∪ t) = closure s ∪ closure t
<GOAL>∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
<VAR>x : ℝ<VAR>x_pos : 0 < x<VAR>hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)<GOAL>∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
<VAR>x : ℝ<VAR>x_pos : 0 < x<VAR>hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)<VAR>hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))<GOAL>∃ a, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
<VAR>x : ℝ<VAR>x_pos : 0 < x<VAR>hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)<VAR>hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))<GOAL>Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
<VAR>x : ℝ<VAR>x_pos : 0 < x<VAR>hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)<VAR>hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))<GOAL>Tendsto (fun n => stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℤ<VAR>X✝ Y✝ : HomologicalComplex C (ComplexShape.up ℤ)<VAR>x✝ : X✝ ⟶ Y✝<VAR>i✝ : ℤ<GOAL>F.map (x✝.f (i✝ + n)) ≫ 𝟙 (F.obj (Y✝.X (i✝ + n))) = 𝟙 (F.obj (X✝.X (i✝ + n))) ≫ F.map (x✝.f (i✝ + n))
<VAR>m n✝ n : ℕ<GOAL>n % 2 = bif n.bodd then 1 else 0
<VAR>m n✝ n : ℕ<VAR>this : (n % 2 + 2 * (n / 2)).bodd = n.bodd<GOAL>n % 2 = bif n.bodd then 1 else 0
<VAR>m n✝ n : ℕ<VAR>this : (n % 2).bodd = n.bodd<GOAL>n % 2 = bif n.bodd then 1 else 0
<VAR>m n✝ n : ℕ<VAR>this : (n % 2).bodd = n.bodd<VAR>x✝¹ : ∀ (b : Bool), (false && b) = false<VAR>x✝ : ∀ (b : Bool), bxor b false = b<GOAL>n % 2 = bif (n % 2).bodd then 1 else 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocRing α<VAR>a b : α<GOAL>(1 - a) * b = b - a * b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R P<VAR>inst✝ : Nontrivial M<VAR>s t : Set α<GOAL>Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R P<VAR>inst✝ : Nontrivial M<VAR>s t : Set α<VAR>h : Disjoint (supported M R s) (supported M R t)<VAR>x : α<VAR>hx1 : x ∈ s<VAR>hx2 : x ∈ t<GOAL>False