ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>f : ↥(simpleFunc G 1 μ)<VAR>h_eq : ∀ (a : α), ↑(SimpleFunc.map (fun x => ↑‖x‖₊) (toSimpleFunc f)) a = ↑‖↑(toSimpleFunc f) a‖₊<GOAL>∀ a ∈ (toSimpleFunc f).range, ↑‖a‖₊ * μ (↑(toSimpleFunc f) ⁻¹' {a}) ≠ ⊤
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (x + z * y) y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime (x + y * z) y<GOAL>IsCoprime x y
<VAR>a : ℂ<GOAL>↑Complex.polarCoord a = (abs a, a.arg)
<VAR>a : ℂ<GOAL>↑Complex.polarCoord a = (√(a.re ^ 2 + a.im ^ 2), a.arg)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>Scheme.Hom.app hU.fromSpec U = (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Type u_11<VAR>σ : ι → Type u_12<VAR>s : Set (Sigma σ)<VAR>x : (i : ι) × σ i<GOAL>x ∈ ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) ↔ x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Type u_11<VAR>σ : ι → Type u_12<VAR>s : Set (Sigma σ)<VAR>x : (i : ι) × σ i<GOAL>(∃ i x_1, ⟨i, x_1⟩ ∈ s ∧ ⟨i, x_1⟩ = x) ↔ x ∈ s
<GOAL>Num.ofNat' ↑1 = Num.pos 1
<GOAL>(bif true then Num.bit1 else Num.bit0) 0 = Num.pos 1
<VAR>p : PosNum<GOAL>Num.ofNat' ↑p.bit0 = Num.pos p.bit0
<VAR>p : PosNum<GOAL>Num.ofNat' ↑p.bit1 = Num.pos p.bit1
<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>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<GOAL>(AffineIndependent k fun p => ↑p) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
<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>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<GOAL>(LinearIndependent k fun i => ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>↑(Nat.factorial 1) ∈ nonZeroDivisors R
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>1 ∈ nonZeroDivisors R
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<GOAL>ker f ⊔ ker g ≤ ker (f ∘ₗ g)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<GOAL>ker f ≤ ker (f ∘ₗ g)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<GOAL>ker f ≤ ker (g ∘ₗ f)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n✝ : ℕ<VAR>x : M<VAR>hn : 0 < n✝<VAR>h : x < 1<VAR>n : ℕ<VAR>x✝ : Nat.succ 0 ≤ n<VAR>ih : x ^ n < 1<GOAL>x ^ (n + 1) < 1
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>n✝ : ℕ<VAR>x : M<VAR>hn : 0 < n✝<VAR>h : x < 1<VAR>n : ℕ<VAR>x✝ : Nat.succ 0 ≤ n<VAR>ih : x ^ n < 1<GOAL>x ^ n * x < 1
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<VAR>V : Y.Opens<VAR>W : X.Opens<VAR>e₁ : V ≤ g ⁻¹ᵁ U<VAR>e₂ : W ≤ f ⁻¹ᵁ V<GOAL>(Hom.app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ Hom.app f V ≫ X.presheaf.map (homOfLE e₂).op = (Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<VAR>V : Y.Opens<VAR>W : X.Opens<VAR>e₁ : V ≤ g ⁻¹ᵁ U<VAR>e₂ : W ≤ f ⁻¹ᵁ V<GOAL>Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.val.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) = (Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atBot<GOAL>Tendsto (fun x => r * f x) l atBot ↔ 0 < r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R B<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>r : R<VAR>f g : M →ₗ[R] N<VAR>x✝ : M<GOAL>((AlgebraTensorModule.curry (baseChange A (r • f))) 1) x✝ = ((AlgebraTensorModule.curry (r • baseChange A f)) 1) x✝
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A✝ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A✝<VAR>inst✝⁴ : TransportsGrothendieckTopology J K e<VAR>inst✝³ : HasSheafify K A✝<VAR>A : Type u_1<VAR>inst✝² : Category.{u_3, u_1} A<VAR>B : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>inst✝ : K.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : Presheaf.IsSheaf J P<GOAL>Presheaf.IsSheaf J (P ⋙ F)
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A✝ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A✝<VAR>inst✝⁴ : TransportsGrothendieckTopology J K e<VAR>inst✝³ : HasSheafify K A✝<VAR>A : Type u_1<VAR>inst✝² : Category.{u_3, u_1} A<VAR>B : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>inst✝ : K.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : Presheaf.IsSheaf J P<VAR>hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F)<GOAL>Presheaf.IsSheaf J (P ⋙ F)
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A✝ : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} A✝<VAR>inst✝⁴ : TransportsGrothendieckTopology J K e<VAR>inst✝³ : HasSheafify K A✝<VAR>A : Type u_1<VAR>inst✝² : Category.{u_3, u_1} A<VAR>B : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>inst✝ : K.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : Presheaf.IsSheaf J P<VAR>hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F)<GOAL>Presheaf.IsSheaf J (P ⋙ F)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(s.erase ⊥).sup id = s.sup id
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>id a ≤ (s.erase ⊥).sup id
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>ha : ⊥ ∈ s<GOAL>id ⊥ ≤ (s.erase ⊥).sup id
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>ha' : a ≠ ⊥<GOAL>id a ≤ (s.erase ⊥).sup id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>u : ℕ → ℝ<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>n : ℕ<VAR>h : ∀ k < n, u (k + 1) ≤ c * u k<GOAL>u n ≤ c ^ n * u 0
<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>x : L<VAR>k : ℕ<GOAL>posFittingCompOf R M x ≤ lowerCentralSeries R L M k
<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>x : L<VAR>k : ℕ<GOAL>∀ (m : M) (l : ℕ), ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
<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>x : L<VAR>k : ℕ<VAR>m : M<VAR>l : ℕ<VAR>ih : ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l<GOAL>((toEnd R L M) x ^ (l + 1)) m ∈ lowerCentralSeries R L M (l + 1)
<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>x : L<VAR>k : ℕ<VAR>m : M<VAR>l : ℕ<VAR>ih : ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l<GOAL>((toEnd R L M) x) (((toEnd R L M) x ^ l) m) ∈ ⁅⊤, lowerCentralSeries R L M l⁆
<VAR>α : Type u_1<VAR>a a' a₁ a₂ b b' b₁ b₂ c : α<VAR>inst✝ : AddGroup α<VAR>p : a = b<VAR>H : a' - b' - (a - b) = 0<GOAL>a' = b'
<VAR>α : Type u_1<VAR>a a' a₁ a₂ b b' b₁ b₂ c : α<VAR>inst✝ : AddGroup α<VAR>p : a - b = 0<VAR>H : a' - b' - (a - b) = 0<GOAL>a' - b' = 0
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>h : ↑j < ↑k<GOAL>j.contractNth op g k = g k.succ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<GOAL>μ univ < ⊤
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<GOAL>(P ∅) univ < ⊤
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<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>x : M ⊗[R] N<GOAL>-0 + 0 = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<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>x : M ⊗[R] N<GOAL>-0 = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<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>x✝ : M ⊗[R] N<VAR>x : M<VAR>y : N<GOAL>-x ⊗ₜ[R] y + x ⊗ₜ[R] y = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<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>x✝ : M ⊗[R] N<VAR>x : M<VAR>y : N<GOAL>0 = (-x + x) ⊗ₜ[R] y
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<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>x✝ x y : M ⊗[R] N<VAR>hx : -x + x = 0<VAR>hy : -y + y = 0<GOAL>-(x + y) + (x + y) = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<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>x✝ x y : M ⊗[R] N<VAR>hx : -x + x = 0<VAR>hy : -y + y = 0<GOAL>-x + x + (-y + y) = 0
<VAR>k : ℤ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => x ^ k) =o[atTop] fun x => rexp (b * x)
<VAR>l✝ : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l✝<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>k l : n<VAR>h : j ≠ k<VAR>d : α<VAR>a b : n<GOAL>(stdBasisMatrix i j c * stdBasisMatrix k l d) a b = 0 a b
<VAR>l✝ : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l✝<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>k l : n<VAR>h : j ≠ k<VAR>d : α<VAR>a b : n<GOAL>(∑ x : n, (if i = a ∧ j = x then c else 0) * if k = x ∧ l = b then d else 0) = 0 a b
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f : MulRingNorm R<GOAL>f.equiv f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n<VAR>hd : Summable fun i => ↑(d i)<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n<VAR>hd : Summable fun i => ↑(d i)<GOAL>∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n<VAR>hd : Summable fun i => ↑(d i)<GOAL>Summable d
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>inst✝ : Mono f<VAR>g₁ g₂ : ↑G<VAR>h : f g₁ = f g₂<VAR>t0 : asHom g₁ ≫ f = asHom g₂ ≫ f<GOAL>g₁ = g₂
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>inst✝ : Mono f<VAR>g₁ g₂ : ↑G<VAR>h : f g₁ = f g₂<VAR>t0 : asHom g₁ ≫ f = asHom g₂ ≫ f<VAR>t1 : asHom g₁ = asHom g₂<GOAL>g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : Measure α<VAR>a b : α<VAR>hb : μ {b} ≠ ⊤<GOAL>IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x y z : G<VAR>H : ∀ (a : G), a * x = z ↔ a = y<GOAL>(f * single x r) z = f y * r
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>h : Red (invRev L₁) (invRev L₂)<GOAL>Red L₁ L₂
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s s' : ↥S<GOAL>IsLocalization.mk' T r s • mk m s' = mk (r • m) (s * s')
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s s' : ↥S<GOAL>∃ u, u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m = u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s s' c : ↥S<VAR>hc : ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) = ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)<GOAL>∃ u, u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m = u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s s' c : ↥S<VAR>hc : ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) = ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)<GOAL>c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m = c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>p q r : Associates M<VAR>hp : Prime p<VAR>hr : r ∣ q<VAR>hp' : p ∣ r<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<GOAL>p = c 1
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>i : Fin (n + 1 + 1)<VAR>hp : Prime (c i)<VAR>hp' : c i ∣ r<GOAL>c i = c 1
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>i : Fin (n + 1 + 1)<VAR>hp : Prime (c i)<VAR>hp' : c i ∣ r<GOAL>1 ≤ i
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>i : Fin (n + 1 + 1)<VAR>hp : Prime (c i)<VAR>hp' : c i ∣ r<VAR>hi : 1 < i<GOAL>False
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>hp : Prime (c 0)<VAR>hp' : c 0 ∣ r<VAR>hi : 1 < 0<GOAL>False
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>j : Fin (n + 1)<VAR>hp : Prime (c j.succ)<VAR>hp' : c j.succ ∣ r<VAR>hi : 1 < j.succ<GOAL>False
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>j : Fin (n + 1)<VAR>hp : Prime (c j.succ)<VAR>hp' : c j.succ ∣ r<VAR>hi : 1 < j.succ<GOAL>0 < ↑↑j
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q r : Associates M<VAR>hr : r ∣ q<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>j : Fin (n + 1)<VAR>hp : Prime (c j.succ)<VAR>hp' : c j.succ ∣ r<VAR>hi : 1 < j.succ<GOAL>DvdNotUnit (c ↑↑j) (c j.succ)
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * s.radius