ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>m : M'<GOAL>m = fromLocalizedModule' S f (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<GOAL>((expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<GOAL>p • Multiset.map (⇑(frobeniusEquiv R p ^ 1).symm) f.roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b x : α<GOAL>x ∈ ↑(s ∆ t) ↔ x ∈ ↑s ∆ ↑t
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<GOAL>ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉₊ ⌈b⌉₊
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>t : Set 𝕜<VAR>h : Dense t<GOAL>range (deriv f) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>t : Set 𝕜<VAR>h : Dense t<GOAL>range (derivWithin f univ) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>t : Set 𝕜<VAR>h : Dense t<GOAL>univ ⊆ closure (univ ∩ t)
<VAR>A : Type u_1<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra ℂ A<VAR>inst✝¹ : StarModule ℂ A<VAR>inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<GOAL>IsSelfAdjoint a ↔ IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM
<VAR>A : Type u_1<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra ℂ A<VAR>inst✝¹ : StarModule ℂ A<VAR>inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>x : ℂ<VAR>hx : x ∈ σ ℂ a<GOAL>(algebraMap ℝ ℂ) (Complex.reCLM x) = x
<VAR>A : Type u_1<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra ℂ A<VAR>inst✝¹ : StarModule ℂ A<VAR>inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<GOAL>IsStarNormal a ∧ SpectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>b : β<GOAL>nndist (f b) (g b) ≤ nndist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>b : β<GOAL>edist (f b) (g b) ≤ edist f g
<VAR>x y : ℤ<GOAL>|x| < |y| ↔ x.natAbs < y.natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : IntegrableOn f (s ×ˢ Set.univ) ρ<GOAL>∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : IntegrableOn f (s ×ˢ Set.univ) ρ<GOAL>∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a r : ℝ<GOAL>volume (Metric.ball a r) = ofReal (2 * r)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{w, v} C<VAR>inst✝ : HasTerminal C<VAR>A a b : C<VAR>f : a ⟶ b<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>(skyscraperPresheaf p₀ a).map i ≫ (fun U => if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) V = (fun U => if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) U ≫ (skyscraperPresheaf p₀ b).map i
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{w, v} C<VAR>inst✝ : HasTerminal C<VAR>A a b : C<VAR>f : a ⟶ b<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>((if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then a else ⊤_ C)) ≫ if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj V)) = (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) ≫ if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then b else ⊤_ C)
<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]<VAR>x : R<GOAL>(C x).roots = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hg : Memℒp g p μ<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)<VAR>this : f = (fun x => g) + fun n => f n - g<GOAL>UnifTight ((fun x => g) + fun n => f n - g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hg : Memℒp g p μ<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)<VAR>this : f = (fun x => g) + fun n => f n - g<GOAL>UnifTight (fun x => g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hg : Memℒp g p μ<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)<VAR>this : f = (fun x => g) + fun n => f n - g<GOAL>UnifTight (fun n => f n - g) p μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>(a :: l).sublists' = l.sublists' ++ map (cons a) l.sublists'
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>‖inclusionInDoubleDual 𝕜 E‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ ≤ 1
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>this : ∀ (a : ↥s) (b : V), (_root_.orthogonalProjection s.direction) b = 0 → (reflection s) ((reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a<GOAL>(reflection s) ((reflection s) p) = p
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>this : ∀ (a : ↥s) (b : V), (_root_.orthogonalProjection s.direction) b = 0 → (reflection s) ((reflection s) (b +ᵥ ↑a)) = b +ᵥ ↑a<GOAL>(reflection s) ((reflection s) (p -ᵥ ↑((orthogonalProjection s) p) +ᵥ ↑((orthogonalProjection s) p))) = p -ᵥ ↑((orthogonalProjection s) p) +ᵥ ↑((orthogonalProjection s) p)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>Odd (m * n) ↔ Odd m ∧ Odd n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>j k : ι<VAR>inst✝ : K.HasHomology j<VAR>h : K.d (c.prev j) j = 0<GOAL>IsIso (K.pOpcycles j)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Ring S<VAR>inst✝¹⁰ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsAlgClosed E<VAR>x : L<GOAL>(algebraMap K E) ((norm K) x) = ∏ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Ring S<VAR>inst✝¹⁰ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsAlgClosed E<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>(algebraMap K E) ((norm K) x) = ∏ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Ring S<VAR>inst✝¹⁰ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsAlgClosed E<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>(∏ σ : ↥K⟮x⟯ →ₐ[K] E, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ : L →ₐ[K] E, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Ring S<VAR>inst✝¹⁰ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : Algebra K F<VAR>ι : Type w<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsAlgClosed E<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>IsSeparable K (adjoin.powerBasis hx).gen
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>xz a1 (m - n) = xz a1 m * xz a1 n - ↑(Pell.d a1) * yz a1 m * yz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>xz a1 (m - n) = xz a1 m * xz a1 n + ↑(Pell.d a1) * yz a1 m * -yz a1 n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ c<VAR>H : a ∣ b + c<GOAL>a ∣ b
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.54457, u_1} C<VAR>inst✝⁵ : Category.{?u.54461, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>F.shiftIso (m + n) a a'' ⋯ = isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫ (shiftFunctor C m).associator (shiftFunctor C n) (F.shift a) ≪≫ isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (P F).W α<VAR>h : WEquiv x y<GOAL>WEquiv y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>i j : α<GOAL>(i, j) ∈ (s ∪ t).diag ↔ (i, j) ∈ s.diag ∪ t.diag
<VAR>x : ℂ<VAR>hx : ¬x = 0<GOAL>log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x
<VAR>x : ℂ<VAR>hx : ¬x = 0<GOAL>(if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x
<VAR>x : ℂ<VAR>hx : ¬x = 0<GOAL>0 < (normSq x)⁻¹
<VAR>x : ℂ<VAR>hx : ¬x = 0<GOAL>(starRingEnd ℂ) x ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>s t : Set α<VAR>l : Filter α<GOAL>t ∈ l ⊓ 𝓟 s ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t
<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 : C<VAR>X : Subobject B<VAR>f : A ⟶ B<VAR>inst✝ : Mono f<VAR>Y : Subobject B<VAR>h₁ : X ≤ mk f<VAR>h₂ : mk f ≤ Y<GOAL>X.ofLEMk f h₁ ≫ ofMkLE f Y h₂ = X.ofLE Y ⋯
<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 : C<VAR>X : Subobject B<VAR>f : A ⟶ B<VAR>inst✝ : Mono f<VAR>Y : Subobject B<VAR>h₁ : X ≤ mk f<VAR>h₂ : mk f ≤ Y<GOAL>underlying.map (h₁.hom ≫ h₂.hom) = underlying.map ⋯.hom
<VAR>B : Type u<VAR>inst✝¹ : Bicategory B<VAR>a b c d e : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>h : b ⟶ c<VAR>inst✝ : IsIso η<GOAL>inv (η ▷ h) = inv η ▷ h
<VAR>B : Type u<VAR>inst✝¹ : Bicategory B<VAR>a b c d e : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>h : b ⟶ c<VAR>inst✝ : IsIso η<GOAL>η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
<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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : ↥(simpleFunc E 1 μ)<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f) + SimpleFunc.setToSimpleFunc T (toSimpleFunc g)
<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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : ↥(simpleFunc E 1 μ)<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (f + g)) = SimpleFunc.setToSimpleFunc T (toSimpleFunc f + toSimpleFunc g)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>h : i ≠ j<VAR>c d : R<GOAL>transvection i j c * transvection i j d = transvection i j (c + d)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>h : c = 0 → s.Nonempty<VAR>x : E<GOAL>egauge 𝕜 s (c • x) = ↑‖c‖₊ * egauge 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>h : c = 0 → s.Nonempty<VAR>x : E<GOAL>egauge 𝕜 s (c • x) ≤ ↑‖c‖₊ * egauge 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>x : E<VAR>h : 0 = 0 → s.Nonempty<GOAL>egauge 𝕜 s (0 • x) ≤ ↑‖0‖₊ * egauge 𝕜 s x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>h : c = 0 → s.Nonempty<VAR>x : E<VAR>hc : c ≠ 0<GOAL>egauge 𝕜 s (c • x) ≤ ↑‖c‖₊ * egauge 𝕜 s x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>hU : IsOpen s<GOAL>s ∈ 𝓝ˢ t ↔ t ⊆ s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f + g ≈ 0<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f + g ≈ 0<VAR>this : 0 ≤ max f.norm g.norm<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>hfg' : f + g ≈ g<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>hfg' : f + g ≈ g<VAR>hcfg : (f + g).norm = g.norm<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>hfg' : f + g ≈ g<VAR>hcfg : (f + g).norm = g.norm<VAR>hcl : f.norm = 0<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : f ≈ 0<VAR>hfg' : f + g ≈ g<VAR>hcfg : (f + g).norm = g.norm<VAR>hcl : f.norm = 0<VAR>this : max f.norm g.norm = g.norm<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>hfg' : f + g ≈ f<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>hfg' : f + g ≈ f<VAR>hcfg : (f + g).norm = f.norm<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>hfg' : f + g ≈ f<VAR>hcfg : (f + g).norm = f.norm<VAR>hcl : g.norm = 0<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>hfg' : f + g ≈ f<VAR>hcfg : (f + g).norm = f.norm<VAR>hcl : g.norm = 0<VAR>this : max f.norm g.norm = f.norm<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<GOAL>(killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule = killingForm R ↥(ad R L).range
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<GOAL>killingForm R ↥↑(ad R L).idealRange = killingForm R ↥(lieIdealSubalgebra R (LieDerivation R L L) (ad R L).idealRange)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>h₀ : 0 < R₁<GOAL>‖deriv f c‖ ≤ R₂ / R₁
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<GOAL>∃ p ∈ s, Sbtw R x p y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SOppSide x y<VAR>p : P<VAR>hp : p ∈ s<VAR>hw : Wbtw R x p y<GOAL>∃ p ∈ s, Sbtw R x p y
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>⇑hU.fromSpec.val.base '' (⇑hU.fromSpec.val.base ⁻¹' ↑(X.basicOpen f)) = ↑(X.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>↑(X.basicOpen f) ⊆ ↑U
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : IsEmpty α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>this : Subsingleton (Measure α)<GOAL>∫⁻ (x : α), f x ∂μ = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝² : LindelofSpace X<VAR>f : Filter X<VAR>inst✝¹ : f.NeBot<VAR>inst✝ : CountableInterFilter f<GOAL>∃ x, ClusterPt x f
<VAR>k : Type u<VAR>inst✝¹⁵ : Field k<VAR>K : Type u<VAR>inst✝¹⁴ : Field K<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Field M<VAR>inst✝¹⁰ : Algebra K M<VAR>inst✝⁹ : IsAlgClosed M<VAR>inst✝⁸ : Algebra.IsAlgebraic K L<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>S : Type v<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R M<VAR>inst✝² : NoZeroSMulDivisors R S<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Algebra.IsAlgebraic R S<GOAL>S →ₐ[R] M
<VAR>k : Type u<VAR>inst✝¹⁵ : Field k<VAR>K : Type u<VAR>inst✝¹⁴ : Field K<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Field M<VAR>inst✝¹⁰ : Algebra K M<VAR>inst✝⁹ : IsAlgClosed M<VAR>inst✝⁸ : Algebra.IsAlgebraic K L<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>S : Type v<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R M<VAR>inst✝² : NoZeroSMulDivisors R S<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Algebra.IsAlgebraic R S<VAR>this : IsDomain R := Function.Injective.isDomain (algebraMap R S) (NoZeroSMulDivisors.algebraMap_injective R S)<GOAL>S →ₐ[R] M