ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ filter p s ∪ filter q s ↔ x ∈ filter (fun x => p x ∨ q x) s
<VAR>R : 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✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : 0 ∉ t<GOAL>t ∈ Filter.map (s.indicator f) (ae μ) → t ∈ Filter.map f (ae (μ.restrict s))
<VAR>R : 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✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : 0 ∉ t<GOAL>μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → μ ((f ⁻¹' t)ᶜ ∩ s) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : ¬IsUnit ((aeval x) (derivative P))<GOAL>P.newtonMap x = 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>s : Finset α<VAR>t : Finset γ<VAR>f : α ⊕ γ → β<GOAL>∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr 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>s : Finset α<VAR>t : Finset γ<VAR>f : α ⊕ γ → β<GOAL>(∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ t, f (Embedding.inr x) = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<GOAL>ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<GOAL>∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<GOAL>(fun a => μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (a ^ (p - 1))) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => μ {a_1 | a < f a_1} * ENNReal.ofReal (a ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>t : ℝ<VAR>ht : μ {a | t ≤ f a} = μ {a | t < f a}<GOAL>μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) = μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>(fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>Complex.exp (↑2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in atTop, Codisjoint (ker (f ^ n)) (range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<GOAL>∀ᶠ (n : ℕ) in atTop, Codisjoint (ker (f ^ n)) (range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<GOAL>ker (f ^ m) ⊔ range (f ^ m) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<GOAL>∀ (x : M), ∃ y ∈ ker (f ^ m), ∃ z ∈ range (f ^ n), y + z = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>x : M<GOAL>∃ y, (f ^ m) ((f ^ n) y) = (f ^ m) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>x : M<GOAL>(f ^ m) x ∈ range (f ^ m)
<VAR>a : ℤ<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : J(a | p) = 1<GOAL>¬¬IsSquare ↑a
<VAR>a : ℤ<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>h : J(a | p) = 1<GOAL>¬1 = -1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<GOAL>(∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → M<VAR>comm : (↑t).Pairwise fun a b => Commute (f a) (f b)<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>t.noncommProd f comm ∈ S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → M<VAR>comm : (↑t).Pairwise fun a b => Commute (f a) (f b)<VAR>h : ∀ c ∈ t, f c ∈ S<GOAL>∀ x ∈ Multiset.map f t.val, x ∈ S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → M<VAR>comm : (↑t).Pairwise fun a b => Commute (f a) (f b)<VAR>h : ∀ c ∈ t, f c ∈ S<VAR>y : M<GOAL>y ∈ Multiset.map f t.val → y ∈ S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S✝ : B<VAR>s S : Submonoid M<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>f : ι → M<VAR>comm : (↑t).Pairwise fun a b => Commute (f a) (f b)<VAR>h : ∀ c ∈ t, f c ∈ S<VAR>y : M<GOAL>(∃ a ∈ t.val, f a = y) → y ∈ S
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>H : ¬s.Terminates<GOAL>s = empty α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>H : ¬s.Terminates<GOAL>↑s = ↑(empty α)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>H : ¬s.Terminates<VAR>n : ℕ<GOAL>↑s n = ↑(empty α) n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>H : ¬s.Terminates<VAR>n : ℕ<VAR>val✝ : α<VAR>h : ↑s n = some val✝<GOAL>s.Terminates
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemiring α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y : α<VAR>hx : 1 ≤ x<VAR>hy : 1 < y<GOAL>∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemiring α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y : α<VAR>hx : 1 ≤ x<VAR>hy : 1 < y<VAR>h : ∃ n, x < y ^ n<GOAL>∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<GOAL>thickenedIndicatorAux δ E x = 1
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 1, K * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ V ∈ 𝓝 1, ∅ * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : MulOneClass G<VAR>inst✝ : ContinuousMul G<VAR>K U : Set G<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<GOAL>FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) ^ 2 * ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 = FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3
<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>M : Type u_7<VAR>N : Type u_8<VAR>inst✝⁴ : LinearOrderedSemifield 𝕜<VAR>inst✝³ : OrderedAddCommMonoid M<VAR>inst✝² : OrderedAddCommMonoid N<VAR>inst✝¹ : MulActionWithZero 𝕜 M<VAR>inst✝ : MulActionWithZero 𝕜 N<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<GOAL>OrderedSMul 𝕜 M
<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>M : Type u_7<VAR>N : Type u_8<VAR>inst✝⁴ : LinearOrderedSemifield 𝕜<VAR>inst✝³ : OrderedAddCommMonoid M<VAR>inst✝² : OrderedAddCommMonoid N<VAR>inst✝¹ : MulActionWithZero 𝕜 M<VAR>inst✝ : MulActionWithZero 𝕜 N<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<VAR>hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b<GOAL>OrderedSMul 𝕜 M
<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>M : Type u_7<VAR>N : Type u_8<VAR>inst✝⁴ : LinearOrderedSemifield 𝕜<VAR>inst✝³ : OrderedAddCommMonoid M<VAR>inst✝² : OrderedAddCommMonoid N<VAR>inst✝¹ : MulActionWithZero 𝕜 M<VAR>inst✝ : MulActionWithZero 𝕜 N<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<VAR>hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b<VAR>a b : M<VAR>c : 𝕜<VAR>hab : c • a < c • b<VAR>hc : 0 < c<GOAL>a < b
<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>M : Type u_7<VAR>N : Type u_8<VAR>inst✝⁴ : LinearOrderedSemifield 𝕜<VAR>inst✝³ : OrderedAddCommMonoid M<VAR>inst✝² : OrderedAddCommMonoid N<VAR>inst✝¹ : MulActionWithZero 𝕜 M<VAR>inst✝ : MulActionWithZero 𝕜 N<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<VAR>hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b<VAR>a b : M<VAR>c : 𝕜ˣ<VAR>hab : ↑c • a < ↑c • b<VAR>hc : 0 < ↑c<GOAL>a < b
<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>M : Type u_7<VAR>N : Type u_8<VAR>inst✝⁴ : LinearOrderedSemifield 𝕜<VAR>inst✝³ : OrderedAddCommMonoid M<VAR>inst✝² : OrderedAddCommMonoid N<VAR>inst✝¹ : MulActionWithZero 𝕜 M<VAR>inst✝ : MulActionWithZero 𝕜 N<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<VAR>hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b<VAR>a b : M<VAR>c : 𝕜ˣ<VAR>hab : ↑c • a < ↑c • b<VAR>hc : 0 < ↑c<GOAL>c⁻¹ • c • a < c⁻¹ • c • b
<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>M : Type u_7<VAR>N : Type u_8<VAR>inst✝⁴ : LinearOrderedSemifield 𝕜<VAR>inst✝³ : OrderedAddCommMonoid M<VAR>inst✝² : OrderedAddCommMonoid N<VAR>inst✝¹ : MulActionWithZero 𝕜 M<VAR>inst✝ : MulActionWithZero 𝕜 N<VAR>h : ∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b<VAR>hlt' : ∀ (a b : M) (c : 𝕜), a < b → 0 < c → c • a < c • b<VAR>a b : M<VAR>c : 𝕜ˣ<VAR>hab : ↑c • a < ↑c • b<VAR>hc : 0 < ↑c<GOAL>0 < ↑c * ↑c⁻¹
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist (a * b) a = ‖b‖
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁✝ a₂✝ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>h : ker f = IsSubgroup.trivial G<VAR>a₁ a₂ : G<VAR>hfa : f a₁ = f a₂<GOAL>a₁ = a₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁✝ a₂✝ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a₁ a₂ : G<VAR>hfa : f a₁ = f a₂<VAR>h : ∀ (x : G), f x = 1 ↔ x = 1<GOAL>a₁ = a₂
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁✝ a₂✝ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a₁ a₂ : G<VAR>hfa : f a₁ = f a₂<VAR>h : ∀ (x : G), f x = 1 ↔ x = 1<VAR>ha : a₁ * a₂⁻¹ = 1<GOAL>a₁ = a₂
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑‖indicatorConstLp p hs hμs c‖₊ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑(‖c‖₊ * (μ s).toNNReal ^ (1 / p.toReal)) = ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>s : Set M<GOAL>IsOpen s ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>s : Set M<GOAL>(∀ (i : M), IsOpen ((chartAt H i).source ∩ s)) ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁵ : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace α'<VAR>inst✝³ : MeasurableSpace β✝<VAR>inst✝² : MeasurableSpace β'<VAR>inst✝¹ : MeasurableSpace γ✝<VAR>μ μ' : Measure α✝<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ✝<VAR>inst✝ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>hg : MeasurableEmbedding g<VAR>hf : MeasurableEmbedding f<GOAL>MeasurableEmbedding fun x => (g x.1, f x.2)
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁵ : MeasurableSpace α✝<VAR>inst✝⁴ : MeasurableSpace α'<VAR>inst✝³ : MeasurableSpace β✝<VAR>inst✝² : MeasurableSpace β'<VAR>inst✝¹ : MeasurableSpace γ✝<VAR>μ μ' : Measure α✝<VAR>ν ν' : Measure β✝<VAR>τ : Measure γ✝<VAR>inst✝ : NormedAddCommGroup E<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>hg : MeasurableEmbedding g<VAR>hf : MeasurableEmbedding f<VAR>h_inj : Injective fun x => (g x.1, f x.2)<GOAL>MeasurableEmbedding fun x => (g x.1, f x.2)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>X✝ Y✝ : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f✝ = eqToHom ⋯ ≫ (generateEquivalenceOpensLe_functor' U ?m.36385 ⋙ generateEquivalenceOpensLe_inverse' U ?m.36432).map f✝ ≫ eqToHom ⋯
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>X✝ Y✝ : FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom<VAR>f✝ : X✝ ⟶ Y✝<GOAL>((𝟭 (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).map f✝).left = (eqToHom ⋯ ≫ (generateEquivalenceOpensLe_functor' U ?m.36385 ⋙ generateEquivalenceOpensLe_inverse' U ?m.36432).map f✝ ≫ eqToHom ⋯).left
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j x : Fin n<VAR>y : Fin (n + 1)<VAR>h : y ≤ x.castSucc<VAR>h' : optParam (y.succAbove x ≠ 0) ⋯<GOAL>(y.succAbove x).pred h' = x
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K V = lift.{u, u} (Module.rank K V)
<VAR>S : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasShift C S<VAR>inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms<VAR>X Y : DifferentialObject S C<VAR>f : X.obj ≅ Y.obj<VAR>hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d<GOAL>Y.d ≫ (shiftFunctor C 1).map f.inv = f.inv ≫ X.d
<VAR>S : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasShift C S<VAR>inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms<VAR>X Y : DifferentialObject S C<VAR>f : X.obj ≅ Y.obj<VAR>hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d<GOAL>autoParam (f.hom ≫ f.inv = 𝟙 X.obj) _auto✝
<VAR>S : Type u_1<VAR>inst✝⁴ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasShift C S<VAR>inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms<VAR>X Y : DifferentialObject S C<VAR>f : X.obj ≅ Y.obj<VAR>hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d<GOAL>autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) _auto✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : s.Countable<GOAL>∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in ⋃ x ∈ s, {x}, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : s.Countable<GOAL>∑' (a : ↑s), ∫⁻ (x : α) in {↑a}, f x ∂μ = ∑' (a : ↑s), f ↑a * μ {↑a}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>n a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * 0 + b * (0 + 1) = s.card<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = 0 ∨ x.card = 0 + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ 0) ∧ (filter (fun i => i.card = 0 + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>m n a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>m_pos : m > 0<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t : Finset α<VAR>m n : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : ¬(a = 0 ∧ b = 0)<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t : Finset α<VAR>m n : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>t✝ : Finset α<VAR>m n✝ : ℕ<VAR>m_pos : m > 0<VAR>s : Finset α<VAR>ih : ∀ t ⊂ s, ∀ {a b : ℕ} {P : Finpartition t}, a * m + b * (m + 1) = t.card → ∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b<VAR>a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<VAR>hab : 0 < a ∨ 0 < b<VAR>n : ℕ := if 0 < a then m else m + 1<VAR>hn : n = if 0 < a then m else m + 1<VAR>hn₀ : 0 < n<VAR>hn₁ : n ≤ m + 1<VAR>hn₂ : n ≤ a * m + b * (m + 1)<VAR>hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = s.card - n<VAR>u : Finset α<VAR>hu₁ : u ∈ P.parts<VAR>hu₂ : m + 1 ≤ u.card<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>htn : t.card = n<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (filter (fun i => i.card = m + 1) Q.parts).card = b