ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>r : R<VAR>x : M ⊗[R] N<VAR>p : M<VAR>q : N<GOAL>(liftAux f) (r • p ⊗ₜ[R] q) = r • (liftAux f) (p ⊗ₜ[R] q)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>r : R<VAR>x p q : M ⊗[R] N<VAR>ih1 : (liftAux f) (r • p) = r • (liftAux f) p<VAR>ih2 : (liftAux f) (r • q) = r • (liftAux f) q<GOAL>(liftAux f) (r • (p + q)) = r • (liftAux f) (p + q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁹ : UniformSpace α<VAR>inst✝⁸ : Group α<VAR>inst✝⁷ : UniformGroup α<VAR>inst✝⁶ : Group β<VAR>γ : Type u_3<VAR>inst✝⁵ : Group γ<VAR>inst✝⁴ : UniformSpace γ<VAR>inst✝³ : UniformGroup γ<VAR>inst✝² : UniformSpace β<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : MonoidHomClass F β γ<VAR>f : F<VAR>hf : UniformInducing ⇑f<GOAL>UniformContinuous fun p => p.1 / p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁹ : UniformSpace α<VAR>inst✝⁸ : Group α<VAR>inst✝⁷ : UniformGroup α<VAR>inst✝⁶ : Group β<VAR>γ : Type u_3<VAR>inst✝⁵ : Group γ<VAR>inst✝⁴ : UniformSpace γ<VAR>inst✝³ : UniformGroup γ<VAR>inst✝² : UniformSpace β<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : MonoidHomClass F β γ<VAR>f : F<VAR>hf : UniformInducing ⇑f<GOAL>UniformContinuous fun x => f x.1 / f x.2
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<VAR>hd' : Disjoint (⇑ofDual ⁻¹' s) (closure (⇑ofDual ⁻¹' t))<VAR>ha' : toDual a ∈ ⇑ofDual ⁻¹' s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>n : σ<VAR>f g : MvPolynomial σ R<GOAL>degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>n : σ<VAR>f g : MvPolynomial σ R<GOAL>((f + g).support.sup fun m => m n) ≤ max (f.support.sup fun m => m n) (g.support.sup fun m => m n)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝² : Category.{u_2, u_1} D<VAR>P : MorphismProperty D<VAR>inst✝¹ : P.RespectsIso<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<GOAL>(P.inverseImage F).map F = P
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<GOAL>Continuous fun x => ⋯.unit
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<VAR>x : X<GOAL>ContinuousAt (fun x => ↑((fun x => ⋯.unit) x)⁻¹) x
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<VAR>x : X<VAR>this : ContinuousAt Ring.inverse ↑⋯.unit<GOAL>ContinuousAt (fun x => ↑((fun x => ⋯.unit) x)⁻¹) x
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<VAR>x : X<VAR>this : ContinuousAt Ring.inverse ↑⋯.unit<GOAL>ContinuousAt (fun x => ↑⋯.unit⁻¹) x
<VAR>X : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f : C(X, R)<VAR>h : ∀ (x : X), IsUnit (f x)<VAR>x : X<VAR>this : ContinuousAt Ring.inverse (f x)<GOAL>ContinuousAt (fun x => Ring.inverse (f x)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : a - b < c<GOAL>a < b + c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>h : a - b < c<GOAL>a - b ≤ c ∧ a ≠ b + c
<VAR>x : ℝ<VAR>hx0 : 0 < x<VAR>hx : x ≤ 1<GOAL>|x| ≤ 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✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>IsSelfAdjoint (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U)))))
<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✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>IsSelfAdjoint ((U.subtypeL.comp (orthogonalProjection U)).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))
<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✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>IsSelfAdjoint ((adjoint (U.subtypeL.comp (orthogonalProjection U))).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : DenselyOrdered α<VAR>a b c : α<VAR>h : ∀ (ε : α), 1 < ε → a / ε ≤ b<VAR>ε : α<VAR>ε1 : ε < 1<GOAL>a * ε ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => f x + g x) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => g x + f x) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>t : Set α<VAR>a b : α<VAR>inst✝ : Preorder α<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsLeast {a} a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f : α → M<VAR>n : ℕ<GOAL>∑ i ∈ range n, i = n * (n - 1) / 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ 0 C<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 hT = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ 0 C<VAR>f : ↥(Lp E 1 μ)<GOAL>ContinuousLinearMap.comp 0 (coeToLp α E ℝ) = setToL1SCLM α E μ hT
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ 0 C<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>(ContinuousLinearMap.comp 0 (coeToLp α E ℝ)) f = (setToL1SCLM α E μ hT) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>S : Set (Set α)<VAR>hs : S.Countable<VAR>hd : S.Pairwise (AEDisjoint μ)<VAR>h : ∀ s ∈ S, NullMeasurableSet s μ<GOAL>μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h : Epi (cyclesMap φ)<GOAL>Epi (homologyMap φ)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h : Epi (cyclesMap φ)<VAR>this : Epi (S₁.homologyπ ≫ homologyMap φ)<GOAL>Epi (homologyMap φ)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<GOAL>derivative (C a) = 0
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<GOAL>exterior {a} ⊆ t ↔ t ∈ 𝓝 a
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : DecidableEq F<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ ↑(Monoid.orderUnits F)<GOAL>Fintype.card Fˣ ∣ Fintype.card F - 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S F : IntermediateField K L<VAR>E : IntermediateField K ↥F<VAR>x : ↥F<VAR>left✝ : x ∈ ↑E.toSubsemiring<GOAL>↑F.val x ∈ F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<GOAL>Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<GOAL>(∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>K : Set Y<VAR>x✝ : IsCompact K<GOAL>(∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Nontrivial R<VAR>h : 1 < Fintype.card n<GOAL>¬IsLieAbelian ↥(sl n R)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Nontrivial R<VAR>h : 1 < Fintype.card n<VAR>j i : n<VAR>hij : j ≠ i<GOAL>¬IsLieAbelian ↥(sl n R)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Nontrivial R<VAR>h : 1 < Fintype.card n<VAR>j i : n<VAR>hij : j ≠ i<VAR>A : ↥(sl n R) := Eb R i j hij<GOAL>¬IsLieAbelian ↥(sl n R)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Nontrivial R<VAR>h : 1 < Fintype.card n<VAR>j i : n<VAR>hij : j ≠ i<VAR>A : ↥(sl n R) := Eb R i j hij<VAR>B : ↥(sl n R) := Eb R j i ⋯<GOAL>¬IsLieAbelian ↥(sl n R)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Nontrivial R<VAR>h : 1 < Fintype.card n<VAR>j i : n<VAR>hij : j ≠ i<VAR>A : ↥(sl n R) := Eb R i j hij<VAR>B : ↥(sl n R) := Eb R j i ⋯<VAR>c : IsLieAbelian ↥(sl n R)<GOAL>False
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Nontrivial R<VAR>h : 1 < Fintype.card n<VAR>j i : n<VAR>hij : j ≠ i<VAR>A : ↥(sl n R) := Eb R i j hij<VAR>B : ↥(sl n R) := Eb R j i ⋯<VAR>c : IsLieAbelian ↥(sl n R)<VAR>c' : ↑A * ↑B = ↑B * ↑A<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x + t • y = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x + t • y = 0<VAR>this : ∑ i : Fin (Nat.succ 0).succ, ![s, t] i • ![x, y] i = 0 → ∀ i ∈ Finset.univ, ![s, t] i = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x + t • y = 0<VAR>this : ∀ (i : Fin (Nat.succ 0).succ), ![s, t] i = 0<GOAL>s = 0 ∧ t = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<GOAL>p.natDegree = 0 ↔ p.degree ≤ 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>n : ℤ<GOAL>logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<GOAL>logDeriv (fun x => f x ^ 0) x = ↑0 * logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : f x = 0<GOAL>logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>n : ℤ<VAR>hn : n ≠ 0<VAR>hf : f x ≠ 0<GOAL>logDeriv (fun x => f x ^ n) x = ↑n * logDeriv f x
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<VAR>hp_supr_pi : IsPiSystem (⋃ n, p n)<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<VAR>hp_supr_pi : IsPiSystem (⋃ n, p n)<VAR>p' : Set (Set Ω) := {t | MeasurableSet t}<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<VAR>hp_supr_pi : IsPiSystem (⋃ n, p n)<VAR>p' : Set (Set Ω) := {t | MeasurableSet t}<VAR>hp'_pi : IsPiSystem p'<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<VAR>hp_supr_pi : IsPiSystem (⋃ n, p n)<VAR>p' : Set (Set Ω) := {t | MeasurableSet t}<VAR>hp'_pi : IsPiSystem p'<VAR>h_gen' : m' = generateFrom p'<GOAL>Indep (⨆ i, m i) m' κ μ
<VAR>α : Type u_1<VAR>Ω✝ : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω✝<VAR>κ✝ : Kernel α Ω✝<VAR>μ✝ : Measure α<VAR>Ω : Type u_4<VAR>m : ι → MeasurableSpace Ω<VAR>m' m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>h_indep : ∀ (i : ι), Indep (m i) m' κ μ<VAR>h_le : ∀ (i : ι), m i ≤ m0<VAR>h_le' : m' ≤ m0<VAR>hm : Directed (fun x x_1 => x ≤ x_1) m<VAR>p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}<VAR>hp : ∀ (n : ι), IsPiSystem (p n)<VAR>h_gen_n : ∀ (n : ι), m n = generateFrom (p n)<VAR>hp_supr_pi : IsPiSystem (⋃ n, p n)<VAR>p' : Set (Set Ω) := {t | MeasurableSet t}<VAR>hp'_pi : IsPiSystem p'<VAR>h_gen' : m' = generateFrom p'<VAR>h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ<GOAL>Indep (⨆ i, m i) m' κ μ