ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<GOAL>∀ x ∈ {x | AnalyticAt 𝕜 f x}, {x | AnalyticAt 𝕜 f x} ∈ 𝓝 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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y : E<VAR>r✝ : ℝ≥0∞<VAR>x : E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hr : HasFPowerSeriesOnBall f p x r<GOAL>{x | AnalyticAt 𝕜 f x} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<VAR>a : α<GOAL>memPartitionSet f n a ∈ memPartition f n
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X✝<VAR>X : Type u<VAR>inst✝ : TopologicalSpace X<GOAL>T0Space X ↔ Pairwise fun x y => ¬Inseparable x y
<VAR>b✝ x y a b : ℝ<GOAL>(logb a b)⁻¹ = logb b a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>s : Set Y<GOAL>IsClosed (⇑h ⁻¹' s) ↔ IsClosed s
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ<VAR>h : IsEmpty ((i : δ) → π i)<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ<VAR>x : (i : δ) → π i<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>inst✝ : DivisionRing K<GOAL>g.convs 0 = g.h
<VAR>G✝ : Type u_1<VAR>inst✝¹ : Group G✝<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<GOAL>center G = ⊤
<VAR>G✝ : Type u_1<VAR>inst✝¹ : Group G✝<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<GOAL>∀ (x : G), x ∈ center G
<VAR>G✝ : Type u_1<VAR>inst✝¹ : Group G✝<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>x : G<GOAL>x ∈ center G
<VAR>G✝ : Type u_1<VAR>inst✝¹ : Group G✝<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>x : G<GOAL>∀ (g : G), g * x = x * g
<VAR>G✝ : Type u_1<VAR>inst✝¹ : Group G✝<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>x y : G<GOAL>y * x = x * y
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : Module R Q<VAR>inst✝⁴ : Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Free R N<VAR>inst✝¹ : Module.Finite R N<VAR>inst✝ : Nontrivial R<VAR>x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)<GOAL>(homTensorHomEquiv R M N P Q) x = (homTensorHomMap R M N P Q) x
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → (i : α) → E i<VAR>this : DecidableEq ι<GOAL>(∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → (i : α) → E i<VAR>this : DecidableEq ι<GOAL>(∀ i ∈ ∅, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ ∅, f i a) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → (i : α) → E i<VAR>this : DecidableEq ι<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p) → (∀ i ∈ insert a s, Memℓp (f i) p) → Memℓp (fun a_3 => ∑ i ∈ insert a s, f i a_3) p
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>h_ne : gaussSum χ e ≠ 0<GOAL>χ.FactorsThrough d
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>h_ne : gaussSum χ e ≠ 0<GOAL>(ZMod.unitsMap hd).ker ≤ (MulChar.toUnitHom χ).ker
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>h_ne : gaussSum χ e ≠ 0<VAR>u : (ZMod N)ˣ<VAR>hu : u ∈ (ZMod.unitsMap hd).ker<GOAL>u ∈ (MulChar.toUnitHom χ).ker
<VAR>N : ℕ<VAR>inst✝² : NeZero N<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>inst✝ : IsDomain R<VAR>χ : DirichletCharacter R N<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>he : e.mulShift ↑d = 1<VAR>h_ne : gaussSum χ e ≠ 0<VAR>u : (ZMod N)ˣ<VAR>hu : u ∈ (ZMod.unitsMap hd).ker<GOAL>χ ↑u = ↑1
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>inst✝ : Countable α<VAR>o : α → Ordinal.{max u_3 u_2}<VAR>ho : ∀ (n : α), o n < (aleph 1).ord<GOAL>sup o < (aleph 1).ord
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>inst✝ : Countable α<VAR>o : α → Ordinal.{max u_3 u_2}<VAR>ho : ∀ (n : α), o n < (aleph 1).ord<GOAL>Cardinal.lift.{u_3, u_2} #α < (aleph 1).ord.cof
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α : Type u_2<VAR>inst✝ : Countable α<VAR>o : α → Ordinal.{max u_3 u_2}<VAR>ho : ∀ (n : α), o n < (aleph 1).ord<GOAL>Cardinal.lift.{u_3, u_2} #α < aleph 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i => α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>UniformSpace.comap F (Pi.uniformSpace fun i => α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>comap (fun p => (F p.1, F p.2)) (𝓤 (X → α)) ≤ comap (fun p => (F p.1, F p.2)) (𝓤 (X → α))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α) ≤ comap (fun p => (F p.1, F p.2)) (𝓤 (X → α))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>∀ i' ∈ 𝓤 α, Prod.map F F ⁻¹' UniformFun.gen X α i' ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>Vsymm : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<GOAL>Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>Vsymm : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<VAR>Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}<GOAL>Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>Vsymm : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<VAR>Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}<VAR>A : Finset X<VAR>Acover : ⋃ x ∈ A, Ω x = ⊤<GOAL>Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : CompactSpace X<VAR>F_eqcont : Equicontinuous F<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>Vsymm : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<VAR>Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}<VAR>A : Finset X<VAR>Acover : ⋃ x ∈ A, Ω x = ⊤<VAR>this : ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U<GOAL>Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>rexp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>k p : ℕ<VAR>f : ℕ → α<VAR>h : Prime p<GOAL>∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ range k, f (p ^ x)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<VAR>c : CliffordAlgebra (Q c₁ c₂)<GOAL>toQuaternion (star c) = star (toQuaternion c)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c₁ c₂ : R<VAR>c : CliffordAlgebra (Q c₁ c₂)<GOAL>toQuaternion (involute (reverse c)) = star (toQuaternion c)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>↑e { proj := b, snd := e.symm b y } = (b, y)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>M.one.app (M.X.obj X) ≫ M.mul.app X = 𝟙 ((𝟭 C).obj (M.X.obj X))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>(MonoidalCategory.rightUnitor M.X).hom.app X = 𝟙 ((𝟭 C).obj (M.X.obj X))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>M.X.map (M.one.app X) ≫ M.mul.app X = 𝟙 (M.X.obj ((𝟭 C).obj X))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>(MonoidalCategory.leftUnitor M.X).hom.app X = 𝟙 (M.X.obj ((𝟭 C).obj X))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>M.X.map (M.mul.app X) ≫ M.mul.app X = M.mul.app (M.X.obj X) ≫ M.mul.app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>(whiskerRight M.mul M.X ≫ M.mul).app X = (whiskerLeft M.X M.mul).app X ≫ M.mul.app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>M : Mon_ (C ⥤ C)<VAR>X : C<GOAL>((MonoidalCategory.associator M.X M.X M.X).hom ≫ MonoidalCategory.whiskerLeft M.X M.mul ≫ M.mul).app X = (whiskerLeft M.X M.mul).app X ≫ M.mul.app X
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : HasPushout f g<GOAL>pushout.inr g f ≫ (pushoutSymmetry f g).inv = pushout.inl f g
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ k, ↑p ^ (-↑k) < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ↑ε<GOAL>∃ k, ↑p ^ (-↑k) < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>k : ℕ<VAR>hk : ↑p ^ (-↑k) < ↑ε<GOAL>↑p ^ (-↑k) < ε
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h₁ : HasDerivAt f f' x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasDerivAt (fun t => log (f t)) (f' / f x) x
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>h₁ : HasDerivAt f f' x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>r : ℝ<GOAL>↑(ℜ ↑r) = ↑r
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>r : ℝ<GOAL>2⁻¹ • 2 • ↑r = ↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>s : Finset ι<VAR>μ : ι → Measure α<GOAL>(sum fun i => μ ↑i) = ∑ i ∈ s, μ i
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫ (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).hom) ≫ (limitIsoLimitCurryCompLim G).hom) ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k = limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫ limit.π (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k)) ≫ (𝟙 ((Prod.braiding K J).functor ⋙ G)).app ((Prod.braiding K J).inverse.obj (j, k)) ≫ G.map (𝟙 j, 𝟙 k) = limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫ limit.π (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k)) ≫ 𝟙 ((Prod.swap K J ⋙ G).obj ((Prod.braiding K J).inverse.obj (j, k))) ≫ G.map (𝟙 j, 𝟙 k) = limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫ limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (𝟙 j, 𝟙 k) = limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
<VAR>J K : Type v<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : SmallCategory K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝ : HasLimits C<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫ limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) = limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>minpoly K (root f) = f * C f.leadingCoeff⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<VAR>f'_monic : (f * C f.leadingCoeff⁻¹).Monic<GOAL>minpoly K (root f) = f * C f.leadingCoeff⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<VAR>f'_monic : (f * C f.leadingCoeff⁻¹).Monic<GOAL>(aeval (root f)) (f * C f.leadingCoeff⁻¹) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<VAR>f'_monic : (f * C f.leadingCoeff⁻¹).Monic<GOAL>∀ (q : K[X]), q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<VAR>f'_monic : (f * C f.leadingCoeff⁻¹).Monic<VAR>q : K[X]<VAR>q_monic : q.Monic<VAR>q_aeval : (aeval (root f)) q = 0<VAR>commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f<GOAL>(f * C f.leadingCoeff⁻¹).degree ≤ q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<VAR>f'_monic : (f * C f.leadingCoeff⁻¹).Monic<VAR>q : K[X]<VAR>q_monic : q.Monic<VAR>q_aeval : (aeval (root f)) q = 0<VAR>commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f<GOAL>f.natDegree ≤ q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<VAR>f'_monic : (f * C f.leadingCoeff⁻¹).Monic<VAR>q : K[X]<VAR>q_monic : q.Monic<VAR>q_aeval : (aeval (root f)) q = 0<VAR>commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f<GOAL>C f.leadingCoeff⁻¹ ≠ 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<GOAL>f ∈ L.mapArrow.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.EssSurj<GOAL>f ∈ L.mapArrow.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.EssSurj<VAR>X : C<VAR>eX : L.obj X ≅ f.left<VAR>Y : C<VAR>eY : L.obj Y ≅ f.right<GOAL>f ∈ L.mapArrow.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.EssSurj<VAR>X : C<VAR>eX : L.obj X ≅ f.left<VAR>Y : C<VAR>eY : L.obj Y ≅ f.right<VAR>φ : W.LeftFraction X Y<VAR>hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯<GOAL>f ∈ L.mapArrow.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.EssSurj<VAR>X : C<VAR>eX : L.obj X ≅ f.left<VAR>Y : C<VAR>eY : L.obj Y ≅ f.right<VAR>φ : W.LeftFraction X Y<VAR>hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯<GOAL>f ≅ L.mapArrow.obj (Arrow.mk φ.f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.EssSurj<VAR>X : C<VAR>eX : L.obj X ≅ f.left<VAR>Y : C<VAR>eY : L.obj Y ≅ f.right<VAR>φ : W.LeftFraction X Y<VAR>hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯<GOAL>eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk φ.f)).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W φ.s ⋯).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.EssSurj<VAR>X : C<VAR>eX : L.obj X ≅ f.left<VAR>Y : C<VAR>eY : L.obj Y ≅ f.right<VAR>φ : W.LeftFraction X Y<VAR>hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map L ⋯<GOAL>eX.inv ≫ L.map φ.f = f.hom ≫ eY.inv ≫ L.map φ.s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t s : Set α<VAR>f : Filter α<GOAL>𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V
<VAR>x : ONote<VAR>inst✝¹ : x.NF<VAR>o : ONote<VAR>inst✝ : o.NF<GOAL>(x.scale o).repr = ω ^ x.repr * o.repr
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : (b : B) → TopologicalSpace (E b)<VAR>inst✝² : ConditionallyCompleteLinearOrder B<VAR>inst✝¹ : OrderTopology B<VAR>inst✝ : FiberBundle F E<VAR>a b : B<GOAL>∃ e, Icc a b ⊆ e.baseSet