ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>hf₁ : ∀ (n : ℕ), f n ∈ s.measureOfNegatives<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<GOAL>restrict 0 Aᶜ ≤ restrict s Aᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<GOAL>∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ Aᶜ → ↑0 j ≤ ↑s j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<GOAL>↑0 C ≤ ↑s C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<VAR>hC₂ : ↑s C < ↑0 C<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<VAR>hC₂ : ↑s C < ↑0 C<VAR>D : Set α<VAR>hD₁ : MeasurableSet D<VAR>hD : D ⊆ C<VAR>hD₂ : restrict s D ≤ restrict 0 D<VAR>hD₃ : ↑s D < 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<VAR>hC₂ : ↑s C < ↑0 C<VAR>D : Set α<VAR>hD₁ : MeasurableSet D<VAR>hD : D ⊆ C<VAR>hD₂ : restrict s D ≤ restrict 0 D<VAR>hD₃ : ↑s D < 0<VAR>this : ↑s (A ∪ D) < sInf s.measureOfNegatives<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<VAR>hC₂ : ↑s C < ↑0 C<VAR>D : Set α<VAR>hD₁ : MeasurableSet D<VAR>hD : D ⊆ C<VAR>hD₂ : restrict s D ≤ restrict 0 D<VAR>hD₃ : ↑s D < 0<VAR>this : ↑s (A ∪ D) < sInf s.measureOfNegatives<GOAL>sInf s.measureOfNegatives ≤ ↑s (A ∪ D)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<VAR>hC₂ : ↑s C < ↑0 C<VAR>D : Set α<VAR>hD₁ : MeasurableSet D<VAR>hD : D ⊆ C<VAR>hD₂ : restrict s D ≤ restrict 0 D<VAR>hD₃ : ↑s D < 0<VAR>this : ↑s (A ∪ D) < sInf s.measureOfNegatives<GOAL>MeasurableSet (A ∪ D)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<VAR>f : ℕ → ℝ<VAR>left✝ : Antitone f<VAR>hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))<VAR>B : ℕ → Set α<VAR>hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ restrict s B ≤ restrict 0 B} ∧ ↑s (B n) = f n<VAR>hB₁ : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hB₂ : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hA₁ : MeasurableSet A<VAR>hA₂ : restrict s A ≤ restrict 0 A<VAR>hA₃ : ↑s A = sInf s.measureOfNegatives<VAR>C : Set α<VAR>a✝ : MeasurableSet C<VAR>hC₁ : C ⊆ Aᶜ<VAR>hC₂ : ↑s C < ↑0 C<VAR>D : Set α<VAR>hD₁ : MeasurableSet D<VAR>hD : D ⊆ C<VAR>hD₂ : restrict s D ≤ restrict 0 D<VAR>hD₃ : ↑s D < 0<VAR>this : ↑s (A ∪ D) < sInf s.measureOfNegatives<GOAL>restrict s (A ∪ D) ≤ restrict 0 (A ∪ D)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<GOAL>(starRingEnd 𝕜) (4⁻¹ * (𝓚 ‖y + x‖ * 𝓚 ‖y + x‖ - 𝓚 ‖y - x‖ * 𝓚 ‖y - x‖ + I * 𝓚 ‖I • y + x‖ * 𝓚 ‖I • y + x‖ - I * 𝓚 ‖I • y - x‖ * 𝓚 ‖I • y - x‖)) = 4⁻¹ * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<GOAL>4⁻¹ * (starRingEnd 𝕜) (𝓚 ‖y + x‖ * 𝓚 ‖y + x‖ - 𝓚 ‖y - x‖ * 𝓚 ‖y - x‖ + I * 𝓚 ‖I • y + x‖ * 𝓚 ‖I • y + x‖ - I * 𝓚 ‖I • y - x‖ * 𝓚 ‖I • y - x‖) = 4⁻¹ * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<GOAL>(starRingEnd 𝕜) (𝓚 ‖y + x‖ * 𝓚 ‖y + x‖ - 𝓚 ‖y - x‖ * 𝓚 ‖y - x‖ + I * 𝓚 ‖I • y + x‖ * 𝓚 ‖I • y + x‖ - I * 𝓚 ‖I • y - x‖ * 𝓚 ‖I • y - x‖) = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<GOAL>↑‖y + x‖ * ↑‖y + x‖ - ↑‖y - x‖ * ↑‖y - x‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<GOAL>↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<VAR>hI : ¬I = 0<GOAL>↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<VAR>hI : ¬I = 0<VAR>this : ‖I‖ = 1<GOAL>↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<VAR>hI : ¬I = 0<VAR>this : ‖I‖ = 1<VAR>h₁ : ‖I • y - x‖ = ‖I • x + y‖<VAR>h₂ : ‖I • y + x‖ = ‖I • x - y‖<GOAL>↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h4 : (starRingEnd 𝕜) 4⁻¹ = 4⁻¹<VAR>hI : ¬I = 0<VAR>this : ‖I‖ = 1<VAR>h₁ : ‖I • y - x‖ = ‖I • x + y‖<VAR>h₂ : ‖I • y + x‖ = ‖I • x - y‖<GOAL>↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ - -I * ↑‖I • x + y‖ * ↑‖I • x + y‖ + -I * ↑‖I • x - y‖ * ↑‖I • x - y‖ = 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<GOAL>∀ x ∈ f.support ∪ g.support, x ∉ f.support → h x (f x) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<VAR>f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h<GOAL>∀ x ∈ f.support ∪ g.support, x ∉ g.support → h x (g x) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<VAR>f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h<VAR>g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h<GOAL>∀ x ∈ f.support ∪ g.support, x ∉ (f + g).support → h x ((f + g) x) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<VAR>f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h<VAR>g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h<GOAL>∏ i ∈ f.support ∪ g.support, h i ((f + g) i) = (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (A ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<GOAL>∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (A ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<GOAL>ENNReal.ofReal (∫ (x : γ) in A, κ.density ν a x s ∂ν a) = (κ a) (A ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<GOAL>Integrable (fun x => κ.density ν a x s) ((ν a).restrict A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<GOAL>0 ≤ᶠ[ae ((ν a).restrict A)] fun x => κ.density ν a x s
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>this : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<GOAL>Continuous ⇑f
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<GOAL>Continuous ⇑f
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 (f 0)<GOAL>U ∈ map (⇑f) (𝓝 0)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜₁<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹⁰ : RingHomIsometric σ₁₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁹ : TopologicalSpace M₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : TopologicalSpace M₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module 𝕜₁ M₁<VAR>inst✝⁴ : Module 𝕜₂ M₂<VAR>inst✝³ : TopologicalAddGroup M₁<VAR>inst✝² : ContinuousConstSMul 𝕜₁ M₁<VAR>inst✝¹ : TopologicalAddGroup M₂<VAR>inst✝ : ContinuousSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>this✝ : UniformSpace M₂ := TopologicalAddGroup.toUniformSpace M₂<VAR>this : UniformAddGroup M₂<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<GOAL>U ∈ map (⇑f) (𝓝 0)