ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>W : MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>L : C ⥤ D<VAR>hL : W.IsInvertedBy L<VAR>this : IsIso (L.map φ.s) := hL φ.s φ.hs<GOAL>φ.map L hL ≫ L.map φ.s = L.map φ.f
<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>m0 : MeasurableSpace α<VAR>μ : Measure α<GOAL>μ ∅ < ⊤
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>map (fun p => m p.1 p.2) (f ×ˢ g) = map₂ m f g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝ : OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>l : Filter α<VAR>hf : IsMinFilter f l a<VAR>hg : IsMaxFilter g l a<GOAL>IsMinFilter (fun x => f x - g x) l a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<GOAL>coclosedCompact X = cocompact X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<GOAL>coclosedCompact X ≤ cocompact X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<GOAL>∀ (i' : Set X), IsCompact i' → ∃ i, (IsClosed i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ
<VAR>x z : Class<VAR>hz : z ∈ x<VAR>w : ZFSet<VAR>hw : (⋂₀ x) w<GOAL>↑w ∈ z
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a✝¹ : i ∈ ↑s<VAR>j : ι<VAR>a✝ : j ∈ ↑s<VAR>hij : i ≠ j<GOAL>(_root_.Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a✝¹ : i ∈ ↑s<VAR>j : ι<VAR>a✝ : j ∈ ↑s<VAR>hij : i ≠ j<GOAL>∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a✝¹ : i ∈ ↑s<VAR>j : ι<VAR>a✝ : j ∈ ↑s<VAR>hij : i ≠ j<GOAL>∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, ⟨i, a_1⟩ = a) → ¬∃ a_2 ∈ t j, ⟨j, a_2⟩ = a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a✝¹ : i ∈ ↑s<VAR>j : ι<VAR>a✝ : j ∈ ↑s<VAR>hij : i ≠ j<VAR>y : α i<VAR>left✝¹ : y ∈ t i<VAR>z : α j<VAR>left✝ : z ∈ t j<VAR>hz' : ⟨j, z⟩ = ⟨i, y⟩<GOAL>False
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : MulAction M α<VAR>inst✝² : Mul α<VAR>r s : M<VAR>x y : α<VAR>inst✝¹ : IsScalarTower M α α<VAR>inst✝ : SMulCommClass M α α<GOAL>r • x * s • y = (r * s) • (x * y)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t : Finset β<GOAL>(interedges r s t).card + (interedges (fun x y => ¬r x y) s t).card = s.card * t.card
<VAR>A : Finset ℕ<GOAL>schnirelmannDensity ↑A = 0
<VAR>A : Finset ℕ<GOAL>schnirelmannDensity ↑A ≤ 0
<VAR>A : Finset ℕ<GOAL>∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ ↑A) (Ioc 0 n)).card / ↑n < ε
<VAR>A : Finset ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε₁ : ε ≤ 1<VAR>n : ℕ := ⌊↑A.card / ε⌋₊ + 1<GOAL>∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ ↑A) (Ioc 0 n)).card / ↑n < ε
<VAR>A : Finset ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε₁ : ε ≤ 1<VAR>n : ℕ := ⌊↑A.card / ε⌋₊ + 1<VAR>hn : 0 < n<GOAL>∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ ↑A) (Ioc 0 n)).card / ↑n < ε
<VAR>A : Finset ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε₁ : ε ≤ 1<VAR>n : ℕ := ⌊↑A.card / ε⌋₊ + 1<VAR>hn : 0 < n<GOAL>↑(filter (fun x => x ∈ ↑A) (Ioc 0 n)).card / ↑n < ε
<VAR>A : Finset ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε₁ : ε ≤ 1<VAR>n : ℕ := ⌊↑A.card / ε⌋₊ + 1<VAR>hn : 0 < n<GOAL>↑(filter (fun x => x ∈ ↑A) (Ioc 0 n)).card / ε < ↑⌊↑A.card / ε⌋₊ + 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a b ≤ toIcoMod hp a b + p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp a b ≤ toIocDiv hp a b + 1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z w : K<GOAL>normSq (z - w) = normSq z + normSq w - 2 * re (z * (starRingEnd K) w)
<VAR>a b c d m✝ n : ℤ<VAR>m : ℕ<GOAL>↑m ∣ n ↔ m ∣ n.natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupSet α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>↑(sSup s) = if ⊤ ∈ (fun a => ↑a) '' s then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupSet α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>Injective fun a => ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupSet α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>⊤ ∉ (fun a => ↑a) '' s
<VAR>x : ℝ<GOAL>(ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)
<VAR>x : ℝ<GOAL>(if x ≤ 0 then ⊥ else if False then ⊤ else ↑(Real.log (ENNReal.ofReal x).toReal)) = if x ≤ 0 then ⊥ else ↑(Real.log x)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>L R : ListBlank Γ<VAR>n : ℕ<GOAL>(mk' L R).nth ↑n = R.nth n
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : C ⥤ Type v₁<VAR>t : F.obj X<GOAL>coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : C ⥤ Type v₁<VAR>u : coyoneda.obj (op X) ⟶ F<GOAL>coyonedaEquiv.symm (F.map f (coyonedaEquiv u)) = coyoneda.map f.op ≫ coyonedaEquiv.symm (coyonedaEquiv u)
<VAR>z : ℂ<GOAL>Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
<VAR>z : ℂ<VAR>pi_ne : ↑π ≠ 0<GOAL>Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
<VAR>z : ℂ<VAR>pi_ne : ↑π ≠ 0<VAR>hs : ¬sin (↑π * z) = 0<GOAL>Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
<VAR>z : ℂ<VAR>pi_ne : ↑π ≠ 0<VAR>hs : ¬sin (↑π * z) = 0<GOAL>Tendsto (fun x => z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))
<VAR>z : ℂ<VAR>pi_ne : ↑π ≠ 0<VAR>hs : ¬sin (↑π * z) = 0<VAR>this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))<GOAL>Tendsto (fun x => z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))
<VAR>z : ℂ<VAR>pi_ne : ↑π ≠ 0<VAR>hs : ¬sin (↑π * z) = 0<VAR>this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))<GOAL>Tendsto (fun n => ↑n / (↑n + 1 - z)) atTop (𝓝 1)
<VAR>z : ℂ<VAR>pi_ne : ↑π ≠ 0<VAR>hs : ¬sin (↑π * z) = 0<VAR>this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))<GOAL>Tendsto (fun n => 1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasStrictDerivAt e e' ↑z<GOAL>HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasStrictDerivAt e e' ↑z<VAR>A : HasStrictFDerivAt ofReal' ofRealCLM z<GOAL>HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasStrictDerivAt e e' ↑z<VAR>A : HasStrictFDerivAt ofReal' ofRealCLM z<VAR>B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<GOAL>HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasStrictDerivAt e e' ↑z<VAR>A : HasStrictFDerivAt ofReal' ofRealCLM z<VAR>B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<VAR>C : HasStrictFDerivAt re reCLM (e (ofRealCLM z))<GOAL>HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasStrictDerivAt e e' ↑z<VAR>A : HasStrictFDerivAt ofReal' ofRealCLM z<VAR>B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<VAR>C : HasStrictFDerivAt re reCLM (e (ofRealCLM z))<GOAL>e'.re = (reCLM.comp ((ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')).comp ofRealCLM)) 1
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasStrictDerivAt e e' ↑z<VAR>A : HasStrictFDerivAt ofReal' ofRealCLM z<VAR>B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<VAR>C : HasStrictFDerivAt re reCLM (e (ofRealCLM z))<GOAL>e'.re = reCLM ((ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM 1))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] E<GOAL>A.IsSymmetric ↔ IsSelfAdjoint A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] E<GOAL>A = adjoint A ↔ adjoint A = A
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>H : finrank K V = finrank K V₂<VAR>f : V →ₗ[K] V₂<GOAL>Injective ⇑f ↔ Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>H : finrank K V = finrank K V₂<VAR>f : V →ₗ[K] V₂<VAR>this : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V<GOAL>Injective ⇑f ↔ Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : FiniteDimensional K V₂<VAR>H : finrank K V = finrank K V₂<VAR>f : V →ₗ[K] V₂<VAR>this : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V<GOAL>ker f = ⊥ ↔ range f = ⊤
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>x : Module.Dual R M ⊗[R] M<GOAL>(trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ a₃ : A<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : B<VAR>h₁ : b₁ = φ a₁<VAR>h₂ : b₂ = φ a₂<VAR>h₃ : b₃ = φ a₃<GOAL>HasShift.shift.map (eqToHom ⋯) = (pullbackShiftIso C φ 0 0 ⋯).inv
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>a b c : α<VAR>C : Type u_3<VAR>inst✝¹ : SetLike C (Equiv.Perm α)<VAR>inst✝ : SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : swap a b ∈ M<VAR>hbc : swap b c ∈ M<GOAL>swap a c ∈ M
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>a c : α<VAR>C : Type u_3<VAR>inst✝¹ : SetLike C (Equiv.Perm α)<VAR>inst✝ : SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : swap a a ∈ M<VAR>hbc : swap a c ∈ M<GOAL>swap a c ∈ M
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>a b c : α<VAR>C : Type u_3<VAR>inst✝¹ : SetLike C (Equiv.Perm α)<VAR>inst✝ : SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : swap a b ∈ M<VAR>hbc : swap b c ∈ M<VAR>hab' : a ≠ b<GOAL>swap a c ∈ M
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>a b : α<VAR>C : Type u_3<VAR>inst✝¹ : SetLike C (Equiv.Perm α)<VAR>inst✝ : SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : swap a b ∈ M<VAR>hab' : a ≠ b<VAR>hbc : swap b a ∈ M<GOAL>swap a a ∈ M
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>a b c : α<VAR>C : Type u_3<VAR>inst✝¹ : SetLike C (Equiv.Perm α)<VAR>inst✝ : SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : swap a b ∈ M<VAR>hbc : swap b c ∈ M<VAR>hab' : a ≠ b<VAR>hac : a ≠ c<GOAL>swap a c ∈ M
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>a b c : α<VAR>C : Type u_3<VAR>inst✝¹ : SetLike C (Equiv.Perm α)<VAR>inst✝ : SubmonoidClass C (Equiv.Perm α)<VAR>M : C<VAR>hab : swap a b ∈ M<VAR>hbc : swap b c ∈ M<VAR>hab' : a ≠ b<VAR>hac : a ≠ c<GOAL>swap b c * swap a b * swap b c ∈ M
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<GOAL>Mono S₂.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<GOAL>Mono (S₂.f ≫ e.inv.τ₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<VAR>this : Mono S₁.f<GOAL>Mono (S₂.f ≫ e.inv.τ₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<VAR>this : Mono S₁.f<GOAL>Mono (e.inv.τ₁ ≫ S₁.f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<GOAL>Epi S₂.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<GOAL>Epi (e.hom.τ₂ ≫ S₂.g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<VAR>this : Epi S₁.g<GOAL>Epi (e.hom.τ₂ ≫ S₂.g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.1347, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.ShortExact<VAR>this : Epi S₁.g<GOAL>Epi (S₁.g ≫ e.hom.τ₃)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>l : Filter α<GOAL>Tendsto (fun x => ↑(f x)) l (𝓝 ⊤) ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>l : Filter α<GOAL>(∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
<VAR>n✝ : ℕ<VAR>x : ℤ × ℤ<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>(box (n + 1)).card = 8 * (n + 1)
<VAR>n✝ : ℕ<VAR>x : ℤ × ℤ<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>(↑n.succ + 1 + ↑n.succ).toNat * (↑n.succ + 1 + ↑n.succ).toNat - (↑n + 1 + ↑n).toNat * (↑n + 1 + ↑n).toNat = 8 * (n + 1)
<VAR>n✝ : ℕ<VAR>x : ℤ × ℤ<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>(n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)
<VAR>n✝ : ℕ<VAR>x : ℤ × ℤ<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>(n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])<VAR>Hi : IntegrableOn (fun z => I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume<VAR>x : ℂ<VAR>hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅<GOAL>[[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<GOAL>IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v : Fin 2 → R<VAR>hab : IsCoprime (v 0) (v 1)<VAR>A : SL(2, R)<GOAL>IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v : Fin 2 → R<VAR>hab : IsCoprime (v 0) (v 1)<VAR>A g : SL(2, R)<VAR>hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1<GOAL>IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v : Fin 2 → R<VAR>hab : IsCoprime (v 0) (v 1)<VAR>A g : SL(2, R)<VAR>hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1<VAR>this : v = ↑g 0<GOAL>IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : Preorder ι<VAR>f : Filtration ι m<VAR>i j : ι<GOAL>MeasurableSet {ω | (fun x => i) ω ≤ j}
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>eval₂ f (↑n) p = f (eval (↑n) p)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>↑n = f ↑n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Precoherent C<VAR>X : C<VAR>S : Sieve X<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)<GOAL>S ∈ (coherentTopology C).sieves X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Precoherent C<VAR>X : C<VAR>S : Sieve X<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)<GOAL>Presieve.ofArrows Y π ≤ S.arrows
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Precoherent C<VAR>X : C<VAR>S : Sieve X<VAR>α : Type<VAR>w✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)<GOAL>Presieve.ofArrows Y π ∈ (coherentCoverage C).covering X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>s.πSummand (IndexSet.id (op [n])) ≫ (s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n = PInfty.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>s.πSummand (IndexSet.id (op [n])) ≫ (s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n = 𝟙 (K[X].X n) ≫ PInfty.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>s.πSummand (IndexSet.id (op [n])) ≫ (s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n = ∑ j : IndexSet (op [n]), (s.πSummand j ≫ (s.cofan (op [n])).inj j) ≫ PInfty.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>∀ (x : IndexSet (op [n])), x ≠ IndexSet.id (op [n]) → (s.πSummand x ≫ (s.cofan (op [n])).inj x) ≫ PInfty.f n = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<VAR>A : IndexSet (op [n])<VAR>hA : ¬A.EqId<GOAL>(s.πSummand A ≫ (s.cofan (op [n])).inj A) ≫ PInfty.f n = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<GOAL>↑(chainBotCoeff (⇑α) β') = ↑(chainBotCoeff (⇑α) β) + n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>β' : Weight K (↥H) L<VAR>n : ℤ<VAR>hβ' : ⇑β' = n • ⇑α + ⇑β<VAR>this : ⇑β' = -n • -⇑α + ⇑β<GOAL>↑(chainBotCoeff (⇑α) β') = ↑(chainBotCoeff (⇑α) β) + n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>↑q < 0 ↔ q < 0
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : IsOpen s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderiv 𝕜 f y) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : IsOpen s<GOAL>DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderiv 𝕜 f y) s