ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ = (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) / 2 - ‖I • x + z‖ * ‖I • x + z‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<VAR>h₀ : ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ + ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ = 2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)<GOAL>‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : IsDomain R<VAR>S : Submonoid R<VAR>inst✝ : StrongRankCondition R<GOAL>Nonempty (OreLocalization.OreSet R⁰)
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : IsDomain R<VAR>S : Submonoid R<VAR>inst✝ : StrongRankCondition R<VAR>h : ¬Nonempty (OreLocalization.OreSet R⁰)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : IsDomain R<VAR>S : Submonoid R<VAR>inst✝ : StrongRankCondition R<VAR>h : ¬Nonempty (OreLocalization.OreSet R⁰)<VAR>this : ℵ₀ ≤ Module.rank R R<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : IsDomain R<VAR>S : Submonoid R<VAR>inst✝ : StrongRankCondition R<VAR>h : ¬Nonempty (OreLocalization.OreSet R⁰)<VAR>this : ℵ₀ ≤ 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x y : α<VAR>S U Z : Set α<VAR>hS : IsClosed S<VAR>hxS : x ∈ S<GOAL>IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x y : α<VAR>S U Z : Set α<VAR>hS : IsClosed S<VAR>hxS : x ∈ S<VAR>this : closure {x} ⊆ S<GOAL>IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>((single 0) r * x).coeff a = r * x.coeff a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<GOAL>t.π.app WalkingCospan.one = t.fst ≫ f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>w : ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one = t.π.app WalkingCospan.left ≫ (cospan f g).map inl<GOAL>t.π.app WalkingCospan.one = t.fst ≫ f
<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>n : ℕ<VAR>r : ℝ<VAR>s : Simplex ℝ P n<VAR>p₁ : P<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)<GOAL>dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius
<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>n : ℕ<VAR>r : ℝ<VAR>s : Simplex ℝ P n<VAR>p₁ : P<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)<GOAL>dist s.circumcenter p₁ * dist s.circumcenter p₁ = dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) * dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) + dist p₁ ↑(s.orthogonalProjectionSpan p₁) * dist p₁ ↑(s.orthogonalProjectionSpan p₁) - s.circumradius * s.circumradius
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s<GOAL>StrictConvex 𝕜 s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s<GOAL>s.Pairwise fun x y => openSegment 𝕜 x y ⊆ interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hne : x ≠ y<VAR>hx' : x ∉ interior s<VAR>hy' : y ∉ interior s<VAR>c : 𝕜<VAR>hc : (lineMap x y) c ∈ interior s<GOAL>openSegment 𝕜 x y ⊆ interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hne : x ≠ y<VAR>hx' : x ∉ interior s<VAR>hy' : y ∉ interior s<VAR>c : 𝕜<VAR>hc : (lineMap x y) c ∈ interior s<GOAL>openSegment 𝕜 x ((lineMap x y) c) ⊆ interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hne : x ≠ y<VAR>hx' : x ∉ interior s<VAR>hy' : y ∉ interior s<VAR>c : 𝕜<VAR>hc : (lineMap x y) c ∈ interior s<GOAL>openSegment 𝕜 ((lineMap x y) c) y ⊆ interior s
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LocalRing R<VAR>q : ℕ<VAR>char_R_q : CharP R q<GOAL>q = 0 ∨ IsPrimePow q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LocalRing R<VAR>q : ℕ<VAR>char_R_q : CharP R q<GOAL>¬q = 0 → IsPrimePow q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LocalRing R<VAR>q : ℕ<VAR>char_R_q : CharP R q<VAR>q_pos : ¬q = 0<VAR>K : Type u_1 := LocalRing.ResidueField R<VAR>RM_char : CharP K (ringChar K)<VAR>r : ℕ := ringChar K<VAR>n : ℕ := q.factorization r<GOAL>IsPrimePow q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LocalRing R<VAR>q : ℕ<VAR>char_R_q : CharP R q<VAR>q_pos : ¬q = 0<VAR>K : Type u_1 := LocalRing.ResidueField R<VAR>RM_char : CharP K (ringChar K)<VAR>r : ℕ := ringChar K<VAR>n : ℕ := q.factorization r<VAR>r_prime : Nat.Prime r<GOAL>IsPrimePow q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : LocalRing R<VAR>q : ℕ<VAR>char_R_q : CharP R q<VAR>q_pos : ¬q = 0<VAR>K : Type u_1 := LocalRing.ResidueField R<VAR>RM_char : CharP K (ringChar K)<VAR>r : ℕ := ringChar K<VAR>n : ℕ := q.factorization r<VAR>r_zero : r = 0<GOAL>IsPrimePow q
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<VAR>j : τ<VAR>h : j ∈ ((bind₁ f) φ).vars<GOAL>∃ i ∈ φ.vars, j ∈ (f i).vars
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>⊤.inv = ⊤
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Vector α n.succ<VAR>v' : Vector α n<VAR>h : v.head = a ∧ v.tail = v'<GOAL>v.head ::ᵥ v.tail = a ::ᵥ v'
<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>x y : P<GOAL>(lineMap y ((pointReflection R x) y)) 2⁻¹ = x
<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>x y : P<GOAL>2⁻¹ • 2 • (x -ᵥ y) +ᵥ y = x
<VAR>x : ℝ*<VAR>r s : ℝ<VAR>hr : x.IsSt r<VAR>hs : x.IsSt s<GOAL>r = s
<VAR>r s : ℝ<VAR>f : ℕ → ℝ<VAR>hr : (ofSeq f).IsSt r<VAR>hs : (ofSeq f).IsSt s<GOAL>r = s
<VAR>r s : ℝ<VAR>f : ℕ → ℝ<VAR>hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)<VAR>hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)<GOAL>r = s
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Antitone seq<VAR>hseq_tendsto : Tendsto seq atTop atBot<GOAL>∀ᵐ (c : β) ∂ν a, Tendsto (fun m => f (a, c) (seq m)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Antitone seq<VAR>hseq_tendsto : Tendsto seq atTop atBot<GOAL>∀ (n : ℕ), Integrable (fun c => f (a, c) (seq n)) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Antitone seq<VAR>hseq_tendsto : Tendsto seq atTop atBot<GOAL>Tendsto (fun i => ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 (∫ (a : β), 0 ∂ν a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Antitone seq<VAR>hseq_tendsto : Tendsto seq atTop atBot<GOAL>∀ᵐ (a_1 : β) ∂ν a, Antitone fun i => f (a, a_1) (seq i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → ℚ<VAR>hseq : Antitone seq<VAR>hseq_tendsto : Tendsto seq atTop atBot<GOAL>∀ᵐ (a_1 : β) ∂ν a, ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
<VAR>x y : ℝ<VAR>h0 : x < 0<VAR>h1 : -1 < x<GOAL>log x < 0
<VAR>x y : ℝ<VAR>h0 : x < 0<VAR>h1 : -1 < x<GOAL>log (-x) < 0
<VAR>x y : ℝ<VAR>h0 : x < 0<VAR>h1 : -1 < x<VAR>h0' : 0 < -x<VAR>h1' : -x < 1<GOAL>log (-x) < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : CommMonoid α<VAR>inst✝⁴ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝³ : CommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>hf : HasProd f a<VAR>G : Type u_5<VAR>inst✝¹ : FunLike G α γ<VAR>inst✝ : MonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>HasProd (⇑g ∘ f) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : CommMonoid α<VAR>inst✝⁴ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝³ : CommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>hf : HasProd f a<VAR>G : Type u_5<VAR>inst✝¹ : FunLike G α γ<VAR>inst✝ : MonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<VAR>this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b<GOAL>HasProd (⇑g ∘ f) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : CommMonoid α<VAR>inst✝⁴ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝³ : CommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>hf : HasProd f a<VAR>G : Type u_5<VAR>inst✝¹ : FunLike G α γ<VAR>inst✝ : MonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<VAR>this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b<GOAL>Tendsto (⇑g ∘ fun s => ∏ b ∈ s, f b) atTop (𝓝 (g a))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>s : Set α<GOAL>kernMap m (𝓟 s) = 𝓟 (kernImage m s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>s : Set α<VAR>g : Filter β<GOAL>g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' s : Cycle α<VAR>h : s.Subsingleton<GOAL>s.formPerm ⋯ = 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' : Cycle α<VAR>s : List α<VAR>h : Subsingleton (Quot.mk Setoid.r s)<GOAL>formPerm (Quot.mk Setoid.r s) ⋯ = 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' : Cycle α<VAR>s : List α<VAR>h : Subsingleton (Quot.mk Setoid.r s)<GOAL>s.formPerm = 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' : Cycle α<VAR>s : List α<VAR>h : s.length ≤ 1<GOAL>s.formPerm = 1
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y Z : C<VAR>f : J → C<VAR>g h : X ⊗ Y ⊗ ⨁ f ⟶ Z<VAR>w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y Z : C<VAR>f : J → C<VAR>g h : X ⊗ Y ⊗ ⨁ f ⟶ Z<VAR>w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h<GOAL>(α_ X Y (⨁ f)).hom ≫ g = (α_ X Y (⨁ f)).hom ≫ h
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix (Fin 3) (Fin 3) α<VAR>i j : Fin 3<GOAL>A.adjugate i j = !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1; -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0; A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0] i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix (Fin 3) (Fin 3) α<VAR>i j : Fin 3<GOAL>(-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 - A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) = !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1; -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0; A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0] i j
<VAR>x : ℂ<VAR>h : x ∈ slitPlane<VAR>h0 : x ≠ 0<GOAL>HasStrictDerivAt (↑expPartialHomeomorph) x (↑expPartialHomeomorph.symm x)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<GOAL>H.subgroupOf K = ⊥ ↔ Disjoint H K
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a ⊔ b) \ b = a \ b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subsemiring.map g f.rangeS = (g.comp f).rangeS
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a b : α<VAR>ab : a ≠ b<VAR>s : Multiset α<VAR>l : List α<GOAL>count a (erase ⟦l⟧ b) = count a ⟦l⟧
<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>(n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>(n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = (n.factorization.prod fun x x_1 => x ^ x_1) * ∏ p ∈ n.primeFactors, (p - 1)
<VAR>n : ℕ<VAR>hn : ¬n = 0<GOAL>(n.factorization.prod fun a b => a ^ (b - 1) * (a - 1) * a) = n.factorization.prod fun a b => a ^ b * (a - 1)
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>p : ℕ<VAR>hp : p ∈ n.factorization.support<GOAL>p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)
<VAR>n : ℕ<VAR>hn : ¬n = 0<VAR>p : ℕ<VAR>hp : 0 < n.factorization p<GOAL>p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>(TensorProduct.mk R ↑(of R R) ↑M).compr₂ (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = (TensorProduct.mk R ↑(of R R) ↑M).compr₂ ((leftUnitor M).hom ≫ f)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>((TensorProduct.mk R ↑(of R R) ↑M).compr₂ (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1 = ((TensorProduct.mk R ↑(of R R) ↑M).compr₂ ((leftUnitor M).hom ≫ f)) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>∀ (x : ↑M), (((TensorProduct.mk R ↑(of R R) ↑M).compr₂ (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x = (((TensorProduct.mk R ↑(of R R) ↑M).compr₂ ((leftUnitor M).hom ≫ f)) 1) x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(leftUnitor N).hom ((tensorHom (𝟙 (of R R)) f) (1 ⊗ₜ[R] x)) = f ((leftUnitor M).hom (1 ⊗ₜ[R] x))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(𝟙 (of R R)) (1, x).1 • f (1, x).2 = f (1 • x)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(𝟙 (of R R)) (1, x).1 • f (1, x).2 = 1 • f x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<GOAL>↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>f ≫ (g + h) = f ≫ g + f ≫ h
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>(f ≫ biprod.lift g h) ≫ biprod.desc (𝟙 Z) (𝟙 Z) = biprod.lift (f ≫ g) (f ≫ h) ≫ biprod.desc (𝟙 Z) (𝟙 Z)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>α : Type u_2<VAR>f : OnePoint X → α<VAR>l : Filter α<GOAL>Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ : P<GOAL>Collinear k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ : P<GOAL>∃ p₀ v, ∀ p ∈ {p₁, p₂}, ∃ r, p = r • v +ᵥ p₀
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ : P<GOAL>∀ p ∈ {p₁, p₂}, ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p : P<VAR>hp : p ∈ {p₁, p₂}<GOAL>∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p : P<VAR>hp : p = p₁ ∨ p = p₂<GOAL>∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<GOAL>spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>h✝ : Subsingleton A<GOAL>spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>h✝ : Nontrivial A<GOAL>spectrum ℂ (star a * a) ⊆ Set.Icc 0 ↑‖star a * a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<VAR>posmeas : Set ι := {i | 0 < μ (As i)}<VAR>posmeas_def : posmeas = {i | 0 < μ (As i)}<GOAL>posmeas.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<VAR>posmeas : Set ι := {i | 0 < μ (As i)}<VAR>posmeas_def : posmeas = {i | 0 < μ (As i)}<VAR>as : ℕ → ℝ≥0∞<VAR>left✝ : StrictAnti as<VAR>as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1<VAR>as_lim : Tendsto as atTop (𝓝 0)<GOAL>posmeas.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<VAR>Union_As_finite : μ (⋃ i, As i) ≠ ⊤<VAR>posmeas : Set ι := {i | 0 < μ (As i)}<VAR>posmeas_def : posmeas = {i | 0 < μ (As i)}<VAR>as : ℕ → ℝ≥0∞<VAR>left✝ : StrictAnti as<VAR>as_mem : ∀ (n : ℕ), as n ∈ Ioo 0 1<VAR>as_lim : Tendsto as atTop (𝓝 0)<VAR>fairmeas : ℕ → Set ι := fun n => {i | as n ≤ μ (As i)}<GOAL>posmeas.Countable