ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t : Set ι'<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬s.PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<VAR>hne : i ≠ j<VAR>x : α<VAR>hx₁ : x ∈ f i<VAR>hx₂ : x ∈ f j<GOAL>∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t : Set ι'<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬s.PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<VAR>hne : i ≠ j<VAR>x : α<VAR>hx₁ : x ∈ f i<VAR>hx₂ : x ∈ f j<VAR>h_lt : i < j<GOAL>∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t : Set ι'<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬s.PairwiseDisjoint f<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<VAR>hne : i ≠ j<VAR>x : α<VAR>hx₁ : x ∈ f i<VAR>hx₂ : x ∈ f j<VAR>h_lt : j < i<GOAL>∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : B<VAR>p : R[X]<GOAL>(aeval x) (map (algebraMap R A) p) = (aeval x) p
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<GOAL>CompleteSpace ↥(Lp E p μ)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<GOAL>CompleteSpace ↥(Lp E p μ)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<GOAL>∃ x, Tendsto f atTop (𝓝 x)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<VAR>M : ℝ<VAR>hB : HasSum B M<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<GOAL>∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<VAR>N n m : ℕ<VAR>hn : N ≤ n<VAR>hm : N ≤ m<GOAL>eLpNorm (f1 n - f1 m) p μ < B1 N
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<VAR>N n m : ℕ<VAR>hn : N ≤ n<VAR>hm : N ≤ m<VAR>hf : dist (f n) (f m) < B N<GOAL>eLpNorm (f1 n - f1 m) p μ < B1 N
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<VAR>N n m : ℕ<VAR>hn : N ≤ n<VAR>hm : N ≤ m<VAR>hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N<GOAL>eLpNorm (f1 n - f1 m) p μ < B1 N
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<VAR>N n m : ℕ<VAR>hn : N ≤ n<VAR>hm : N ≤ m<VAR>hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N<GOAL>eLpNorm (↑↑(f n) - ↑↑(f m)) p μ < B1 N
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<VAR>N n m : ℕ<VAR>hn : N ≤ n<VAR>hm : N ≤ m<VAR>hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N<GOAL>eLpNorm (↑↑(f n) - ↑↑(f m)) p μ ≠ ⊤
<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>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, Memℒp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)<VAR>B : ℕ → ℝ := fun n => (1 / 2) ^ n<VAR>hB_pos : ∀ (n : ℕ), 0 < B n<VAR>f : ℕ → ↥(Lp E p μ)<VAR>M : ℝ<VAR>hB : HasSum B M<VAR>B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)<VAR>hB1_has : HasSum B1 (ENNReal.ofReal M)<VAR>hB1 : ∑' (i : ℕ), B1 i < ⊤<VAR>f1 : ℕ → α → E := fun n => ↑↑(f n)<VAR>N n m : ℕ<VAR>hn : N ≤ n<VAR>hm : N ≤ m<VAR>hf : (eLpNorm (↑↑(f n) - ↑↑(f m)) p μ).toReal < B N<GOAL>eLpNorm (↑↑(f n - f m)) p μ ≠ ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h : 0 < n<VAR>x : R<GOAL>x ∈ nthRootsFinset n R ↔ x ^ n = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hNF : ¬IsField A<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : ⟨a, haI⟩ ≠ 0<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<VAR>Z : Multiset (PrimeSpectrum A)<VAR>hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<VAR>Z : Multiset (PrimeSpectrum A)<VAR>hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>b : A<VAR>hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod<VAR>hbJ : b ∉ J<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<VAR>Z : Multiset (PrimeSpectrum A)<VAR>hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>b : A<VAR>hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod<VAR>hbJ : b ∉ J<VAR>hnz_fa : (algebraMap A K) a ≠ 0<GOAL>¬(↑I)⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<VAR>Z : Multiset (PrimeSpectrum A)<VAR>hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>b : A<VAR>hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod<VAR>hbJ : b ∉ J<VAR>hnz_fa : (algebraMap A K) a ≠ 0<GOAL>↑I ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<VAR>Z : Multiset (PrimeSpectrum A)<VAR>hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>b : A<VAR>hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod<VAR>hbJ : b ∉ J<VAR>hnz_fa : (algebraMap A K) a ≠ 0<GOAL>∀ y ∈ ↑I, (algebraMap A K) b * ((algebraMap A K) a)⁻¹ * y ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I : Ideal A<VAR>hI0✝ : I ≠ ⊥<VAR>hI1 : I ≠ ⊤<VAR>hM : I.IsMaximal<VAR>hI0 : ⊥ < I<VAR>a : A<VAR>haI : a ∈ I<VAR>ha0 : a ≠ 0<VAR>J : Ideal A := span {a}<VAR>hJ0 : J ≠ ⊥<VAR>hJI : J ≤ I<VAR>Z : Multiset (PrimeSpectrum A)<VAR>hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J<VAR>b : A<VAR>hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod<VAR>hbJ : b ∉ J<VAR>hnz_fa : (algebraMap A K) a ≠ 0<GOAL>(algebraMap A K) b * ((algebraMap A K) a)⁻¹ ∉ ↑((fun a => ↑a) 1)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.420688, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯<GOAL>3 < 5 + 1
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<GOAL>↑(lp.single p i a) i = a
<VAR>q : ℚ<VAR>n₁ d₁ n₂ d₂ : ℤ<GOAL>n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)
<VAR>q : ℚ<VAR>n₁ n₂ d₂ : ℤ<GOAL>n₁ /. 0 * (n₂ /. d₂) = n₁ * n₂ /. (0 * d₂)
<VAR>q : ℚ<VAR>n₁ d₁ n₂ d₂ : ℤ<VAR>h₁ : d₁ ≠ 0<GOAL>n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)
<VAR>q : ℚ<VAR>n₁ d₁ n₂ : ℤ<VAR>h₁ : d₁ ≠ 0<GOAL>n₁ /. d₁ * (n₂ /. 0) = n₁ * n₂ /. (d₁ * 0)
<VAR>q : ℚ<VAR>n₁ d₁ n₂ d₂ : ℤ<VAR>h₁ : d₁ ≠ 0<VAR>h₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>s ⋖ t ↔ ∃ a ∉ s, insert a s = t
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>(f.comp C).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>hf : Function.Surjective ⇑f<VAR>this : (RingHom.ker f).IsMaximal<GOAL>(f.comp C).IsIntegral
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>S : Type u_2<VAR>inst✝ : Field S<VAR>f : R[X] →+* S<VAR>hf : Function.Surjective ⇑f<VAR>this : (RingHom.ker f).IsMaximal<VAR>g : R[X] ⧸ RingHom.ker f →+* S := Quotient.lift (RingHom.ker f) f ⋯<GOAL>(f.comp C).IsIntegral