ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx : x ∈ I ⊔ J<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx⟩, ↑n⁆ = m<GOAL>m ∈ ↑(⁅I, N⁆ ⊔ ⁅J, N⁆)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx : x ∈ I ⊔ J<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx⟩, ↑n⁆ = m<GOAL>∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx✝ : x ∈ I ⊔ J<VAR>hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx✝⟩, ↑n⁆ = m<GOAL>∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx : x ∈ I ⊔ J<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx⟩, ↑n⁆ = m<VAR>x₁ : L<VAR>hx₁ : x₁ ∈ I<VAR>x₂ : L<VAR>hx₂ : x₂ ∈ J<VAR>hx' : x₁ + x₂ = x<GOAL>∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx : x ∈ I ⊔ J<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx⟩, ↑n⁆ = m<VAR>x₁ : L<VAR>hx₁ : x₁ ∈ I<VAR>x₂ : L<VAR>hx₂ : x₂ ∈ J<VAR>hx' : x₁ + x₂ = x<GOAL>⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆ ∧ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx : x ∈ I ⊔ J<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx⟩, ↑n⁆ = m<VAR>x₁ : L<VAR>hx₁ : x₁ ∈ I<VAR>x₂ : L<VAR>hx₂ : x₂ ∈ J<VAR>hx' : x₁ + x₂ = x<GOAL>∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<VAR>m : M<VAR>x : L<VAR>hx : x ∈ I ⊔ J<VAR>n : ↥N<VAR>h : ⁅↑⟨x, hx⟩, ↑n⁆ = m<VAR>x₁ : L<VAR>hx₁ : x₁ ∈ I<VAR>x₂ : L<VAR>hx₂ : x₂ ∈ J<VAR>hx' : x₁ + x₂ = x<GOAL>⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆ ∧ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m
<VAR>x : ℤ<GOAL>IsUnit x ↔ |x| = 1
<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✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → β<VAR>s : β<VAR>hx : x ∉ t<GOAL>⨆ i ∈ insert x t, update f x s i = s ⊔ ⨆ i ∈ t, f i
<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✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → β<VAR>s : β<VAR>hx : x ∉ t<GOAL>s ⊔ ⨆ x_1 ∈ t, update f x s x_1 = s ⊔ ⨆ i ∈ t, f i
<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✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → β<VAR>s : β<VAR>hx : x ∉ t<VAR>i : α<VAR>hi : i ∈ t<GOAL>update f x s i = f i
<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✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>t : Finset α<VAR>f : α → β<VAR>s : β<VAR>hx : x ∉ t<VAR>i : α<VAR>hi : i ∈ t<GOAL>i ≠ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s t✝ u : Finset α<VAR>ha : a ∉ s<VAR>𝒜 : Finset (Finset α)<VAR>t : Finset α<GOAL>t ∈ filter (fun t => t.erase a = s) 𝒜 ↔ t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>I.incl.IsIdealMorphism
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>lieIdealSubalgebra R L I = I.incl.range
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioi 0<GOAL>log x / x ^ (-r) = (fun x => log x * x ^ r) x
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>h : b < 1<GOAL>a * b < a
<VAR>A : Class<VAR>hA : A.powerset ⊆ A<GOAL>∀ (x : ZFSet), A x
<VAR>A : Class<VAR>hA : A.powerset ⊆ A<VAR>hnA : ∃ x, ¬A x<GOAL>False
<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>d : ℕ<GOAL>invOneSubPow d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ (d + 1)
<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>d : ℕ<GOAL>invOneSubPow d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1))⁻¹
<VAR>m n a b c d : ℤ<GOAL>a ≡ b [ZMOD 0] ↔ a = b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>¬a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s<GOAL>infDist x s ≤ dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s<GOAL>(infEdist x s).toReal ≤ (edist x y).toReal
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_3, u_2} D<VAR>inst✝ : Preadditive D<VAR>F G : C ⥤ D<VAR>X : C<VAR>α : F ⟶ G<VAR>n : ℤˣ<GOAL>(n • α).app X = n • α.app X
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<GOAL>⨅ k, lowerCentralSeries R L M k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L M k = ⊥<GOAL>⨅ k, lowerCentralSeries R L M k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L M k = ⊥<GOAL>⨅ k, lowerCentralSeries R L M k ≤ lowerCentralSeries R L M k
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<GOAL>(frobenius (ZMod p) p) a = (RingHom.id (ZMod p)) a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>0 < (B (P.root i)) (P.root j) ↔ 0 < P.pairing i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<VAR>h : 0 < (B (P.root i)) (P.root j)<GOAL>0 < P.pairing i j * (B (P.root j)) (P.root j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<VAR>h : 0 < P.pairing i j<GOAL>0 < 2 * (B (P.root i)) (P.root j)
<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✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x✝ y✝ : E<VAR>r✝ : ℝ<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>y ∈ p.closedBall x r ↔ y ∈ ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ
<VAR>x : PartENat<GOAL>x ≠ ⊤ ↔ x.Dom
<VAR>α : Type u<VAR>inst✝ : CommMonoid α<VAR>x y : α<VAR>ux uy : αˣ<GOAL>x /ₚ ux * (y /ₚ uy) = x * y /ₚ (ux * uy)
<VAR>R : Type u_1<VAR>inst✝¹² : Semiring R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>N' : Type u_6<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>a : M [⋀^ι]→ₗ[R] N'<GOAL>MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a
<VAR>R : Type u_1<VAR>inst✝¹² : Semiring R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>N' : Type u_6<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>a : M [⋀^ι]→ₗ[R] N'<GOAL>⇑(MultilinearMap.alternatization ↑a) = ⇑((Fintype.card ι).factorial • a)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<GOAL>∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>σ : Equiv.Perm α<VAR>s : Finset α<VAR>f : α → α → β<VAR>hs : {a | σ a ≠ a} ⊆ ↑s<VAR>x✝ : α<VAR>a✝ : x✝ ∈ s<GOAL>x✝ = (Equiv.symm σ) (σ x✝)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).WellFoundedOn r ↔ s.WellFoundedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<GOAL>f.SameCycle x (f⁻¹ y) ↔ f.SameCycle x y
<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>r : α → α → Prop<VAR>a b c d : α<VAR>r' : α → α → Prop<VAR>hr' : Transitive r'<VAR>h : ∀ (x y : α), r x y → r' x y<VAR>x y : α<VAR>hxy : TransGen r x y<GOAL>r' x y
<VAR>δ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : δ → α → β → δ<VAR>init : δ<VAR>l : AssocList α β<GOAL>foldl f init l = List.foldl (fun d x => match x with | (a, b) => f d a b) init l.toList
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>C : G.ConnectedComponent<GOAL>map Hom.id C = C
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>C : G.ConnectedComponent<GOAL>∀ (v : V), map Hom.id (G.connectedComponentMk v) = G.connectedComponentMk v
<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>inst✝ : IsFiniteMeasure μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>ε : ℝ≥0∞<VAR>h : μ s ≤ μ t + ε<GOAL>μ tᶜ ≤ μ sᶜ + ε
<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>inst✝ : IsFiniteMeasure μ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>ε : ℝ≥0∞<VAR>h : μ s ≤ μ t + ε<GOAL>μ univ ≤ μ univ - μ s + ε + μ t
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ (X ⊗ Y) Z).hom = (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom = (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>((α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom) ≫ (α_ Z X Y).inv = ((α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom) ≫ (α_ Z X Y).inv
<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>T T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f
<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>T T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ filter (fun x => x ≠ 0) f.range, (T'' (↑f ⁻¹' {x})) x = ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (↑f ⁻¹' {x})) x + ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T' (↑f ⁻¹' {x})) x
<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>T T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∀ x ∈ filter (fun x => x ≠ 0) f.range, T'' (↑f ⁻¹' {x}) = T (↑f ⁻¹' {x}) + T' (↑f ⁻¹' {x})
<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>T T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>hx : x ∈ filter (fun x => x ≠ 0) f.range<GOAL>T'' (↑f ⁻¹' {x}) = T (↑f ⁻¹' {x}) + T' (↑f ⁻¹' {x})
<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>T T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>hx : x ∈ filter (fun x => x ≠ 0) f.range<GOAL>x ≠ 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>T T' T'' : Set α → E →L[ℝ] F<VAR>h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>hx : x ∈ f.range ∧ x ≠ 0<GOAL>x ≠ 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : a < b<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-a)<VAR>this : log =o[𝓝[>] 0] fun t => t ^ (a - b)<GOAL>(fun t => log t • f t) =O[𝓝[>] 0] fun x => x ^ (-b)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : a < b<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-a)<VAR>this : log =o[𝓝[>] 0] fun t => t ^ (a - b)<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>(fun x => x ^ (a - b) • x ^ (-a)) t = (fun x => x ^ (-b)) t
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : a < b<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-a)<VAR>this : log =o[𝓝[>] 0] fun t => t ^ (a - b)<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>t ^ (a - b + -a) = t ^ (-b)
<VAR>x y : ℝ<VAR>hy : 0 ≤ y<GOAL>√x ≤ y ↔ x ≤ y ^ 2
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>(((𝟙 (N₁.obj (Γ₀.obj K)) ≫ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K))) ≫ 𝟙 ((toKaroubi (ChainComplex C ℕ)).obj (Γ₀.splitting K).nondegComplex)) ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K)) ≫ 𝟙 ((toKaroubi (ChainComplex C ℕ)).obj K) = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K)) ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K) = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : t ∈ 𝓝[s] x<GOAL>HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>g : M →ₗ[R] M<VAR>f : (M →ₗ[R] M)ˣ<GOAL>(trace R M) (↑f * g * ↑f⁻¹) = (trace R M) g
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>g : M →ₗ[R] M<VAR>f : (M →ₗ[R] M)ˣ<GOAL>(trace R M) (↑f⁻¹ * (↑f * g)) = (trace R M) g
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, Measurable f<GOAL>Measurable fun x => (map (fun f => f x) l).prod