ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>m : M<VAR>hm : m ∈ weightSpace M χ<VAR>x : L<VAR>this : ((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f = ↑f ∘ₗ ((toEnd R L M) x - χ x • 1)<VAR>k : ℕ<VAR>h : (((toEnd R L M) x - χ x • 1) ^ k) m = 0<GOAL>∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x y z : E<VAR>hx : x ≠ z<VAR>hy : y ≠ z<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>z ∈ openSegment 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x y z : E<VAR>hx : x ≠ z<VAR>hy : y ≠ z<VAR>hz : z ∈ insert x (insert y (openSegment 𝕜 x y))<GOAL>z ∈ openSegment 𝕜 x y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>f : α ⊕ β → Ordinal.{max (max u v) w}<GOAL>sup f = max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>f : α ⊕ β → Ordinal.{max (max u v) w}<GOAL>∀ (i : α ⊕ β), f i ≤ max (sup fun a => f (Sum.inl a)) (sup fun b => f (Sum.inr b))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>f : α ⊕ β → Ordinal.{max (max u v) w}<GOAL>(sup fun a => f (Sum.inl a)) ≤ sup f
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>f : α ⊕ β → Ordinal.{max (max u v) w}<GOAL>(sup fun b => f (Sum.inr b)) ≤ sup f
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>a : R<GOAL>a - a / 2 = a / 2
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hf : Integrable f volume<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v = (1 / 2) • ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • (f v - f (v + i w))
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hf : Integrable f volume<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v = (1 / 2) • ∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v - 𝐞 (-⟪v, w⟫_ℝ) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hf : Integrable f volume<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v = (1 / 2 * 2) • ∫ (a : V), 𝐞 (-⟪a, w⟫_ℝ) • f a
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hf : Integrable f volume<GOAL>Integrable (fun v => 𝐞 (-⟪v, w⟫_ℝ) • f v) volume
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hf : Integrable f volume<GOAL>Integrable (fun v => 𝐞 (-⟪v, w⟫_ℝ) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w)) volume
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<GOAL>∀ (l : ListBlank Γ), cons l.head l.tail = l
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<GOAL>∀ (a : List Γ), cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)) = Quotient.mk'' a
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : List Γ<GOAL>BlankExtends l (head (Quotient.mk'' l) :: l.tail)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>Balanced 𝕜 (Metric.ball 0 r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>Balanced 𝕜 ((normSeminorm 𝕜 E).ball 0 r)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(cokernel.π f).op ≫ f.op = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>f ≫ (kernel.ι f.op).unop = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(kernel.ι f.op ≫ f.op).unop = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(kernel.lift f.op (cokernel.π f).op ⋯).unop ≫ cokernel.desc f (kernel.ι f.op).unop ⋯ = 𝟙 (Opposite.unop (kernel f.op))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>((cokernel.desc f (kernel.ι f.op).unop ⋯).op ≫ kernel.lift f.op (cokernel.π f).op ⋯).unop = (𝟙 (kernel f.op)).unop
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>((cokernel.desc f (kernel.ι f.op).unop ⋯).op ≫ kernel.lift f.op (cokernel.π f).op ⋯) ≫ equalizer.ι f.op 0 = 𝟙 (kernel f.op) ≫ equalizer.ι f.op 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.1400, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>coequalizer.π f 0 ≫ cokernel.desc f (kernel.ι f.op).unop ⋯ ≫ (kernel.lift f.op (cokernel.π f).op ⋯).unop = coequalizer.π f 0 ≫ 𝟙 (cokernel f)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.97646, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₂.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + φ₁.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.97646, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₂.τ₁ = -S₁.f ≫ h.h₁ + -h.h₀ + (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.97646, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₂.τ₂ = S₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + φ₁.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.97646, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₂.τ₂ = -S₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.97646, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₂.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + φ₁.τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.97646, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₂.τ₃ = -h.h₃ + -h.h₂ ≫ S₂.g + (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃)
<VAR>α : Type u_1<VAR>inst✝ : NonAssocRing α<VAR>m : ℤ<GOAL>∀ (n : ℤ), ↑(m * n) = ↑m * ↑n
<VAR>α : Type u_1<VAR>inst✝ : NonAssocRing α<VAR>m : ℕ<GOAL>∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n
<VAR>α : Type u_1<VAR>inst✝ : NonAssocRing α<VAR>m : ℕ<GOAL>∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>M : Matroid α<GOAL>M = loopyOn M.E ∨ M.RkPos
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>M : Matroid α<GOAL>M.Base ∅ ∨ ¬M.Base ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>la : Filter α<VAR>lb : Filter β<VAR>p : α → β → Prop<VAR>h✝ : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y<VAR>h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬(fun xy => p xy.1 xy.2) x<GOAL>∀ᶠ (x : α) in la, ¬(fun x => ∃ᶠ (y : β) in lb, p x y) x
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>ι : Type u_1<VAR>S : ι → L[[α]].Theory<VAR>x✝ : T.CompleteType α<GOAL>x✝ ∈ ⋂ i, {p | S i ⊆ ↑p} ↔ x✝ ∈ {p | ⋃ i, S i ⊆ ↑p}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>h : DifferentiableAt ℂ f z<VAR>hf' : deriv f z ≠ 0<GOAL>ConformalAt f z
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>h : DifferentiableAt ℂ f z<VAR>hf' : deriv f z ≠ 0<GOAL>IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<VAR>f : ℂ → E<VAR>h : DifferentiableAt ℂ f z<VAR>hf' : deriv f z ≠ 0<GOAL>fderiv ℂ f z ≠ 0
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n✝ n : ℕ+<VAR>hn : Fintype.card ↥(rootsOfUnity n L) = ↑n<VAR>g : L ≃+* L<VAR>c : ZMod ↑n<VAR>hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val<GOAL>c = (ZMod.ringEquivCongr hn) (toFun n g)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set (α × α)<VAR>ht₁ : t ∈ 𝓤 α<VAR>ht₂ : t ○ t ⊆ s<GOAL>∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set (α × α)<VAR>ht₁ : t ∈ 𝓤 α<VAR>ht₂ : t ○ t ⊆ s<VAR>u : Set (α × α)<VAR>hu₄ : u ⊆ t<VAR>hu₁ : u ∈ 𝓤 α<VAR>hu₂ : IsOpen u<VAR>hu₃ : SymmetricRel u<GOAL>∃ t ∈ 𝓤 α, IsOpen t ∧ SymmetricRel t ∧ t ○ t ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>Continuous ⇑T
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<GOAL>y = T x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<GOAL>⟪y - T x, y - T x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<VAR>hlhs : ∀ (k : ℕ), ⟪T (u k) - T x, y - T x⟫_𝕜 = ⟪u k - x, T (y - T x)⟫_𝕜<GOAL>⟪y - T x, y - T x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<VAR>hlhs : ∀ (k : ℕ), ⟪T (u k) - T x, y - T x⟫_𝕜 = ⟪u k - x, T (y - T x)⟫_𝕜<GOAL>Filter.Tendsto (fun t => ⟪(⇑T ∘ u) t - T x, y - T x⟫_𝕜) Filter.atTop (nhds 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<VAR>hlhs : ∀ (k : ℕ), ⟪T (u k) - T x, y - T x⟫_𝕜 = ⟪u k - x, T (y - T x)⟫_𝕜<GOAL>Filter.Tendsto (fun t => ⟪u t - x, T (y - T x)⟫_𝕜) Filter.atTop (nhds 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<VAR>hlhs : ∀ (k : ℕ), ⟪T (u k) - T x, y - T x⟫_𝕜 = ⟪u k - x, T (y - T x)⟫_𝕜<GOAL>Filter.Tendsto (fun t => ⟪u t - x, T (y - T x)⟫_𝕜) Filter.atTop (nhds ⟪0, T (y - T x)⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<VAR>hlhs : ∀ (k : ℕ), ⟪T (u k) - T x, y - T x⟫_𝕜 = ⟪u k - x, T (y - T x)⟫_𝕜<GOAL>Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : InnerProductSpace ℝ E'<VAR>inst✝ : CompleteSpace E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>u : ℕ → E<VAR>x y : E<VAR>hu : Filter.Tendsto u Filter.atTop (nhds x)<VAR>hTu : Filter.Tendsto (⇑T ∘ u) Filter.atTop (nhds y)<VAR>hlhs : ∀ (k : ℕ), ⟪T (u k) - T x, y - T x⟫_𝕜 = ⟪u k - x, T (y - T x)⟫_𝕜<GOAL>Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds (x - x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : SubtractionMonoid β<VAR>h : Antiperiodic f c<VAR>hi : f 0 = 0<VAR>n : ℕ<GOAL>f (↑↑n * c) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : SubtractionMonoid β<VAR>h : Antiperiodic f c<VAR>hi : f 0 = 0<VAR>n : ℕ<GOAL>f (↑(Int.negSucc n) * c) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>hf : Cauchy f<VAR>adhs : ClusterPt x f<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>hf : Cauchy f<VAR>adhs : ClusterPt x f<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set α<VAR>t_mem : t ∈ f<VAR>ht : t ×ˢ t ⊆ s<GOAL>∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>hf : Cauchy f<VAR>adhs : ClusterPt x f<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>t : Set α<VAR>t_mem : t ∈ f<VAR>ht : t ×ˢ t ⊆ s<GOAL>∃ y, (x, y) ∈ s ∧ y ∈ t
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hdeg : finSepDegree F E = 1<GOAL>IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hdeg : finSepDegree F E = 1<GOAL>∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hdeg : finSepDegree F E = 1<VAR>x : E<VAR>hsep : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hdeg : finSepDegree F E = 1<VAR>x : E<VAR>hsep : IsSeparable F x<VAR>this : Algebra.IsAlgebraic (↥F⟮x⟯) E<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hdeg : finSepDegree F E = 1<VAR>x : E<VAR>hsep : IsSeparable F x<VAR>this✝ : Algebra.IsAlgebraic (↥F⟮x⟯) E<VAR>this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hdeg : finSepDegree F E = 1<VAR>x : E<VAR>hsep : IsSeparable F x<VAR>this✝ : Algebra.IsAlgebraic (↥F⟮x⟯) E<VAR>this : F⟮x⟯ = ⊥ ∧ finSepDegree (↥F⟮x⟯) E = 1<GOAL>x ∈ (algebraMap F E).range
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>h : IsNilpotent y<GOAL>IsNilpotent (x * y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>h : IsNilpotent y<GOAL>IsNilpotent (y * x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1✝ : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f1 f2 : α →₀ M<VAR>g1 g2 : α → M → N<VAR>h1 : f1.support ⊆ f2.support<VAR>h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)<GOAL>f1.prod g1 ∣ f2.prod g2
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<GOAL>⨆ n, ↑(partitionFiltration ht) n = generateFrom (Set.range t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<GOAL>⨆ n, ↑(partitionFiltration ht) n = ⨆ i, generateFrom (memPartition t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a b : K<GOAL>-1 * -1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).Basis (⇑f '' I) (⇑f '' X)
<VAR>θ : Angle<GOAL>0 ≤ θ.toReal ↔ 0 ≤ θ.sign
<VAR>θ : Angle<VAR>h : θ.toReal < 0<GOAL>0 ≤ θ.toReal ↔ 0 ≤ θ.sign
<VAR>θ : Angle<VAR>h : θ.toReal = 0<GOAL>0 ≤ θ.toReal ↔ 0 ≤ θ.sign
<VAR>θ : Angle<VAR>h : 0 < θ.toReal<GOAL>0 ≤ θ.toReal ↔ 0 ≤ θ.sign
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>s : Set α<VAR>f : α → β<VAR>this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s := { prf := fun y x => match x with | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }<VAR>t : Finset ↑s<GOAL>∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>s : Set α<VAR>f : α → β<VAR>this : CanLift β (↑s) (f ∘ Subtype.val) fun y => y ∈ f '' s := { prf := fun y x => match x with | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }<VAR>t : Finset ↑s<GOAL>image f (map (Embedding.subtype fun x => x ∈ s) t) = image (f ∘ Subtype.val) t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<GOAL>vectorSpan k (range p) = Submodule.span k (range fun i => p ↑i -ᵥ p i₀)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<GOAL>Submodule.span k ((fun x => x -ᵥ p i₀) '' (p '' (univ \ {i₀}))) = Submodule.span k (range fun i => p ↑i -ᵥ p i₀)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<VAR>v : V<GOAL>v ∈ (fun x => x -ᵥ p i₀) '' (p '' (univ \ {i₀})) ↔ v ∈ range fun i => p ↑i -ᵥ p i₀