ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>i : ι<VAR>hi : x ∈ K i<VAR>R : ℝ≥0∞<VAR>hR₀ : 0 < R<VAR>hR : closedBall x R ⊆ U i<GOAL>∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>i : ι<VAR>hi : x ∈ K i<VAR>R : ℝ≥0∞<VAR>hR₀ : 0 < R<VAR>hR : closedBall x R ⊆ U i<VAR>r : ℝ≥0<VAR>hr₀ : 0 < ↑r<VAR>hrR : ↑r < R<GOAL>∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>i : ι<VAR>hi : x ∈ K i<VAR>R : ℝ≥0∞<VAR>hR₀ : 0 < R<VAR>hR : closedBall x R ⊆ U i<VAR>r : ℝ≥0<VAR>hr₀ : 0 < ↑r<VAR>hrR : ↑r < R<VAR>p : ℝ≥0∞ × X<VAR>hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)<VAR>z : X<VAR>hz : z ∈ closedBall p.2 p.1<GOAL>z ∈ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>i : ι<VAR>hi : x ∈ K i<VAR>R : ℝ≥0∞<VAR>hR₀ : 0 < R<VAR>hR : closedBall x R ⊆ U i<VAR>r : ℝ≥0<VAR>hr₀ : 0 < ↑r<VAR>hrR : ↑r < R<VAR>p : ℝ≥0∞ × X<VAR>hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)<VAR>z : X<VAR>hz : z ∈ closedBall p.2 p.1<GOAL>z ∈ closedBall x R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hκ : IsSFiniteKernel κ<GOAL>κ ⊗ₖ η = Kernel.sum fun n => κ ⊗ₖ η.seq n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hκ : IsSFiniteKernel κ<GOAL>(Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) = Kernel.sum fun n => κ ⊗ₖ η.seq n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>hκ : IsSFiniteKernel κ<GOAL>(Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) = Kernel.sum fun n => Kernel.sum fun n_1 => κ.seq n_1 ⊗ₖ η.seq n
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L I J P : Ideal R<VAR>hp : P.IsPrime<GOAL>I * J ≤ P ↔ I ≤ P ∨ J ≤ P
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J✝ K L I J P : Ideal R<VAR>hp : P.IsPrime<GOAL>(∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonUnitalNonAssocSemiring α<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : NonUnitalSemiring R<VAR>v : m → R<VAR>A : Matrix m n R<VAR>w : n → R<GOAL>v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonUnitalNonAssocSemiring α<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : NonUnitalSemiring R<VAR>v : m → R<VAR>A : Matrix m n R<VAR>w : n → R<GOAL>∑ x : m, ∑ i : n, v x * (A x i * w i) = ∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : A ⟶ S.cycles<GOAL>f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles
<VAR>θ : Angle<GOAL>2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ Ioo a b ↔ False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<GOAL>(f =O[𝓝[≠] a] fun x => 1) ↔ f =O[𝓝 a] fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>h : f =O[𝓝[≠] a] fun x => 1<GOAL>f =O[𝓝 a] fun x => 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>h : ∃ b, ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b<GOAL>∃ b, ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>c : ℝ<VAR>hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c<GOAL>∃ b, ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>c : ℝ<VAR>hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c<GOAL>∀ᶠ (a_1 : α) in 𝓝 a, ‖f a_1‖ ≤ max c ‖f a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>c : ℝ<VAR>hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c<VAR>b : α<VAR>hb : b ∈ {a}ᶜ → ‖f b‖ ≤ c<GOAL>‖f b‖ ≤ max c ‖f a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>c : ℝ<VAR>b : α<VAR>hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c<VAR>hb : b ∈ {b}ᶜ → ‖f b‖ ≤ c<GOAL>‖f b‖ ≤ max c ‖f b‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁶ : Norm E<VAR>inst✝¹⁵ : Norm F<VAR>inst✝¹⁴ : Norm G<VAR>inst✝¹³ : SeminormedAddCommGroup E'<VAR>inst✝¹² : SeminormedAddCommGroup F'<VAR>inst✝¹¹ : SeminormedAddCommGroup G'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F''<VAR>inst✝⁸ : NormedAddCommGroup G''<VAR>inst✝⁷ : SeminormedRing R<VAR>inst✝⁶ : SeminormedAddGroup E'''<VAR>inst✝⁵ : SeminormedRing R'<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝² : One F<VAR>inst✝¹ : NormOneClass F<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>c : ℝ<VAR>hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c<VAR>b : α<VAR>hb : b ∈ {a}ᶜ → ‖f b‖ ≤ c<VAR>hb' : b ≠ a<GOAL>‖f b‖ ≤ max c ‖f a‖
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : head s₁ = head s₂<VAR>ht : last s₁ = last s₂<VAR>hs₁ : s₁.length = 0<GOAL>s₂.length = 0
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : head s₁ = head s₂<VAR>ht : last s₁ = last s₂<VAR>hs₁ : s₁.length = 0<VAR>this : Fin.last s₂.length = 0<GOAL>s₂.length = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e✝ : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>A₁ : Type u_2<VAR>A₂ : Type u_3<VAR>A₃ : Type u_4<VAR>inst✝⁵ : CommSemiring A₁<VAR>inst✝⁴ : CommSemiring A₂<VAR>inst✝³ : CommSemiring A₃<VAR>inst✝² : Algebra R A₁<VAR>inst✝¹ : Algebra R A₂<VAR>inst✝ : Algebra R A₃<VAR>e : A₁ ≃ₐ[R] A₂<VAR>f : A₂ ≃ₐ[R] A₃<VAR>a✝ : MvPolynomial σ A₁<VAR>m✝ : σ →₀ ℕ<GOAL>coeff m✝ (((mapAlgEquiv σ e).trans (mapAlgEquiv σ f)) a✝) = coeff m✝ ((mapAlgEquiv σ (e.trans f)) a✝)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e✝ : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>A₁ : Type u_2<VAR>A₂ : Type u_3<VAR>A₃ : Type u_4<VAR>inst✝⁵ : CommSemiring A₁<VAR>inst✝⁴ : CommSemiring A₂<VAR>inst✝³ : CommSemiring A₃<VAR>inst✝² : Algebra R A₁<VAR>inst✝¹ : Algebra R A₂<VAR>inst✝ : Algebra R A₃<VAR>e : A₁ ≃ₐ[R] A₂<VAR>f : A₂ ≃ₐ[R] A₃<VAR>a✝ : MvPolynomial σ A₁<VAR>m✝ : σ →₀ ℕ<GOAL>coeff m✝ ((map ((↑f).comp ↑e)) a✝) = coeff m✝ ((map ↑(e.trans f)) a✝)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>n : ℕ<VAR>x : α<GOAL>f^[n.succ] x = f (f^[n] x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>n : ℕ<VAR>x : α<GOAL>(f ∘ f^[n]) x = f (f^[n] x)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<GOAL>IsUnit f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<GOAL>IsUnit f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<GOAL>IsUnit f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<GOAL>IsUnit f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<VAR>ic : IsCompatible (sheaf X).val V g<GOAL>IsUnit f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<VAR>ic : IsCompatible (sheaf X).val V g<VAR>gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))<VAR>gl_spec : ∀ (i : ↥U), ((sheaf X).val.map (iVU i).op) gl = g i<GOAL>IsUnit f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<VAR>ic : IsCompatible (sheaf X).val V g<VAR>gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))<VAR>gl_spec : ∀ (i : ↥U), ((sheaf X).val.map (iVU i).op) gl = g i<GOAL>f * gl = 1
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<VAR>ic : IsCompatible (sheaf X).val V g<VAR>gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))<VAR>gl_spec : ∀ (i : ↥U), ((sheaf X).val.map (iVU i).op) gl = g i<GOAL>∀ (i : ↥U), ((sheaf X).val.map (iVU i).op) (f * gl) = ((sheaf X).val.map (iVU i).op) 1
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<VAR>ic : IsCompatible (sheaf X).val V g<VAR>gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))<VAR>gl_spec : ∀ (i : ↥U), ((sheaf X).val.map (iVU i).op) gl = g i<VAR>i : ↥U<GOAL>((sheaf X).val.map (iVU i).op) (f * gl) = ((sheaf X).val.map (iVU i).op) 1
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<VAR>V : ↥U → Opens ↑↑X.toPresheafedSpace<VAR>iVU : (x : ↥U) → V x ⟶ U<VAR>m : ∀ (x : ↥U), ↑x ∈ V x<VAR>h_unit : ∀ (x : ↥U), IsUnit ((X.presheaf.map (iVU x).op) f)<VAR>hcover : U ≤ iSup V<VAR>g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))<VAR>hg : ∀ (x : ↥U), (X.presheaf.map (iVU x).op) f * g x = 1<VAR>ic : IsCompatible (sheaf X).val V g<VAR>gl : (CategoryTheory.forget CommRingCat).obj ((sheaf X).val.obj (op U))<VAR>gl_spec : ∀ (i : ↥U), ((sheaf X).val.map (iVU i).op) gl = g i<VAR>i : ↥U<GOAL>((sheaf X).val.map (iVU i).op) f * g i = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>IsBlock G B ↔ IsBlock (↥⊤) B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>(∀ (g : G), g • B = B ∨ Disjoint (g • B) B) ↔ ∀ (g : ↥⊤), g • B = B ∨ Disjoint (g • B) B
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>inst✝¹ : MvFunctor F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β✝ : Type u<VAR>pp : β✝ → Prop<VAR>β : Type u<VAR>P : β → Prop<VAR>x : F (α ::: β)<GOAL>(∃ u, (fun i => Subtype.val) <$$> u = x) ↔ ∃ u, (fun i => Subtype.val) <$$> u = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>inst✝¹ : MvFunctor F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β✝ : Type u<VAR>pp : β✝ → Prop<VAR>β : Type u<VAR>P : β → Prop<VAR>x : F (α ::: β)<GOAL>MvFunctor.f P n α ⊚ MvFunctor.g P n α = TypeVec.id
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>inst✝¹ : MvFunctor F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β✝ : Type u<VAR>pp : β✝ → Prop<VAR>β : Type u<VAR>P : β → Prop<VAR>x : F (α ::: β)<GOAL>∀ (u : F fun i => { p_1 // ofRepeat (α.PredLast' P i p_1) }), (fun i => Subtype.val) <$$> u = x ↔ (fun i => Subtype.val) <$$> MvFunctor.f P n α <$$> u = x
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ℝ<GOAL>volume (Ico a b) = ofReal (b - a)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : ConnectedSpace α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>f : α → (i : ι) × π i<VAR>hf : Continuous f<GOAL>∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : ConnectedSpace α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>f : α → (i : ι) × π i<VAR>hf : Continuous f<VAR>i : ι<VAR>hi : range f ⊆ range (Sigma.mk i)<GOAL>∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : ConnectedSpace α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>i : ι<VAR>g : α → π i<VAR>hf : Continuous (Sigma.mk i ∘ g)<VAR>hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)<GOAL>∃ i_1 g_1, Continuous g_1 ∧ Sigma.mk i ∘ g = Sigma.mk i_1 ∘ g_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : ConnectedSpace α<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>i : ι<VAR>g : α → π i<VAR>hf : Continuous (Sigma.mk i ∘ g)<VAR>hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)<GOAL>Continuous g
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<GOAL>∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<GOAL>∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<VAR>h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))<GOAL>∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<VAR>h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))<GOAL>(∫ (a : ℝ), cexp (- -b * (↑a + c / (2 * b)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<VAR>h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))<GOAL>(∫ (a : ℝ), cexp (- -b * (↑a + (↑(c / (2 * b)).re + ↑(c / (2 * b)).im * I)) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>hb : b.re < 0<VAR>c d : ℂ<VAR>hb' : b ≠ 0<VAR>h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))<GOAL>(∫ (a : ℝ), cexp (- -b * (↑(a + (c / (2 * b)).re) + ↑(c / (2 * b)).im * I) ^ 2)) * cexp (d - c ^ 2 / (4 * b)) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))